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 16864

Description: Lemma for prmrec 16869. 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 7402	. . . 4 ⊢ ({0, 1} ↑_m (1...𝐾)) ∈ V
2		fveqeq2 6849	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑦) = 1))
3	2	elrab 3656	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1))
4		prmrec.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
5	4	ssrab3 4041	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 ⊆ (1...𝑁)
6		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → 𝑦 ∈ 𝑀)
7	6	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ 𝑀)
8	5, 7	sselid 3941	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ (1...𝑁))
9		elfznn 13490	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
10	8, 9	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℕ)
11		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
12		prmuz2 16642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ_≥‘2))
13	11, 12	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ (ℤ_≥‘2))
14		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
15	14	prmreclem1 16863	. . . . . . . . . . . . . . . . . 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 7384	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = (1↑2))
21		sq1 14136	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1↑2) = 1
22	20, 21	eqtrdi 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = 1)
23	22	oveq2d 7385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑦 / 1))
24	10	nncnd 12178	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℂ)
25	24	div1d 11926	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / 1) = 𝑦)
26	23, 25	eqtrd 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = 𝑦)
27	26	breq2d 5114	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ↔ (𝑛↑2) ∥ 𝑦))
28	10	nnzd 12532	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℤ)
29		2nn0 12435	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
30	29	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 2 ∈ ℕ₀)
31		pcdvdsb 16816	. . . . . . . . . . . . . . . . . 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 16797	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℕ₀)
36	35	nn0red 12480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℝ)
37		2re 12236	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
38		ltnle 11229	. . . . . . . . . . . . . . . 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 12225	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
42	40, 41	breqtrdi 5143	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < (1 + 1))
43	35	nn0zd 12531	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℤ)
44		1z 12539	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
45		zleltp1 12560	. . . . . . . . . . . . . 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 12811	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
49	35, 48	eleqtrdi 2838	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (ℤ_≥‘0))
50		elfz5 13453	. . . . . . . . . . . . 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 12516	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
54		fzpr 13516	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
55	53, 54	ax-mp 5	. . . . . . . . . . . 12 ⊢ (0...(0 + 1)) = {0, (0 + 1)}
56		1e0p1 12667	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
57	56	oveq2i 7380	. . . . . . . . . . . 12 ⊢ (0...1) = (0...(0 + 1))
58	56	preq2i 4697	. . . . . . . . . . . 12 ⊢ {0, 1} = {0, (0 + 1)}
59	55, 57, 58	3eqtr4i 2762	. . . . . . . . . . 11 ⊢ (0...1) = {0, 1}
60	52, 59	eleqtrdi 2838	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ {0, 1})
61		c0ex 11144	. . . . . . . . . . . 12 ⊢ 0 ∈ V
62	61	prid1 4722	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
63	62	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ ¬ 𝑛 ∈ ℙ) → 0 ∈ {0, 1})
64	60, 63	ifclda 4520	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ {0, 1})
65	64	fmpttd 7069	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
66		prex 5387	. . . . . . . . 9 ⊢ {0, 1} ∈ V
67		ovex 7402	. . . . . . . . 9 ⊢ (1...𝐾) ∈ V
68	66, 67	elmap 8821	. . . . . . . 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 6849	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑧) = 1))
73	72	elrab 3656	. . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))
74	3, 73	anbi12i 628	. . . . . 6 ⊢ ((𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ 𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ↔ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1)))
75		ovex 7402	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑦) ∈ V
76	75, 61	ifex 4535	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ V
77		eqid 2729	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))
78	76, 77	fnmpti 6643	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) Fn (1...𝐾)
79		ovex 7402	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑧) ∈ V
80	79, 61	ifex 4535	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) ∈ V
81		eqid 2729	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))
82	80, 81	fnmpti 6643	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) Fn (1...𝐾)
83		eqfnfv 6985	. . . . . . . . . 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 2811	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
86		oveq1 7376	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑦) = (𝑝 pCnt 𝑦))
87	85, 86	ifbieq1d 4509	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
88		ovex 7402	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑦) ∈ V
89	88, 61	ifex 4535	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) ∈ V
90	87, 77, 89	fvmpt 6950	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
91		oveq1 7376	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑧) = (𝑝 pCnt 𝑧))
92	85, 91	ifbieq1d 4509	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
93		ovex 7402	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑧) ∈ V
94	93, 61	ifex 4535	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∈ V
95	92, 81, 94	fvmpt 6950	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
96	90, 95	eqeq12d 2745	. . . . . . . . . 10 ⊢ (𝑝 ∈ (1...𝐾) → (((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
97	96	ralbiia 3073	. . . . . . . . 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 5106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
101	100	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
102	101	ralbidv 3156	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
103	102, 4	elrab2 3659	. . . . . . . . . . . . . 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 5106	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑧 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑧))
108	107	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑧 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑧))
109	108	ralbidv 3156	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑧 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
110	109, 4	elrab2 3659	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝑀 ↔ (𝑧 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
111	110	simprbi 496	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
112	106, 111	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
113		r19.26 3091	. . . . . . . . . . . . 13 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) ↔ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
114		eldifi 4090	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
115		fz1ssnn 13492	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ⊆ ℕ
116	5, 115	sstri 3953	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ⊆ ℕ
117	116, 99	sselid 3941	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ)
118		pceq0 16818	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
119	114, 117, 118	syl2anr 597	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
120	116, 106	sselid 3941	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ)
121		pceq0 16818	. . . . . . . . . . . . . . . . 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 2751	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
125	123, 124	biimtrrdi 254	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
126	125	ralimdva 3145	. . . . . . . . . . . . 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 4168	. . . . . . . . . . . . . . 15 ⊢ (ℙ ∩ (1...𝐾)) = ((1...𝐾) ∩ ℙ)
131	130	uneq1i 4123	. . . . . . . . . . . . . 14 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ))
132		inundif 4438	. . . . . . . . . . . . . 14 ⊢ (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
133	131, 132	eqtri 2752	. . . . . . . . . . . . 13 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
134	133	raleqi 3294	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
135		ralunb 4156	. . . . . . . . . . . 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 4091	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ((1...𝐾) ∖ ℙ) → ¬ 𝑝 ∈ ℙ)
138		iffalse 4493	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = 0)
139		iffalse 4493	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = 0)
140	138, 139	eqtr4d 2767	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
141	137, 140	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ((1...𝐾) ∖ ℙ) → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
142	141	rgen 3046	. . . . . . . . . . . . 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 4160	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (ℙ ∩ (1...𝐾)) → 𝑝 ∈ ℙ)
145		iftrue 4490	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = (𝑝 pCnt 𝑦))
146		iftrue 4490	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = (𝑝 pCnt 𝑧))
147	145, 146	eqeq12d 2745	. . . . . . . . . . . . . 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 3073	. . . . . . . . . . . 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 4438	. . . . . . . . . . . 12 ⊢ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾))) = ℙ
153	152	raleqi 3294	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
154		ralunb 4156	. . . . . . . . . . 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 12479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ₀)
158	120	nnnn0d 12479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ₀)
159		pc11 16827	. . . . . . . . . 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 8941	. . . 4 ⊢ (𝜑 → (({0, 1} ↑_m (1...𝐾)) ∈ V → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾))))
166	1, 165	mpi 20	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾)))
167		fzfi 13913	. . . . . . 7 ⊢ (1...𝑁) ∈ Fin
168		ssrab2 4039	. . . . . . 7 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)
169		ssfi 9114	. . . . . . 7 ⊢ (((1...𝑁) ∈ Fin ∧ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)) → {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin)
170	167, 168, 169	mp2an 692	. . . . . 6 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin
171	4, 170	eqeltri 2824	. . . . 5 ⊢ 𝑀 ∈ Fin
172		ssrab2 4039	. . . . 5 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
173		ssfi 9114	. . . . 5 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
174	171, 172, 173	mp2an 692	. . . 4 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
175		prfi 9250	. . . . 5 ⊢ {0, 1} ∈ Fin
176		fzfid 13914	. . . . 5 ⊢ (𝜑 → (1...𝐾) ∈ Fin)
177		mapfi 9275	. . . . 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 14320	. . . 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 14376	. . . 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 14340	. . . . 5 ⊢ (♯‘{0, 1}) = 2
185	184	a1i 11	. . . 4 ⊢ (𝜑 → (♯‘{0, 1}) = 2)
186		prmrec.2	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ)
187	186	nnnn0d 12479	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
188		hashfz1 14287	. . . . 5 ⊢ (𝐾 ∈ ℕ₀ → (♯‘(1...𝐾)) = 𝐾)
189	187, 188	syl 17	. . . 4 ⊢ (𝜑 → (♯‘(1...𝐾)) = 𝐾)
190	185, 189	oveq12d 7387	. . 3 ⊢ (𝜑 → ((♯‘{0, 1})↑(♯‘(1...𝐾))) = (2↑𝐾))
191	183, 190	eqtrd 2764	. 2 ⊢ (𝜑 → (♯‘({0, 1} ↑_m (1...𝐾))) = (2↑𝐾))
192	181, 191	breqtrd 5128	1 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ∀wral 3044 {crab 3402 Vcvv 3444 ∖ cdif 3908 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 ifcif 4484 {cpr 4587 class class class wbr 5102 ↦ cmpt 5183 Fn wfn 6494 ⟶wf 6495 ‘cfv 6499 (class class class)co 7369 ↑_m cmap 8776 ≼ cdom 8893 Fincfn 8895 supcsup 9367 ℝcr 11043 0cc0 11044 1c1 11045 + caddc 11047 < clt 11184 ≤ cle 11185 / cdiv 11811 ℕcn 12162 2c2 12217 ℕ₀cn0 12418 ℤcz 12505 ℤ_≥cuz 12769 ...cfz 13444 ↑cexp 14002 ♯chash 14271 ∥ cdvds 16198 ℙcprime 16617 pCnt cpc 16783

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-2o 8412 df-oadd 8415 df-er 8648 df-map 8778 df-pm 8779 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9369 df-inf 9370 df-dju 9830 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-xnn0 12492 df-z 12506 df-uz 12770 df-q 12884 df-rp 12928 df-fz 13445 df-fl 13730 df-mod 13808 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-dvds 16199 df-gcd 16441 df-prm 16618 df-pc 16784

This theorem is referenced by: prmreclem3 16865

W3C validator