prmreclem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > prmreclem2		Structured version Visualization version GIF version

Theorem prmreclem2 15621

Description: Lemma for prmrec 15626. There are at most 2↑𝐾 squarefree numbers which divide no primes larger than 𝐾. (We could strengthen this to 2↑#(ℙ ∩ (1...𝐾)) but there's no reason to.) We establish the inequality by showing that the prime counts of the number up to 𝐾 completely determine it because all higher prime counts are zero, and they are all at most 1 because no square divides the number, so there are at most 2↑𝐾 possibilities. (Contributed by Mario Carneiro, 5-Aug-2014.)

**Hypotheses**
Ref	Expression
prmrec.1	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
prmrec.2	⊢ (𝜑 → 𝐾 ∈ ℕ)
prmrec.3	⊢ (𝜑 → 𝑁 ∈ ℕ)
prmrec.4	⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
prmreclem2.5	⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))

**Assertion**
Ref	Expression
prmreclem2	⊢ (𝜑 → (#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))

Distinct variable groups: 𝑛,𝑝,𝑟,𝑥,𝐹 𝑛,𝐾,𝑝,𝑥 𝑛,𝑀,𝑝,𝑥 𝜑,𝑛,𝑝,𝑥 𝑄,𝑛,𝑝,𝑟,𝑥 𝑛,𝑁,𝑝,𝑥 Allowed substitution hints: 𝜑(𝑟) 𝐾(𝑟) 𝑀(𝑟) 𝑁(𝑟)

Proof of Theorem prmreclem2 Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 6678	. . . 4 ⊢ ({0, 1} ↑_𝑚 (1...𝐾)) ∈ V
2		fveq2 6191	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑄‘𝑥) = (𝑄‘𝑦))
3	2	eqeq1d 2624	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑦) = 1))
4	3	elrab 3363	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1))
5		prmrec.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
6		ssrab2 3687	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)
7	5, 6	eqsstri 3635	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 ⊆ (1...𝑁)
8		simprl 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → 𝑦 ∈ 𝑀)
9	8	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ 𝑀)
10	7, 9	sseldi 3601	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ (1...𝑁))
11		elfznn 12370	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
12	10, 11	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℕ)
13		simpr 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
14		prmuz2 15408	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ_≥‘2))
15	13, 14	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ (ℤ_≥‘2))
16		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
17	16	prmreclem1 15620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
18	17	simp3d 1075	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
19	12, 15, 18	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
20		simprr 796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑄‘𝑦) = 1)
21	20	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑄‘𝑦) = 1)
22	21	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = (1↑2))
23		sq1 12958	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1↑2) = 1
24	22, 23	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = 1)
25	24	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑦 / 1))
26	12	nncnd 11036	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℂ)
27	26	div1d 10793	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / 1) = 𝑦)
28	25, 27	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = 𝑦)
29	28	breq2d 4665	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ↔ (𝑛↑2) ∥ 𝑦))
30	12	nnzd 11481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℤ)
31		2nn0 11309	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
32	31	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 2 ∈ ℕ₀)
33		pcdvdsb 15573	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 2 ∈ ℕ₀) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
34	13, 30, 32, 33	syl3anc 1326	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
35	29, 34	bitr4d 271	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ↔ 2 ≤ (𝑛 pCnt 𝑦)))
36	19, 35	mtbid 314	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ 2 ≤ (𝑛 pCnt 𝑦))
37	13, 12	pccld 15555	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℕ₀)
38	37	nn0red 11352	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℝ)
39		2re 11090	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
40		ltnle 10117	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 pCnt 𝑦) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
41	38, 39, 40	sylancl 694	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
42	36, 41	mpbird 247	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < 2)
43		df-2 11079	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
44	42, 43	syl6breq 4694	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < (1 + 1))
45	37	nn0zd 11480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℤ)
46		1z 11407	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
47		zleltp1 11428	. . . . . . . . . . . . . 14 ⊢ (((𝑛 pCnt 𝑦) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
48	45, 46, 47	sylancl 694	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
49	44, 48	mpbird 247	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ≤ 1)
50		nn0uz 11722	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
51	37, 50	syl6eleq 2711	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (ℤ_≥‘0))
52		elfz5 12334	. . . . . . . . . . . . 13 ⊢ (((𝑛 pCnt 𝑦) ∈ (ℤ_≥‘0) ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
53	51, 46, 52	sylancl 694	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
54	49, 53	mpbird 247	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (0...1))
55		0z 11388	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
56		fzpr 12396	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
57	55, 56	ax-mp 5	. . . . . . . . . . . 12 ⊢ (0...(0 + 1)) = {0, (0 + 1)}
58		1e0p1 11552	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
59	58	oveq2i 6661	. . . . . . . . . . . 12 ⊢ (0...1) = (0...(0 + 1))
60	58	preq2i 4272	. . . . . . . . . . . 12 ⊢ {0, 1} = {0, (0 + 1)}
61	57, 59, 60	3eqtr4i 2654	. . . . . . . . . . 11 ⊢ (0...1) = {0, 1}
62	54, 61	syl6eleq 2711	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ {0, 1})
63		c0ex 10034	. . . . . . . . . . . 12 ⊢ 0 ∈ V
64	63	prid1 4297	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
65	64	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ ¬ 𝑛 ∈ ℙ) → 0 ∈ {0, 1})
66	62, 65	ifclda 4120	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ {0, 1})
67		eqid 2622	. . . . . . . . 9 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))
68	66, 67	fmptd 6385	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
69		prex 4909	. . . . . . . . 9 ⊢ {0, 1} ∈ V
70		ovex 6678	. . . . . . . . 9 ⊢ (1...𝐾) ∈ V
71	69, 70	elmap 7886	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_𝑚 (1...𝐾)) ↔ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
72	68, 71	sylibr 224	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_𝑚 (1...𝐾)))
73	72	ex 450	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_𝑚 (1...𝐾))))
74	4, 73	syl5bi 232	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_𝑚 (1...𝐾))))
75		fveq2 6191	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑄‘𝑥) = (𝑄‘𝑧))
76	75	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑧) = 1))
77	76	elrab 3363	. . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))
78	4, 77	anbi12i 733	. . . . . 6 ⊢ ((𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ 𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ↔ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1)))
79		ovex 6678	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑦) ∈ V
80	79, 63	ifex 4156	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ V
81	80, 67	fnmpti 6022	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) Fn (1...𝐾)
82		ovex 6678	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑧) ∈ V
83	82, 63	ifex 4156	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) ∈ V
84		eqid 2622	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))
85	83, 84	fnmpti 6022	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) Fn (1...𝐾)
86		eqfnfv 6311	. . . . . . . . . 10 ⊢ (((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) Fn (1...𝐾) ∧ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) Fn (1...𝐾)) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝)))
87	81, 85, 86	mp2an 708	. . . . . . . . 9 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝))
88		eleq1 2689	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
89		oveq1 6657	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑦) = (𝑝 pCnt 𝑦))
90	88, 89	ifbieq1d 4109	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
91		ovex 6678	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑦) ∈ V
92	91, 63	ifex 4156	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) ∈ V
93	90, 67, 92	fvmpt 6282	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
94		oveq1 6657	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑧) = (𝑝 pCnt 𝑧))
95	88, 94	ifbieq1d 4109	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
96		ovex 6678	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑧) ∈ V
97	96, 63	ifex 4156	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∈ V
98	95, 84, 97	fvmpt 6282	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
99	93, 98	eqeq12d 2637	. . . . . . . . . 10 ⊢ (𝑝 ∈ (1...𝐾) → (((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
100	99	ralbiia 2979	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
101	87, 100	bitri 264	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
102		simprll 802	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ 𝑀)
103		breq2 4657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
104	103	notbid 308	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
105	104	ralbidv 2986	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
106	105, 5	elrab2 3366	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
107	106	simprbi 480	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
108	102, 107	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
109		simprrl 804	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ 𝑀)
110		breq2 4657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑧 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑧))
111	110	notbid 308	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑧 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑧))
112	111	ralbidv 2986	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑧 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
113	112, 5	elrab2 3366	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝑀 ↔ (𝑧 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
114	113	simprbi 480	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
115	109, 114	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
116		r19.26 3064	. . . . . . . . . . . . 13 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) ↔ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
117		eldifi 3732	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
118		fz1ssnn 12372	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ⊆ ℕ
119	7, 118	sstri 3612	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ⊆ ℕ
120	119, 102	sseldi 3601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ)
121		pceq0 15575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
122	117, 120, 121	syl2anr 495	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
123	119, 109	sseldi 3601	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ)
124		pceq0 15575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑧 ∈ ℕ) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝 ∥ 𝑧))
125	117, 123, 124	syl2anr 495	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝 ∥ 𝑧))
126	122, 125	anbi12d 747	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) ↔ (¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧)))
127		eqtr3 2643	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
128	126, 127	syl6bir 244	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
129	128	ralimdva 2962	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
130	116, 129	syl5bir 233	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ((∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
131	108, 115, 130	mp2and 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
132	131	biantrud 528	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))))
133		incom 3805	. . . . . . . . . . . . . . 15 ⊢ (ℙ ∩ (1...𝐾)) = ((1...𝐾) ∩ ℙ)
134	133	uneq1i 3763	. . . . . . . . . . . . . 14 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ))
135		inundif 4046	. . . . . . . . . . . . . 14 ⊢ (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
136	134, 135	eqtri 2644	. . . . . . . . . . . . 13 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
137	136	raleqi 3142	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
138		ralunb 3794	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
139	137, 138	bitr3i 266	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
140		eldifn 3733	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ((1...𝐾) ∖ ℙ) → ¬ 𝑝 ∈ ℙ)
141		iffalse 4095	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = 0)
142		iffalse 4095	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = 0)
143	141, 142	eqtr4d 2659	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
144	140, 143	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ((1...𝐾) ∖ ℙ) → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
145	144	rgen 2922	. . . . . . . . . . . . 13 ⊢ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)
146	145	biantru 526	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
147		elinel1 3799	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (ℙ ∩ (1...𝐾)) → 𝑝 ∈ ℙ)
148		iftrue 4092	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = (𝑝 pCnt 𝑦))
149		iftrue 4092	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = (𝑝 pCnt 𝑧))
150	148, 149	eqeq12d 2637	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℙ → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
151	147, 150	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (ℙ ∩ (1...𝐾)) → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
152	151	ralbiia 2979	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
153	146, 152	bitr3i 266	. . . . . . . . . . 11 ⊢ ((∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
154	139, 153	bitri 264	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
155		inundif 4046	. . . . . . . . . . . 12 ⊢ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾))) = ℙ
156	155	raleqi 3142	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
157		ralunb 3794	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
158	156, 157	bitr3i 266	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
159	132, 154, 158	3bitr4g 303	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
160	120	nnnn0d 11351	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ₀)
161	123	nnnn0d 11351	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ₀)
162		pc11 15584	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ 𝑧 ∈ ℕ₀) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
163	160, 161, 162	syl2anc 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
164	159, 163	bitr4d 271	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ 𝑦 = 𝑧))
165	101, 164	syl5bb 272	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧))
166	165	ex 450	. . . . . 6 ⊢ (𝜑 → (((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1)) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
167	78, 166	syl5bi 232	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ 𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
168	74, 167	dom2d 7996	. . . 4 ⊢ (𝜑 → (({0, 1} ↑_𝑚 (1...𝐾)) ∈ V → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_𝑚 (1...𝐾))))
169	1, 168	mpi 20	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_𝑚 (1...𝐾)))
170		fzfi 12771	. . . . . . 7 ⊢ (1...𝑁) ∈ Fin
171		ssfi 8180	. . . . . . 7 ⊢ (((1...𝑁) ∈ Fin ∧ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)) → {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin)
172	170, 6, 171	mp2an 708	. . . . . 6 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin
173	5, 172	eqeltri 2697	. . . . 5 ⊢ 𝑀 ∈ Fin
174		ssrab2 3687	. . . . 5 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
175		ssfi 8180	. . . . 5 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
176	173, 174, 175	mp2an 708	. . . 4 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
177		prfi 8235	. . . . 5 ⊢ {0, 1} ∈ Fin
178		fzfid 12772	. . . . 5 ⊢ (𝜑 → (1...𝐾) ∈ Fin)
179		mapfi 8262	. . . . 5 ⊢ (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → ({0, 1} ↑_𝑚 (1...𝐾)) ∈ Fin)
180	177, 178, 179	sylancr 695	. . . 4 ⊢ (𝜑 → ({0, 1} ↑_𝑚 (1...𝐾)) ∈ Fin)
181		hashdom 13168	. . . 4 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ ({0, 1} ↑_𝑚 (1...𝐾)) ∈ Fin) → ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (#‘({0, 1} ↑_𝑚 (1...𝐾))) ↔ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_𝑚 (1...𝐾))))
182	176, 180, 181	sylancr 695	. . 3 ⊢ (𝜑 → ((#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (#‘({0, 1} ↑_𝑚 (1...𝐾))) ↔ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_𝑚 (1...𝐾))))
183	169, 182	mpbird 247	. 2 ⊢ (𝜑 → (#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (#‘({0, 1} ↑_𝑚 (1...𝐾))))
184		hashmap 13222	. . . 4 ⊢ (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → (#‘({0, 1} ↑_𝑚 (1...𝐾))) = ((#‘{0, 1})↑(#‘(1...𝐾))))
185	177, 178, 184	sylancr 695	. . 3 ⊢ (𝜑 → (#‘({0, 1} ↑_𝑚 (1...𝐾))) = ((#‘{0, 1})↑(#‘(1...𝐾))))
186		prhash2ex 13187	. . . . 5 ⊢ (#‘{0, 1}) = 2
187	186	a1i 11	. . . 4 ⊢ (𝜑 → (#‘{0, 1}) = 2)
188		prmrec.2	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ)
189	188	nnnn0d 11351	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
190		hashfz1 13134	. . . . 5 ⊢ (𝐾 ∈ ℕ₀ → (#‘(1...𝐾)) = 𝐾)
191	189, 190	syl 17	. . . 4 ⊢ (𝜑 → (#‘(1...𝐾)) = 𝐾)
192	187, 191	oveq12d 6668	. . 3 ⊢ (𝜑 → ((#‘{0, 1})↑(#‘(1...𝐾))) = (2↑𝐾))
193	185, 192	eqtrd 2656	. 2 ⊢ (𝜑 → (#‘({0, 1} ↑_𝑚 (1...𝐾))) = (2↑𝐾))
194	183, 193	breqtrd 4679	1 ⊢ (𝜑 → (#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∀wral 2912 {crab 2916 Vcvv 3200 ∖ cdif 3571 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ifcif 4086 {cpr 4179 class class class wbr 4653 ↦ cmpt 4729 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↑_𝑚 cmap 7857 ≼ cdom 7953 Fincfn 7955 supcsup 8346 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 < clt 10074 ≤ cle 10075 / cdiv 10684 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ...cfz 12326 ↑cexp 12860 #chash 13117 ∥ cdvds 14983 ℙcprime 15385 pCnt cpc 15541

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-sup 8348 df-inf 8349 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-fz 12327 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-dvds 14984 df-gcd 15217 df-prm 15386 df-pc 15542

This theorem is referenced by: prmreclem3 15622

W3C validator