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 15838

Description: Lemma for prmrec 15843. 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 6906	. . . 4 ⊢ ({0, 1} ↑_𝑚 (1...𝐾)) ∈ V
2		fveqeq2 6417	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑦) = 1))
3	2	elrab 3559	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1))
4		prmrec.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
5		ssrab2 3884	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)
6	4, 5	eqsstri 3832	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 ⊆ (1...𝑁)
7		simprl 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → 𝑦 ∈ 𝑀)
8	7	ad2antrr 708	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ 𝑀)
9	6, 8	sseldi 3796	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ (1...𝑁))
10		elfznn 12593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
11	9, 10	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℕ)
12		simpr 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
13		prmuz2 15626	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ_≥‘2))
14	12, 13	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ (ℤ_≥‘2))
15		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
16	15	prmreclem1 15837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
17	16	simp3d 1167	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
18	11, 14, 17	sylc 65	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
19		simprr 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑄‘𝑦) = 1)
20	19	ad2antrr 708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑄‘𝑦) = 1)
21	20	oveq1d 6889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = (1↑2))
22		sq1 13181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1↑2) = 1
23	21, 22	syl6eq 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄‘𝑦)↑2) = 1)
24	23	oveq2d 6890	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑦 / 1))
25	11	nncnd 11321	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℂ)
26	25	div1d 11078	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / 1) = 𝑦)
27	24, 26	eqtrd 2840	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄‘𝑦)↑2)) = 𝑦)
28	27	breq2d 4856	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ↔ (𝑛↑2) ∥ 𝑦))
29	11	nnzd 11747	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℤ)
30		2nn0 11576	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ₀
31	30	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 2 ∈ ℕ₀)
32		pcdvdsb 15790	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 2 ∈ ℕ₀) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
33	12, 29, 31, 32	syl3anc 1483	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
34	28, 33	bitr4d 273	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ↔ 2 ≤ (𝑛 pCnt 𝑦)))
35	18, 34	mtbid 315	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ 2 ≤ (𝑛 pCnt 𝑦))
36	12, 11	pccld 15772	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℕ₀)
37	36	nn0red 11618	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℝ)
38		2re 11374	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℝ
39		ltnle 10402	. . . . . . . . . . . . . . . 16 ⊢ (((𝑛 pCnt 𝑦) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
40	37, 38, 39	sylancl 576	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
41	35, 40	mpbird 248	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < 2)
42		df-2 11364	. . . . . . . . . . . . . 14 ⊢ 2 = (1 + 1)
43	41, 42	syl6breq 4885	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < (1 + 1))
44	36	nn0zd 11746	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℤ)
45		1z 11673	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℤ
46		zleltp1 11694	. . . . . . . . . . . . . 14 ⊢ (((𝑛 pCnt 𝑦) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
47	44, 45, 46	sylancl 576	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
48	43, 47	mpbird 248	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ≤ 1)
49		nn0uz 11940	. . . . . . . . . . . . . 14 ⊢ ℕ₀ = (ℤ_≥‘0)
50	36, 49	syl6eleq 2895	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (ℤ_≥‘0))
51		elfz5 12557	. . . . . . . . . . . . 13 ⊢ (((𝑛 pCnt 𝑦) ∈ (ℤ_≥‘0) ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
52	50, 45, 51	sylancl 576	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
53	48, 52	mpbird 248	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (0...1))
54		0z 11654	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
55		fzpr 12619	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
56	54, 55	ax-mp 5	. . . . . . . . . . . 12 ⊢ (0...(0 + 1)) = {0, (0 + 1)}
57		1e0p1 11801	. . . . . . . . . . . . 13 ⊢ 1 = (0 + 1)
58	57	oveq2i 6885	. . . . . . . . . . . 12 ⊢ (0...1) = (0...(0 + 1))
59	57	preq2i 4463	. . . . . . . . . . . 12 ⊢ {0, 1} = {0, (0 + 1)}
60	56, 58, 59	3eqtr4i 2838	. . . . . . . . . . 11 ⊢ (0...1) = {0, 1}
61	53, 60	syl6eleq 2895	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ {0, 1})
62		c0ex 10319	. . . . . . . . . . . 12 ⊢ 0 ∈ V
63	62	prid1 4488	. . . . . . . . . . 11 ⊢ 0 ∈ {0, 1}
64	63	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ ¬ 𝑛 ∈ ℙ) → 0 ∈ {0, 1})
65	61, 64	ifclda 4313	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ {0, 1})
66	65	fmpttd 6607	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
67		prex 5099	. . . . . . . . 9 ⊢ {0, 1} ∈ V
68		ovex 6906	. . . . . . . . 9 ⊢ (1...𝐾) ∈ V
69	67, 68	elmap 8121	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_𝑚 (1...𝐾)) ↔ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
70	66, 69	sylibr 225	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_𝑚 (1...𝐾)))
71	70	ex 399	. . . . . 6 ⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_𝑚 (1...𝐾))))
72	3, 71	syl5bi 233	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑_𝑚 (1...𝐾))))
73		fveqeq2 6417	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝑄‘𝑥) = 1 ↔ (𝑄‘𝑧) = 1))
74	73	elrab 3559	. . . . . . 7 ⊢ (𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ↔ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))
75	3, 74	anbi12i 614	. . . . . 6 ⊢ ((𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ 𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ↔ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1)))
76		ovex 6906	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑦) ∈ V
77	76, 62	ifex 4327	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ V
78		eqid 2806	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))
79	77, 78	fnmpti 6233	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) Fn (1...𝐾)
80		ovex 6906	. . . . . . . . . . . 12 ⊢ (𝑛 pCnt 𝑧) ∈ V
81	80, 62	ifex 4327	. . . . . . . . . . 11 ⊢ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) ∈ V
82		eqid 2806	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))
83	81, 82	fnmpti 6233	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) Fn (1...𝐾)
84		eqfnfv 6533	. . . . . . . . . 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))‘𝑝)))
85	79, 83, 84	mp2an 675	. . . . . . . . 9 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝))
86		eleq1w 2868	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
87		oveq1 6881	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑦) = (𝑝 pCnt 𝑦))
88	86, 87	ifbieq1d 4302	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
89		ovex 6906	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑦) ∈ V
90	89, 62	ifex 4327	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) ∈ V
91	88, 78, 90	fvmpt 6503	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
92		oveq1 6881	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt 𝑧) = (𝑝 pCnt 𝑧))
93	86, 92	ifbieq1d 4302	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
94		ovex 6906	. . . . . . . . . . . . 13 ⊢ (𝑝 pCnt 𝑧) ∈ V
95	94, 62	ifex 4327	. . . . . . . . . . . 12 ⊢ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∈ V
96	93, 82, 95	fvmpt 6503	. . . . . . . . . . 11 ⊢ (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
97	91, 96	eqeq12d 2821	. . . . . . . . . 10 ⊢ (𝑝 ∈ (1...𝐾) → (((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
98	97	ralbiia 3167	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
99	85, 98	bitri 266	. . . . . . . 8 ⊢ ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
100		simprll 788	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ 𝑀)
101		breq2 4848	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
102	101	notbid 309	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
103	102	ralbidv 3174	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
104	103, 4	elrab2 3562	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
105	104	simprbi 486	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
106	100, 105	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
107		simprrl 790	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ 𝑀)
108		breq2 4848	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑧 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑧))
109	108	notbid 309	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑧 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑧))
110	109	ralbidv 3174	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑧 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
111	110, 4	elrab2 3562	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ 𝑀 ↔ (𝑧 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
112	111	simprbi 486	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
113	107, 112	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧)
114		r19.26 3252	. . . . . . . . . . . . 13 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) ↔ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧))
115		eldifi 3931	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
116		fz1ssnn 12595	. . . . . . . . . . . . . . . . . . 19 ⊢ (1...𝑁) ⊆ ℕ
117	6, 116	sstri 3807	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ⊆ ℕ
118	117, 100	sseldi 3796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ)
119		pceq0 15792	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
120	115, 118, 119	syl2anr 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝 ∥ 𝑦))
121	117, 107	sseldi 3796	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ)
122		pceq0 15792	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ ℙ ∧ 𝑧 ∈ ℕ) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝 ∥ 𝑧))
123	115, 121, 122	syl2anr 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝 ∥ 𝑧))
124	120, 123	anbi12d 618	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) ↔ (¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧)))
125		eqtr3 2827	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
126	124, 125	syl6bir 245	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
127	126	ralimdva 3150	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝 ∥ 𝑦 ∧ ¬ 𝑝 ∥ 𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
128	114, 127	syl5bir 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ((∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
129	106, 113, 128	mp2and 682	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
130	129	biantrud 523	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))))
131		incom 4004	. . . . . . . . . . . . . . 15 ⊢ (ℙ ∩ (1...𝐾)) = ((1...𝐾) ∩ ℙ)
132	131	uneq1i 3962	. . . . . . . . . . . . . 14 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ))
133		inundif 4242	. . . . . . . . . . . . . 14 ⊢ (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
134	132, 133	eqtri 2828	. . . . . . . . . . . . 13 ⊢ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
135	134	raleqi 3331	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
136		ralunb 3993	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
137	135, 136	bitr3i 268	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
138		eldifn 3932	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ((1...𝐾) ∖ ℙ) → ¬ 𝑝 ∈ ℙ)
139		iffalse 4288	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = 0)
140		iffalse 4288	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = 0)
141	139, 140	eqtr4d 2843	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
142	138, 141	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ((1...𝐾) ∖ ℙ) → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
143	142	rgen 3110	. . . . . . . . . . . . 13 ⊢ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)
144	143	biantru 521	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
145		elinel1 3998	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (ℙ ∩ (1...𝐾)) → 𝑝 ∈ ℙ)
146		iftrue 4285	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = (𝑝 pCnt 𝑦))
147		iftrue 4285	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = (𝑝 pCnt 𝑧))
148	146, 147	eqeq12d 2821	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℙ → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
149	145, 148	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (ℙ ∩ (1...𝐾)) → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
150	149	ralbiia 3167	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
151	144, 150	bitr3i 268	. . . . . . . . . . 11 ⊢ ((∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
152	137, 151	bitri 266	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
153		inundif 4242	. . . . . . . . . . . 12 ⊢ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾))) = ℙ
154	153	raleqi 3331	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
155		ralunb 3993	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
156	154, 155	bitr3i 268	. . . . . . . . . 10 ⊢ (∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
157	130, 152, 156	3bitr4g 305	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
158	118	nnnn0d 11617	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑦 ∈ ℕ₀)
159	121	nnnn0d 11617	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → 𝑧 ∈ ℕ₀)
160		pc11 15801	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ₀ ∧ 𝑧 ∈ ℕ₀) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
161	158, 159, 160	syl2anc 575	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
162	157, 161	bitr4d 273	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ 𝑦 = 𝑧))
163	99, 162	syl5bb 274	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1))) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧))
164	163	ex 399	. . . . . 6 ⊢ (𝜑 → (((𝑦 ∈ 𝑀 ∧ (𝑄‘𝑦) = 1) ∧ (𝑧 ∈ 𝑀 ∧ (𝑄‘𝑧) = 1)) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
165	75, 164	syl5bi 233	. . . . 5 ⊢ (𝜑 → ((𝑦 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∧ 𝑧 ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
166	72, 165	dom2d 8233	. . . 4 ⊢ (𝜑 → (({0, 1} ↑_𝑚 (1...𝐾)) ∈ V → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_𝑚 (1...𝐾))))
167	1, 166	mpi 20	. . 3 ⊢ (𝜑 → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_𝑚 (1...𝐾)))
168		fzfi 12995	. . . . . . 7 ⊢ (1...𝑁) ∈ Fin
169		ssfi 8419	. . . . . . 7 ⊢ (((1...𝑁) ∈ Fin ∧ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁)) → {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin)
170	168, 5, 169	mp2an 675	. . . . . 6 ⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ∈ Fin
171	4, 170	eqeltri 2881	. . . . 5 ⊢ 𝑀 ∈ Fin
172		ssrab2 3884	. . . . 5 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
173		ssfi 8419	. . . . 5 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
174	171, 172, 173	mp2an 675	. . . 4 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
175		prfi 8474	. . . . 5 ⊢ {0, 1} ∈ Fin
176		fzfid 12996	. . . . 5 ⊢ (𝜑 → (1...𝐾) ∈ Fin)
177		mapfi 8501	. . . . 5 ⊢ (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → ({0, 1} ↑_𝑚 (1...𝐾)) ∈ Fin)
178	175, 176, 177	sylancr 577	. . . 4 ⊢ (𝜑 → ({0, 1} ↑_𝑚 (1...𝐾)) ∈ Fin)
179		hashdom 13386	. . . 4 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ ({0, 1} ↑_𝑚 (1...𝐾)) ∈ Fin) → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (♯‘({0, 1} ↑_𝑚 (1...𝐾))) ↔ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_𝑚 (1...𝐾))))
180	174, 178, 179	sylancr 577	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (♯‘({0, 1} ↑_𝑚 (1...𝐾))) ↔ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ≼ ({0, 1} ↑_𝑚 (1...𝐾))))
181	167, 180	mpbird 248	. 2 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (♯‘({0, 1} ↑_𝑚 (1...𝐾))))
182		hashmap 13439	. . . 4 ⊢ (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → (♯‘({0, 1} ↑_𝑚 (1...𝐾))) = ((♯‘{0, 1})↑(♯‘(1...𝐾))))
183	175, 176, 182	sylancr 577	. . 3 ⊢ (𝜑 → (♯‘({0, 1} ↑_𝑚 (1...𝐾))) = ((♯‘{0, 1})↑(♯‘(1...𝐾))))
184		prhash2ex 13404	. . . . 5 ⊢ (♯‘{0, 1}) = 2
185	184	a1i 11	. . . 4 ⊢ (𝜑 → (♯‘{0, 1}) = 2)
186		prmrec.2	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ)
187	186	nnnn0d 11617	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
188		hashfz1 13354	. . . . 5 ⊢ (𝐾 ∈ ℕ₀ → (♯‘(1...𝐾)) = 𝐾)
189	187, 188	syl 17	. . . 4 ⊢ (𝜑 → (♯‘(1...𝐾)) = 𝐾)
190	185, 189	oveq12d 6892	. . 3 ⊢ (𝜑 → ((♯‘{0, 1})↑(♯‘(1...𝐾))) = (2↑𝐾))
191	183, 190	eqtrd 2840	. 2 ⊢ (𝜑 → (♯‘({0, 1} ↑_𝑚 (1...𝐾))) = (2↑𝐾))
192	181, 191	breqtrd 4870	1 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 = wceq 1637 ∈ wcel 2156 ∀wral 3096 {crab 3100 Vcvv 3391 ∖ cdif 3766 ∪ cun 3767 ∩ cin 3768 ⊆ wss 3769 ifcif 4279 {cpr 4372 class class class wbr 4844 ↦ cmpt 4923 Fn wfn 6096 ⟶wf 6097 ‘cfv 6101 (class class class)co 6874 ↑_𝑚 cmap 8092 ≼ cdom 8190 Fincfn 8192 supcsup 8585 ℝcr 10220 0cc0 10221 1c1 10222 + caddc 10224 < clt 10359 ≤ cle 10360 / cdiv 10969 ℕcn 11305 2c2 11356 ℕ₀cn0 11559 ℤcz 11643 ℤ_≥cuz 11904 ...cfz 12549 ↑cexp 13083 ♯chash 13337 ∥ cdvds 15203 ℙcprime 15603 pCnt cpc 15758

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2068 ax-7 2104 ax-8 2158 ax-9 2165 ax-10 2185 ax-11 2201 ax-12 2214 ax-13 2420 ax-ext 2784 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5096 ax-un 7179 ax-cnex 10277 ax-resscn 10278 ax-1cn 10279 ax-icn 10280 ax-addcl 10281 ax-addrcl 10282 ax-mulcl 10283 ax-mulrcl 10284 ax-mulcom 10285 ax-addass 10286 ax-mulass 10287 ax-distr 10288 ax-i2m1 10289 ax-1ne0 10290 ax-1rid 10291 ax-rnegex 10292 ax-rrecex 10293 ax-cnre 10294 ax-pre-lttri 10295 ax-pre-lttrn 10296 ax-pre-ltadd 10297 ax-pre-mulgt0 10298 ax-pre-sup 10299

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-ex 1860 df-nf 1864 df-sb 2061 df-eu 2634 df-mo 2635 df-clab 2793 df-cleq 2799 df-clel 2802 df-nfc 2937 df-ne 2979 df-nel 3082 df-ral 3101 df-rex 3102 df-reu 3103 df-rmo 3104 df-rab 3105 df-v 3393 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4117 df-if 4280 df-pw 4353 df-sn 4371 df-pr 4373 df-tp 4375 df-op 4377 df-uni 4631 df-int 4670 df-iun 4714 df-br 4845 df-opab 4907 df-mpt 4924 df-tr 4947 df-id 5219 df-eprel 5224 df-po 5232 df-so 5233 df-fr 5270 df-we 5272 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-rn 5322 df-res 5323 df-ima 5324 df-pred 5893 df-ord 5939 df-on 5940 df-lim 5941 df-suc 5942 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-riota 6835 df-ov 6877 df-oprab 6878 df-mpt2 6879 df-om 7296 df-1st 7398 df-2nd 7399 df-wrecs 7642 df-recs 7704 df-rdg 7742 df-1o 7796 df-2o 7797 df-oadd 7800 df-er 7979 df-map 8094 df-pm 8095 df-en 8193 df-dom 8194 df-sdom 8195 df-fin 8196 df-sup 8587 df-inf 8588 df-card 9048 df-cda 9275 df-pnf 10361 df-mnf 10362 df-xr 10363 df-ltxr 10364 df-le 10365 df-sub 10553 df-neg 10554 df-div 10970 df-nn 11306 df-2 11364 df-3 11365 df-n0 11560 df-xnn0 11630 df-z 11644 df-uz 11905 df-q 12008 df-rp 12047 df-fz 12550 df-fl 12817 df-mod 12893 df-seq 13025 df-exp 13084 df-hash 13338 df-cj 14062 df-re 14063 df-im 14064 df-sqrt 14198 df-abs 14199 df-dvds 15204 df-gcd 15436 df-prm 15604 df-pc 15759

This theorem is referenced by: prmreclem3 15839

W3C validator