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

Theorem prmreclem2 15405
Description: Lemma for prmrec 15410. 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.
StepHypRef Expression
1 ovex 6555 . . . 4 ({0, 1} ↑𝑚 (1...𝐾)) ∈ V
2 fveq2 6088 . . . . . . . 8 (𝑥 = 𝑦 → (𝑄𝑥) = (𝑄𝑦))
32eqeq1d 2611 . . . . . . 7 (𝑥 = 𝑦 → ((𝑄𝑥) = 1 ↔ (𝑄𝑦) = 1))
43elrab 3330 . . . . . 6 (𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ↔ (𝑦𝑀 ∧ (𝑄𝑦) = 1))
5 prmrec.4 . . . . . . . . . . . . . . . . . . . 20 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
6 ssrab2 3649 . . . . . . . . . . . . . . . . . . . 20 {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ⊆ (1...𝑁)
75, 6eqsstri 3597 . . . . . . . . . . . . . . . . . . 19 𝑀 ⊆ (1...𝑁)
8 simprl 789 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → 𝑦𝑀)
98ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦𝑀)
107, 9sseldi 3565 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ (1...𝑁))
11 elfznn 12196 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
1210, 11syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℕ)
13 simpr 475 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
14 prmuz2 15192 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ‘2))
1513, 14syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ (ℤ‘2))
16 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
1716prmreclem1 15404 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
1817simp3d 1067 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2))))
1912, 15, 18sylc 62 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
20 simprr 791 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → (𝑄𝑦) = 1)
2120ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑄𝑦) = 1)
2221oveq1d 6542 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄𝑦)↑2) = (1↑2))
23 sq1 12775 . . . . . . . . . . . . . . . . . . . . 21 (1↑2) = 1
2422, 23syl6eq 2659 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄𝑦)↑2) = 1)
2524oveq2d 6543 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄𝑦)↑2)) = (𝑦 / 1))
2612nncnd 10883 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℂ)
2726div1d 10642 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / 1) = 𝑦)
2825, 27eqtrd 2643 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄𝑦)↑2)) = 𝑦)
2928breq2d 4589 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ↔ (𝑛↑2) ∥ 𝑦))
3012nnzd 11313 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℤ)
31 2nn0 11156 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ0
3231a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 2 ∈ ℕ0)
33 pcdvdsb 15357 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 2 ∈ ℕ0) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
3413, 30, 32, 33syl3anc 1317 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
3529, 34bitr4d 269 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ↔ 2 ≤ (𝑛 pCnt 𝑦)))
3619, 35mtbid 312 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ 2 ≤ (𝑛 pCnt 𝑦))
3713, 12pccld 15339 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℕ0)
3837nn0red 11199 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℝ)
39 2re 10937 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
40 ltnle 9968 . . . . . . . . . . . . . . . 16 (((𝑛 pCnt 𝑦) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
4138, 39, 40sylancl 692 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
4236, 41mpbird 245 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < 2)
43 df-2 10926 . . . . . . . . . . . . . 14 2 = (1 + 1)
4442, 43syl6breq 4618 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < (1 + 1))
4537nn0zd 11312 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℤ)
46 1z 11240 . . . . . . . . . . . . . 14 1 ∈ ℤ
47 zleltp1 11261 . . . . . . . . . . . . . 14 (((𝑛 pCnt 𝑦) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
4845, 46, 47sylancl 692 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
4944, 48mpbird 245 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ≤ 1)
50 nn0uz 11554 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
5137, 50syl6eleq 2697 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (ℤ‘0))
52 elfz5 12160 . . . . . . . . . . . . 13 (((𝑛 pCnt 𝑦) ∈ (ℤ‘0) ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
5351, 46, 52sylancl 692 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
5449, 53mpbird 245 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (0...1))
55 0z 11221 . . . . . . . . . . . . 13 0 ∈ ℤ
56 fzpr 12221 . . . . . . . . . . . . 13 (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
5755, 56ax-mp 5 . . . . . . . . . . . 12 (0...(0 + 1)) = {0, (0 + 1)}
58 1e0p1 11384 . . . . . . . . . . . . 13 1 = (0 + 1)
5958oveq2i 6538 . . . . . . . . . . . 12 (0...1) = (0...(0 + 1))
6058preq2i 4215 . . . . . . . . . . . 12 {0, 1} = {0, (0 + 1)}
6157, 59, 603eqtr4i 2641 . . . . . . . . . . 11 (0...1) = {0, 1}
6254, 61syl6eleq 2697 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ {0, 1})
63 c0ex 9890 . . . . . . . . . . . 12 0 ∈ V
6463prid1 4240 . . . . . . . . . . 11 0 ∈ {0, 1}
6564a1i 11 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ ¬ 𝑛 ∈ ℙ) → 0 ∈ {0, 1})
6662, 65ifclda 4069 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ {0, 1})
67 eqid 2609 . . . . . . . . 9 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))
6866, 67fmptd 6277 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
69 prex 4831 . . . . . . . . 9 {0, 1} ∈ V
70 ovex 6555 . . . . . . . . 9 (1...𝐾) ∈ V
7169, 70elmap 7749 . . . . . . . 8 ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑𝑚 (1...𝐾)) ↔ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
7268, 71sylibr 222 . . . . . . 7 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑𝑚 (1...𝐾)))
7372ex 448 . . . . . 6 (𝜑 → ((𝑦𝑀 ∧ (𝑄𝑦) = 1) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑𝑚 (1...𝐾))))
744, 73syl5bi 230 . . . . 5 (𝜑 → (𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑𝑚 (1...𝐾))))
75 fveq2 6088 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑄𝑥) = (𝑄𝑧))
7675eqeq1d 2611 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑄𝑥) = 1 ↔ (𝑄𝑧) = 1))
7776elrab 3330 . . . . . . 7 (𝑧 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ↔ (𝑧𝑀 ∧ (𝑄𝑧) = 1))
784, 77anbi12i 728 . . . . . 6 ((𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∧ 𝑧 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1}) ↔ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1)))
79 ovex 6555 . . . . . . . . . . . 12 (𝑛 pCnt 𝑦) ∈ V
8079, 63ifex 4105 . . . . . . . . . . 11 if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ V
8180, 67fnmpti 5921 . . . . . . . . . 10 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) Fn (1...𝐾)
82 ovex 6555 . . . . . . . . . . . 12 (𝑛 pCnt 𝑧) ∈ V
8382, 63ifex 4105 . . . . . . . . . . 11 if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) ∈ V
84 eqid 2609 . . . . . . . . . . 11 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))
8583, 84fnmpti 5921 . . . . . . . . . 10 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) Fn (1...𝐾)
86 eqfnfv 6204 . . . . . . . . . 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))‘𝑝)))
8781, 85, 86mp2an 703 . . . . . . . . 9 ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝))
88 eleq1 2675 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
89 oveq1 6534 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → (𝑛 pCnt 𝑦) = (𝑝 pCnt 𝑦))
9088, 89ifbieq1d 4058 . . . . . . . . . . . 12 (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
91 ovex 6555 . . . . . . . . . . . . 13 (𝑝 pCnt 𝑦) ∈ V
9291, 63ifex 4105 . . . . . . . . . . . 12 if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) ∈ V
9390, 67, 92fvmpt 6176 . . . . . . . . . . 11 (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
94 oveq1 6534 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → (𝑛 pCnt 𝑧) = (𝑝 pCnt 𝑧))
9588, 94ifbieq1d 4058 . . . . . . . . . . . 12 (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
96 ovex 6555 . . . . . . . . . . . . 13 (𝑝 pCnt 𝑧) ∈ V
9796, 63ifex 4105 . . . . . . . . . . . 12 if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∈ V
9895, 84, 97fvmpt 6176 . . . . . . . . . . 11 (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
9993, 98eqeq12d 2624 . . . . . . . . . 10 (𝑝 ∈ (1...𝐾) → (((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
10099ralbiia 2961 . . . . . . . . 9 (∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
10187, 100bitri 262 . . . . . . . 8 ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
102 simprll 797 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑦𝑀)
103 breq2 4581 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 → (𝑝𝑛𝑝𝑦))
104103notbid 306 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑦 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑦))
105104ralbidv 2968 . . . . . . . . . . . . . . 15 (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
106105, 5elrab2 3332 . . . . . . . . . . . . . 14 (𝑦𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
107106simprbi 478 . . . . . . . . . . . . 13 (𝑦𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
108102, 107syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
109 simprrl 799 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑧𝑀)
110 breq2 4581 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑧 → (𝑝𝑛𝑝𝑧))
111110notbid 306 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑧 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑧))
112111ralbidv 2968 . . . . . . . . . . . . . . 15 (𝑛 = 𝑧 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧))
113112, 5elrab2 3332 . . . . . . . . . . . . . 14 (𝑧𝑀 ↔ (𝑧 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧))
114113simprbi 478 . . . . . . . . . . . . 13 (𝑧𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧)
115109, 114syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧)
116 r19.26 3045 . . . . . . . . . . . . 13 (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧) ↔ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧))
117 eldifi 3693 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
118 fz1ssnn 12198 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) ⊆ ℕ
1197, 118sstri 3576 . . . . . . . . . . . . . . . . . 18 𝑀 ⊆ ℕ
120119, 102sseldi 3565 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑦 ∈ ℕ)
121 pceq0 15359 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝𝑦))
122117, 120, 121syl2anr 493 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝𝑦))
123119, 109sseldi 3565 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑧 ∈ ℕ)
124 pceq0 15359 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℙ ∧ 𝑧 ∈ ℕ) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝𝑧))
125117, 123, 124syl2anr 493 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝𝑧))
126122, 125anbi12d 742 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) ↔ (¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧)))
127 eqtr3 2630 . . . . . . . . . . . . . . 15 (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
128126, 127syl6bir 242 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
129128ralimdva 2944 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
130116, 129syl5bir 231 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ((∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
131108, 115, 130mp2and 710 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
132131biantrud 526 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))))
133 incom 3766 . . . . . . . . . . . . . . 15 (ℙ ∩ (1...𝐾)) = ((1...𝐾) ∩ ℙ)
134133uneq1i 3724 . . . . . . . . . . . . . 14 ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ))
135 inundif 3997 . . . . . . . . . . . . . 14 (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
136134, 135eqtri 2631 . . . . . . . . . . . . 13 ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
137136raleqi 3118 . . . . . . . . . . . 12 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
138 ralunb 3755 . . . . . . . . . . . 12 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
139137, 138bitr3i 264 . . . . . . . . . . 11 (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
140 eldifn 3694 . . . . . . . . . . . . . . 15 (𝑝 ∈ ((1...𝐾) ∖ ℙ) → ¬ 𝑝 ∈ ℙ)
141 iffalse 4044 . . . . . . . . . . . . . . . 16 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = 0)
142 iffalse 4044 . . . . . . . . . . . . . . . 16 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = 0)
143141, 142eqtr4d 2646 . . . . . . . . . . . . . . 15 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
144140, 143syl 17 . . . . . . . . . . . . . 14 (𝑝 ∈ ((1...𝐾) ∖ ℙ) → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
145144rgen 2905 . . . . . . . . . . . . 13 𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)
146145biantru 524 . . . . . . . . . . . 12 (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
147 elinel1 3760 . . . . . . . . . . . . . 14 (𝑝 ∈ (ℙ ∩ (1...𝐾)) → 𝑝 ∈ ℙ)
148 iftrue 4041 . . . . . . . . . . . . . . 15 (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = (𝑝 pCnt 𝑦))
149 iftrue 4041 . . . . . . . . . . . . . . 15 (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = (𝑝 pCnt 𝑧))
150148, 149eqeq12d 2624 . . . . . . . . . . . . . 14 (𝑝 ∈ ℙ → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
151147, 150syl 17 . . . . . . . . . . . . 13 (𝑝 ∈ (ℙ ∩ (1...𝐾)) → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
152151ralbiia 2961 . . . . . . . . . . . 12 (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
153146, 152bitr3i 264 . . . . . . . . . . 11 ((∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
154139, 153bitri 262 . . . . . . . . . 10 (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
155 inundif 3997 . . . . . . . . . . . 12 ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾))) = ℙ
156155raleqi 3118 . . . . . . . . . . 11 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
157 ralunb 3755 . . . . . . . . . . 11 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
158156, 157bitr3i 264 . . . . . . . . . 10 (∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
159132, 154, 1583bitr4g 301 . . . . . . . . 9 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
160120nnnn0d 11198 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑦 ∈ ℕ0)
161123nnnn0d 11198 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑧 ∈ ℕ0)
162 pc11 15368 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑧 ∈ ℕ0) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
163160, 161, 162syl2anc 690 . . . . . . . . 9 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
164159, 163bitr4d 269 . . . . . . . 8 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ 𝑦 = 𝑧))
165101, 164syl5bb 270 . . . . . . 7 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧))
166165ex 448 . . . . . 6 (𝜑 → (((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1)) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
16778, 166syl5bi 230 . . . . 5 (𝜑 → ((𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∧ 𝑧 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1}) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
16874, 167dom2d 7859 . . . 4 (𝜑 → (({0, 1} ↑𝑚 (1...𝐾)) ∈ V → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑𝑚 (1...𝐾))))
1691, 168mpi 20 . . 3 (𝜑 → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑𝑚 (1...𝐾)))
170 fzfi 12588 . . . . . . 7 (1...𝑁) ∈ Fin
171 ssfi 8042 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ⊆ (1...𝑁)) → {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ∈ Fin)
172170, 6, 171mp2an 703 . . . . . 6 {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ∈ Fin
1735, 172eqeltri 2683 . . . . 5 𝑀 ∈ Fin
174 ssrab2 3649 . . . . 5 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀
175 ssfi 8042 . . . . 5 ((𝑀 ∈ Fin ∧ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀) → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin)
176173, 174, 175mp2an 703 . . . 4 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin
177 prfi 8097 . . . . 5 {0, 1} ∈ Fin
178 fzfid 12589 . . . . 5 (𝜑 → (1...𝐾) ∈ Fin)
179 mapfi 8122 . . . . 5 (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → ({0, 1} ↑𝑚 (1...𝐾)) ∈ Fin)
180177, 178, 179sylancr 693 . . . 4 (𝜑 → ({0, 1} ↑𝑚 (1...𝐾)) ∈ Fin)
181 hashdom 12981 . . . 4 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ ({0, 1} ↑𝑚 (1...𝐾)) ∈ Fin) → ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (#‘({0, 1} ↑𝑚 (1...𝐾))) ↔ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑𝑚 (1...𝐾))))
182176, 180, 181sylancr 693 . . 3 (𝜑 → ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (#‘({0, 1} ↑𝑚 (1...𝐾))) ↔ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑𝑚 (1...𝐾))))
183169, 182mpbird 245 . 2 (𝜑 → (#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (#‘({0, 1} ↑𝑚 (1...𝐾))))
184 hashmap 13034 . . . 4 (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → (#‘({0, 1} ↑𝑚 (1...𝐾))) = ((#‘{0, 1})↑(#‘(1...𝐾))))
185177, 178, 184sylancr 693 . . 3 (𝜑 → (#‘({0, 1} ↑𝑚 (1...𝐾))) = ((#‘{0, 1})↑(#‘(1...𝐾))))
186 prhash2ex 13000 . . . . 5 (#‘{0, 1}) = 2
187186a1i 11 . . . 4 (𝜑 → (#‘{0, 1}) = 2)
188 prmrec.2 . . . . . 6 (𝜑𝐾 ∈ ℕ)
189188nnnn0d 11198 . . . . 5 (𝜑𝐾 ∈ ℕ0)
190 hashfz1 12948 . . . . 5 (𝐾 ∈ ℕ0 → (#‘(1...𝐾)) = 𝐾)
191189, 190syl 17 . . . 4 (𝜑 → (#‘(1...𝐾)) = 𝐾)
192187, 191oveq12d 6545 . . 3 (𝜑 → ((#‘{0, 1})↑(#‘(1...𝐾))) = (2↑𝐾))
193185, 192eqtrd 2643 . 2 (𝜑 → (#‘({0, 1} ↑𝑚 (1...𝐾))) = (2↑𝐾))
194183, 193breqtrd 4603 1 (𝜑 → (#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (2↑𝐾))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895  {crab 2899  Vcvv 3172  cdif 3536  cun 3537  cin 3538  wss 3539  ifcif 4035  {cpr 4126   class class class wbr 4577  cmpt 4637   Fn wfn 5785  wf 5786  cfv 5790  (class class class)co 6527  𝑚 cmap 7721  cdom 7816  Fincfn 7818  supcsup 8206  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   < clt 9930  cle 9931   / cdiv 10533  cn 10867  2c2 10917  0cn0 11139  cz 11210  cuz 11519  ...cfz 12152  cexp 12677  #chash 12934  cdvds 14767  cprime 15169   pCnt cpc 15325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-2o 7425  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-sup 8208  df-inf 8209  df-card 8625  df-cda 8850  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-n0 11140  df-z 11211  df-uz 11520  df-q 11621  df-rp 11665  df-fz 12153  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-hash 12935  df-cj 13633  df-re 13634  df-im 13635  df-sqrt 13769  df-abs 13770  df-dvds 14768  df-gcd 15001  df-prm 15170  df-pc 15326
This theorem is referenced by:  prmreclem3  15406
  Copyright terms: Public domain W3C validator