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 16829

Description: Lemma for prmrec 16834. 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 7379	. . . 4 ⊢ ({0, 1} ↑_m (1...𝐾)) ∈ V
2		fveqeq2 6831	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑦) = 1))
3	2	elrab 3642	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1))
4		prmrec.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
5	4	ssrab3 4029	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 ⊆ (1...𝑁)
6		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → 𝑦 ∈ 𝑀)
7	6	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ 𝑀)
8	5, 7	sselid 3927	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ (1...𝑁))
9		elfznn 13453	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
10	8, 9	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℕ)
11		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
12		prmuz2 16607	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ_≥‘2))
13	11, 12	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ (ℤ_≥‘2))
14		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
15	14	prmreclem1 16828	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
16	15	simp3d 1144	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
17	10, 13, 16	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
18		simprr 772	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑄‘𝑦) = 1)
19	18	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑄‘𝑦) = 1)
20	19	oveq1d 7361	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = (1↑2))
21		sq1 14102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1↑2) = 1
22	20, 21	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = 1)
23	22	oveq2d 7362	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑦 / 1))
24	10	nncnd 12141	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℂ)
25	24	div1d 11889	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / 1) = 𝑦)
26	23, 25	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = 𝑦)
27	26	breq2d 5101	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ↔ (𝑛↑2) ∥ 𝑦))
28	10	nnzd 12495	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℤ)
29		2nn0 12398	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
30	29	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 2 ∈ ℕ₀)
31		pcdvdsb 16781	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 2 ∈ ℕ₀) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
32	11, 28, 30, 31	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
33	27, 32	bitr4d 282	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ↔ 2 ≤ (𝑛 pCnt 𝑦)))
34	17, 33	mtbid 324	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ 2 ≤ (𝑛 pCnt 𝑦))
35	11, 10	pccld 16762	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℕ₀)
36	35	nn0red 12443	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℝ)
37		2re 12199	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
38		ltnle 11192	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 pCnt 𝑦) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
39	36, 37, 38	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
40	34, 39	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < 2)
41		df-2 12188	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
42	40, 41	breqtrdi 5130	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < (1 + 1))
43	35	nn0zd 12494	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℤ)
44		1z 12502	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
45		zleltp1 12523	. . . . . . . . . . . . . 14 ⊢ (((𝑛 pCnt 𝑦) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
46	43, 44, 45	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
47	42, 46	mpbird 257	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ≤ 1)
48		nn0uz 12774	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
49	35, 48	eleqtrdi 2841	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (ℤ_≥‘0))
50		elfz5 13416	. . . . . . . . . . . . 13 ⊢ (((𝑛 pCnt 𝑦) ∈ (ℤ_≥‘0) ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
51	49, 44, 50	sylancl 586	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
52	47, 51	mpbird 257	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (0...1))
53		0z 12479	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
54		fzpr 13479	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
55	53, 54	ax-mp 5	. . . . . . . . . . . 12 ⊢ (0...(0 + 1)) = {0, (0 + 1)}
56		1e0p1 12630	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
57	56	oveq2i 7357	. . . . . . . . . . . 12 ⊢ (0...1) = (0...(0 + 1))
58	56	preq2i 4687	. . . . . . . . . . . 12 ⊢ {0, 1} = {0, (0 + 1)}
59	55, 57, 58	3eqtr4i 2764	. . . . . . . . . . 11 ⊢ (0...1) = {0, 1}
60	52, 59	eleqtrdi 2841	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ {0, 1})
61		c0ex 11106	. . . . . . . . . . . 12 ⊢ 0 ∈ V
62	61	prid1 4712	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
63	62	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ ¬ 𝑛 ∈ ℙ) → 0 ∈ {0, 1})
64	60, 63	ifclda 4508	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ {0, 1})
65	64	fmpttd 7048	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
66		prex 5373	. . . . . . . . 9 ⊢ {0, 1} ∈ V
67		ovex 7379	. . . . . . . . 9 ⊢ (1...𝐾) ∈ V
68	66, 67	elmap 8795	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_m (1...𝐾)) ↔ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
69	65, 68	sylibr 234	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_m (1...𝐾)))
70	69	ex 412	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_m (1...𝐾))))
71	3, 70	biimtrid 242	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_m (1...𝐾))))
72		fveqeq2 6831	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑧) = 1))
73	72	elrab 3642	. . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))
74	3, 73	anbi12i 628	. . . . . 6 ⊢ ((𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ 𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ↔ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1)))
75		ovex 7379	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑦) ∈ V
76	75, 61	ifex 4523	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ V
77		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))
78	76, 77	fnmpti 6624	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) Fn (1...𝐾)
79		ovex 7379	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑧) ∈ V
80	79, 61	ifex 4523	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) ∈ V
81		eqid 2731	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))
82	80, 81	fnmpti 6624	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) Fn (1...𝐾)
83		eqfnfv 6964	. . . . . . . . . 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))‘𝑝)))
84	78, 82, 83	mp2an 692	. . . . . . . . 9 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝))
85		eleq1w 2814	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
86		oveq1 7353	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑦) = (𝑝 pCnt 𝑦))
87	85, 86	ifbieq1d 4497	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
88		ovex 7379	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑦) ∈ V
89	88, 61	ifex 4523	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) ∈ V
90	87, 77, 89	fvmpt 6929	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
91		oveq1 7353	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑧) = (𝑝 pCnt 𝑧))
92	85, 91	ifbieq1d 4497	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
93		ovex 7379	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑧) ∈ V
94	93, 61	ifex 4523	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∈ V
95	92, 81, 94	fvmpt 6929	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
96	90, 95	eqeq12d 2747	. . . . . . . . . 10 ⊢ (𝑝 ∈ (1...𝐾) → (((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
97	96	ralbiia 3076	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
98	84, 97	bitri 275	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
99		simprll 778	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ 𝑀)
100		breq2 5093	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
101	100	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
102	101	ralbidv 3155	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
103	102, 4	elrab2 3645	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
104	103	simprbi 496	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
105	99, 104	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
106		simprrl 780	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ 𝑀)
107		breq2 5093	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑧 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑧))
108	107	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑧 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑧))
109	108	ralbidv 3155	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑧 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
110	109, 4	elrab2 3645	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝑀 ↔ (𝑧 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
111	110	simprbi 496	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
112	106, 111	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
113		r19.26 3092	. . . . . . . . . . . . 13 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) ↔ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
114		eldifi 4078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
115		fz1ssnn 13455	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ⊆ ℕ
116	5, 115	sstri 3939	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ⊆ ℕ
117	116, 99	sselid 3927	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ)
118		pceq0 16783	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
119	114, 117, 118	syl2anr 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
120	116, 106	sselid 3927	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ)
121		pceq0 16783	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑧 ∈ ℕ) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝 ∥ 𝑧))
122	114, 120, 121	syl2anr 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝 ∥ 𝑧))
123	119, 122	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) ↔ (¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧)))
124		eqtr3 2753	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
125	123, 124	biimtrrdi 254	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
126	125	ralimdva 3144	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
127	113, 126	biimtrrid 243	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ((∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
128	105, 112, 127	mp2and 699	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
129	128	biantrud 531	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))))
130		incom 4156	. . . . . . . . . . . . . . 15 ⊢ (ℙ ∩ (1...𝐾)) = ((1...𝐾) ∩ ℙ)
131	130	uneq1i 4111	. . . . . . . . . . . . . 14 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ))
132		inundif 4426	. . . . . . . . . . . . . 14 ⊢ (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
133	131, 132	eqtri 2754	. . . . . . . . . . . . 13 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
134	133	raleqi 3290	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
135		ralunb 4144	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
136	134, 135	bitr3i 277	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
137		eldifn 4079	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ((1...𝐾) ∖ ℙ) → ¬ 𝑝 ∈ ℙ)
138		iffalse 4481	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = 0)
139		iffalse 4481	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = 0)
140	138, 139	eqtr4d 2769	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
141	137, 140	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ((1...𝐾) ∖ ℙ) → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
142	141	rgen 3049	. . . . . . . . . . . . 13 ⊢ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)
143	142	biantru 529	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
144		elinel1 4148	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (ℙ ∩ (1...𝐾)) → 𝑝 ∈ ℙ)
145		iftrue 4478	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = (𝑝 pCnt 𝑦))
146		iftrue 4478	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = (𝑝 pCnt 𝑧))
147	145, 146	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℙ → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
148	144, 147	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (ℙ ∩ (1...𝐾)) → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
149	148	ralbiia 3076	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
150	143, 149	bitr3i 277	. . . . . . . . . . 11 ⊢ ((∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
151	136, 150	bitri 275	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
152		inundif 4426	. . . . . . . . . . . 12 ⊢ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾))) = ℙ
153	152	raleqi 3290	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
154		ralunb 4144	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
155	153, 154	bitr3i 277	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
156	129, 151, 155	3bitr4g 314	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
157	117	nnnn0d 12442	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ₀)
158	120	nnnn0d 12442	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ₀)
159		pc11 16792	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ 𝑧 ∈ ℕ₀) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
160	157, 158, 159	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
161	156, 160	bitr4d 282	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ 𝑦 = 𝑧))
162	98, 161	bitrid 283	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧))
163	162	ex 412	. . . . . 6 ⊢ (𝜑 → (((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1)) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
164	74, 163	biimtrid 242	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ 𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
165	71, 164	dom2d 8915	. . . 4 ⊢ (𝜑 → (({0, 1} ↑_m (1...𝐾)) ∈ V → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾))))
166	1, 165	mpi 20	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾)))
167		fzfi 13879	. . . . . . 7 ⊢ (1...𝑁) ∈ Fin
168		ssrab2 4027	. . . . . . 7 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)
169		ssfi 9082	. . . . . . 7 ⊢ (((1...𝑁) ∈ Fin ∧ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)) → {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin)
170	167, 168, 169	mp2an 692	. . . . . 6 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin
171	4, 170	eqeltri 2827	. . . . 5 ⊢ 𝑀 ∈ Fin
172		ssrab2 4027	. . . . 5 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
173		ssfi 9082	. . . . 5 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
174	171, 172, 173	mp2an 692	. . . 4 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
175		prfi 9208	. . . . 5 ⊢ {0, 1} ∈ Fin
176		fzfid 13880	. . . . 5 ⊢ (𝜑 → (1...𝐾) ∈ Fin)
177		mapfi 9232	. . . . 5 ⊢ (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → ({0, 1} ↑_m (1...𝐾)) ∈ Fin)
178	175, 176, 177	sylancr 587	. . . 4 ⊢ (𝜑 → ({0, 1} ↑_m (1...𝐾)) ∈ Fin)
179		hashdom 14286	. . . 4 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ ({0, 1} ↑_m (1...𝐾)) ∈ Fin) → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (♯‘({0, 1} ↑_m (1...𝐾))) ↔ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾))))
180	174, 178, 179	sylancr 587	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (♯‘({0, 1} ↑_m (1...𝐾))) ↔ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾))))
181	166, 180	mpbird 257	. 2 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (♯‘({0, 1} ↑_m (1...𝐾))))
182		hashmap 14342	. . . 4 ⊢ (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → (♯‘({0, 1} ↑_m (1...𝐾))) = ((♯‘{0, 1})↑(♯‘(1...𝐾))))
183	175, 176, 182	sylancr 587	. . 3 ⊢ (𝜑 → (♯‘({0, 1} ↑_m (1...𝐾))) = ((♯‘{0, 1})↑(♯‘(1...𝐾))))
184		prhash2ex 14306	. . . . 5 ⊢ (♯‘{0, 1}) = 2
185	184	a1i 11	. . . 4 ⊢ (𝜑 → (♯‘{0, 1}) = 2)
186		prmrec.2	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ)
187	186	nnnn0d 12442	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
188		hashfz1 14253	. . . . 5 ⊢ (𝐾 ∈ ℕ₀ → (♯‘(1...𝐾)) = 𝐾)
189	187, 188	syl 17	. . . 4 ⊢ (𝜑 → (♯‘(1...𝐾)) = 𝐾)
190	185, 189	oveq12d 7364	. . 3 ⊢ (𝜑 → ((♯‘{0, 1})↑(♯‘(1...𝐾))) = (2↑𝐾))
191	183, 190	eqtrd 2766	. 2 ⊢ (𝜑 → (♯‘({0, 1} ↑_m (1...𝐾))) = (2↑𝐾))
192	181, 191	breqtrd 5115	1 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ∀wral 3047 {crab 3395 Vcvv 3436 ∖ cdif 3894 ∪ cun 3895 ∩ cin 3896 ⊆ wss 3897 ifcif 4472 {cpr 4575 class class class wbr 5089 ↦ cmpt 5170 Fn wfn 6476 ⟶wf 6477 ‘cfv 6481 (class class class)co 7346 ↑_m cmap 8750 ≼ cdom 8867 Fincfn 8869 supcsup 9324 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 < clt 11146 ≤ cle 11147 / cdiv 11774 ℕcn 12125 2c2 12180 ℕ₀cn0 12381 ℤcz 12468 ℤ_≥cuz 12732 ...cfz 13407 ↑cexp 13968 ♯chash 14237 ∥ cdvds 16163 ℙcprime 16582 pCnt cpc 16748

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-oadd 8389 df-er 8622 df-map 8752 df-pm 8753 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-inf 9327 df-dju 9794 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-xnn0 12455 df-z 12469 df-uz 12733 df-q 12847 df-rp 12891 df-fz 13408 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-dvds 16164 df-gcd 16406 df-prm 16583 df-pc 16749

This theorem is referenced by: prmreclem3 16830

W3C validator