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 16919

Description: Lemma for prmrec 16924. 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 7457	. . . 4 ⊢ ({0, 1} ↑_m (1...𝐾)) ∈ V
2		fveqeq2 6910	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑦) = 1))
3	2	elrab 3681	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1))
4		prmrec.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
5	4	ssrab3 4079	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 ⊆ (1...𝑁)
6		simprl 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → 𝑦 ∈ 𝑀)
7	6	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ 𝑀)
8	5, 7	sselid 3977	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ (1...𝑁))
9		elfznn 13584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
10	8, 9	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℕ)
11		simpr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
12		prmuz2 16697	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ_≥‘2))
13	11, 12	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ (ℤ_≥‘2))
14		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
15	14	prmreclem1 16918	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
16	15	simp3d 1141	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
17	10, 13, 16	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
18		simprr 771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑄‘𝑦) = 1)
19	18	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑄‘𝑦) = 1)
20	19	oveq1d 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = (1↑2))
21		sq1 14213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1↑2) = 1
22	20, 21	eqtrdi 2782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = 1)
23	22	oveq2d 7440	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑦 / 1))
24	10	nncnd 12280	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℂ)
25	24	div1d 12033	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / 1) = 𝑦)
26	23, 25	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = 𝑦)
27	26	breq2d 5165	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ↔ (𝑛↑2) ∥ 𝑦))
28	10	nnzd 12637	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℤ)
29		2nn0 12541	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
30	29	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 2 ∈ ℕ₀)
31		pcdvdsb 16871	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 2 ∈ ℕ₀) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
32	11, 28, 30, 31	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
33	27, 32	bitr4d 281	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ↔ 2 ≤ (𝑛 pCnt 𝑦)))
34	17, 33	mtbid 323	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ 2 ≤ (𝑛 pCnt 𝑦))
35	11, 10	pccld 16852	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℕ₀)
36	35	nn0red 12585	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℝ)
37		2re 12338	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
38		ltnle 11343	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 pCnt 𝑦) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
39	36, 37, 38	sylancl 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
40	34, 39	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < 2)
41		df-2 12327	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
42	40, 41	breqtrdi 5194	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < (1 + 1))
43	35	nn0zd 12636	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℤ)
44		1z 12644	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
45		zleltp1 12665	. . . . . . . . . . . . . 14 ⊢ (((𝑛 pCnt 𝑦) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
46	43, 44, 45	sylancl 584	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
47	42, 46	mpbird 256	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ≤ 1)
48		nn0uz 12916	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
49	35, 48	eleqtrdi 2836	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (ℤ_≥‘0))
50		elfz5 13547	. . . . . . . . . . . . 13 ⊢ (((𝑛 pCnt 𝑦) ∈ (ℤ_≥‘0) ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
51	49, 44, 50	sylancl 584	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
52	47, 51	mpbird 256	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (0...1))
53		0z 12621	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
54		fzpr 13610	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
55	53, 54	ax-mp 5	. . . . . . . . . . . 12 ⊢ (0...(0 + 1)) = {0, (0 + 1)}
56		1e0p1 12771	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
57	56	oveq2i 7435	. . . . . . . . . . . 12 ⊢ (0...1) = (0...(0 + 1))
58	56	preq2i 4746	. . . . . . . . . . . 12 ⊢ {0, 1} = {0, (0 + 1)}
59	55, 57, 58	3eqtr4i 2764	. . . . . . . . . . 11 ⊢ (0...1) = {0, 1}
60	52, 59	eleqtrdi 2836	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ {0, 1})
61		c0ex 11258	. . . . . . . . . . . 12 ⊢ 0 ∈ V
62	61	prid1 4771	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
63	62	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ ¬ 𝑛 ∈ ℙ) → 0 ∈ {0, 1})
64	60, 63	ifclda 4568	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ {0, 1})
65	64	fmpttd 7129	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
66		prex 5438	. . . . . . . . 9 ⊢ {0, 1} ∈ V
67		ovex 7457	. . . . . . . . 9 ⊢ (1...𝐾) ∈ V
68	66, 67	elmap 8900	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_m (1...𝐾)) ↔ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
69	65, 68	sylibr 233	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_m (1...𝐾)))
70	69	ex 411	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_m (1...𝐾))))
71	3, 70	biimtrid 241	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_m (1...𝐾))))
72		fveqeq2 6910	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑧) = 1))
73	72	elrab 3681	. . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))
74	3, 73	anbi12i 626	. . . . . 6 ⊢ ((𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ 𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ↔ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1)))
75		ovex 7457	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑦) ∈ V
76	75, 61	ifex 4583	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ V
77		eqid 2726	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))
78	76, 77	fnmpti 6704	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) Fn (1...𝐾)
79		ovex 7457	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑧) ∈ V
80	79, 61	ifex 4583	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) ∈ V
81		eqid 2726	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))
82	80, 81	fnmpti 6704	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) Fn (1...𝐾)
83		eqfnfv 7044	. . . . . . . . . 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 690	. . . . . . . . 9 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝))
85		eleq1w 2809	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
86		oveq1 7431	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑦) = (𝑝 pCnt 𝑦))
87	85, 86	ifbieq1d 4557	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
88		ovex 7457	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑦) ∈ V
89	88, 61	ifex 4583	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) ∈ V
90	87, 77, 89	fvmpt 7009	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
91		oveq1 7431	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑧) = (𝑝 pCnt 𝑧))
92	85, 91	ifbieq1d 4557	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
93		ovex 7457	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑧) ∈ V
94	93, 61	ifex 4583	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∈ V
95	92, 81, 94	fvmpt 7009	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
96	90, 95	eqeq12d 2742	. . . . . . . . . 10 ⊢ (𝑝 ∈ (1...𝐾) → (((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
97	96	ralbiia 3081	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
98	84, 97	bitri 274	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
99		simprll 777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ 𝑀)
100		breq2 5157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
101	100	notbid 317	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
102	101	ralbidv 3168	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
103	102, 4	elrab2 3684	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
104	103	simprbi 495	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
105	99, 104	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
106		simprrl 779	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ 𝑀)
107		breq2 5157	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑧 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑧))
108	107	notbid 317	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑧 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑧))
109	108	ralbidv 3168	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑧 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
110	109, 4	elrab2 3684	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝑀 ↔ (𝑧 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
111	110	simprbi 495	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
112	106, 111	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
113		r19.26 3101	. . . . . . . . . . . . 13 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) ↔ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
114		eldifi 4126	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
115		fz1ssnn 13586	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ⊆ ℕ
116	5, 115	sstri 3989	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ⊆ ℕ
117	116, 99	sselid 3977	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ)
118		pceq0 16873	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
119	114, 117, 118	syl2anr 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
120	116, 106	sselid 3977	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ)
121		pceq0 16873	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑧 ∈ ℕ) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝 ∥ 𝑧))
122	114, 120, 121	syl2anr 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝 ∥ 𝑧))
123	119, 122	anbi12d 630	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) ↔ (¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧)))
124		eqtr3 2752	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
125	123, 124	biimtrrdi 253	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
126	125	ralimdva 3157	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
127	113, 126	biimtrrid 242	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ((∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
128	105, 112, 127	mp2and 697	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
129	128	biantrud 530	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))))
130		incom 4202	. . . . . . . . . . . . . . 15 ⊢ (ℙ ∩ (1...𝐾)) = ((1...𝐾) ∩ ℙ)
131	130	uneq1i 4159	. . . . . . . . . . . . . 14 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ))
132		inundif 4483	. . . . . . . . . . . . . 14 ⊢ (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
133	131, 132	eqtri 2754	. . . . . . . . . . . . 13 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
134	133	raleqi 3313	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
135		ralunb 4192	. . . . . . . . . . . 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 276	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
137		eldifn 4127	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ((1...𝐾) ∖ ℙ) → ¬ 𝑝 ∈ ℙ)
138		iffalse 4542	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = 0)
139		iffalse 4542	. . . . . . . . . . . . . . . 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 3053	. . . . . . . . . . . . 13 ⊢ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)
143	142	biantru 528	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
144		elinel1 4196	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (ℙ ∩ (1...𝐾)) → 𝑝 ∈ ℙ)
145		iftrue 4539	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = (𝑝 pCnt 𝑦))
146		iftrue 4539	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = (𝑝 pCnt 𝑧))
147	145, 146	eqeq12d 2742	. . . . . . . . . . . . . 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 3081	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
150	143, 149	bitr3i 276	. . . . . . . . . . 11 ⊢ ((∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
151	136, 150	bitri 274	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
152		inundif 4483	. . . . . . . . . . . 12 ⊢ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾))) = ℙ
153	152	raleqi 3313	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
154		ralunb 4192	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
155	153, 154	bitr3i 276	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
156	129, 151, 155	3bitr4g 313	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
157	117	nnnn0d 12584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ₀)
158	120	nnnn0d 12584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ₀)
159		pc11 16882	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ 𝑧 ∈ ℕ₀) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
160	157, 158, 159	syl2anc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
161	156, 160	bitr4d 281	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ 𝑦 = 𝑧))
162	98, 161	bitrid 282	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧))
163	162	ex 411	. . . . . 6 ⊢ (𝜑 → (((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1)) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
164	74, 163	biimtrid 241	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ 𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
165	71, 164	dom2d 9024	. . . 4 ⊢ (𝜑 → (({0, 1} ↑_m (1...𝐾)) ∈ V → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾))))
166	1, 165	mpi 20	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾)))
167		fzfi 13992	. . . . . . 7 ⊢ (1...𝑁) ∈ Fin
168		ssrab2 4076	. . . . . . 7 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)
169		ssfi 9211	. . . . . . 7 ⊢ (((1...𝑁) ∈ Fin ∧ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)) → {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin)
170	167, 168, 169	mp2an 690	. . . . . 6 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin
171	4, 170	eqeltri 2822	. . . . 5 ⊢ 𝑀 ∈ Fin
172		ssrab2 4076	. . . . 5 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
173		ssfi 9211	. . . . 5 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
174	171, 172, 173	mp2an 690	. . . 4 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
175		prfi 9365	. . . . 5 ⊢ {0, 1} ∈ Fin
176		fzfid 13993	. . . . 5 ⊢ (𝜑 → (1...𝐾) ∈ Fin)
177		mapfi 9392	. . . . 5 ⊢ (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → ({0, 1} ↑_m (1...𝐾)) ∈ Fin)
178	175, 176, 177	sylancr 585	. . . 4 ⊢ (𝜑 → ({0, 1} ↑_m (1...𝐾)) ∈ Fin)
179		hashdom 14396	. . . 4 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ ({0, 1} ↑_m (1...𝐾)) ∈ Fin) → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (♯‘({0, 1} ↑_m (1...𝐾))) ↔ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾))))
180	174, 178, 179	sylancr 585	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (♯‘({0, 1} ↑_m (1...𝐾))) ↔ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_m (1...𝐾))))
181	166, 180	mpbird 256	. 2 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (♯‘({0, 1} ↑_m (1...𝐾))))
182		hashmap 14452	. . . 4 ⊢ (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → (♯‘({0, 1} ↑_m (1...𝐾))) = ((♯‘{0, 1})↑(♯‘(1...𝐾))))
183	175, 176, 182	sylancr 585	. . 3 ⊢ (𝜑 → (♯‘({0, 1} ↑_m (1...𝐾))) = ((♯‘{0, 1})↑(♯‘(1...𝐾))))
184		prhash2ex 14416	. . . . 5 ⊢ (♯‘{0, 1}) = 2
185	184	a1i 11	. . . 4 ⊢ (𝜑 → (♯‘{0, 1}) = 2)
186		prmrec.2	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ)
187	186	nnnn0d 12584	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
188		hashfz1 14363	. . . . 5 ⊢ (𝐾 ∈ ℕ₀ → (♯‘(1...𝐾)) = 𝐾)
189	187, 188	syl 17	. . . 4 ⊢ (𝜑 → (♯‘(1...𝐾)) = 𝐾)
190	185, 189	oveq12d 7442	. . 3 ⊢ (𝜑 → ((♯‘{0, 1})↑(♯‘(1...𝐾))) = (2↑𝐾))
191	183, 190	eqtrd 2766	. 2 ⊢ (𝜑 → (♯‘({0, 1} ↑_m (1...𝐾))) = (2↑𝐾))
192	181, 191	breqtrd 5179	1 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ∀wral 3051 {crab 3419 Vcvv 3462 ∖ cdif 3944 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ifcif 4533 {cpr 4635 class class class wbr 5153 ↦ cmpt 5236 Fn wfn 6549 ⟶wf 6550 ‘cfv 6554 (class class class)co 7424 ↑_m cmap 8855 ≼ cdom 8972 Fincfn 8974 supcsup 9483 ℝcr 11157 0cc0 11158 1c1 11159 + caddc 11161 < clt 11298 ≤ cle 11299 / cdiv 11921 ℕcn 12264 2c2 12319 ℕ₀cn0 12524 ℤcz 12610 ℤ_≥cuz 12874 ...cfz 13538 ↑cexp 14081 ♯chash 14347 ∥ cdvds 16256 ℙcprime 16672 pCnt cpc 16838

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 ax-cnex 11214 ax-resscn 11215 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-addrcl 11219 ax-mulcl 11220 ax-mulrcl 11221 ax-mulcom 11222 ax-addass 11223 ax-mulass 11224 ax-distr 11225 ax-i2m1 11226 ax-1ne0 11227 ax-1rid 11228 ax-rnegex 11229 ax-rrecex 11230 ax-cnre 11231 ax-pre-lttri 11232 ax-pre-lttrn 11233 ax-pre-ltadd 11234 ax-pre-mulgt0 11235 ax-pre-sup 11236

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-int 4955 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6312 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-riota 7380 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7877 df-1st 8003 df-2nd 8004 df-frecs 8296 df-wrecs 8327 df-recs 8401 df-rdg 8440 df-1o 8496 df-2o 8497 df-oadd 8500 df-er 8734 df-map 8857 df-pm 8858 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-sup 9485 df-inf 9486 df-dju 9944 df-card 9982 df-pnf 11300 df-mnf 11301 df-xr 11302 df-ltxr 11303 df-le 11304 df-sub 11496 df-neg 11497 df-div 11922 df-nn 12265 df-2 12327 df-3 12328 df-n0 12525 df-xnn0 12597 df-z 12611 df-uz 12875 df-q 12985 df-rp 13029 df-fz 13539 df-fl 13812 df-mod 13890 df-seq 14022 df-exp 14082 df-hash 14348 df-cj 15104 df-re 15105 df-im 15106 df-sqrt 15240 df-abs 15241 df-dvds 16257 df-gcd 16495 df-prm 16673 df-pc 16839

This theorem is referenced by: prmreclem3 16920

W3C validator