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

Theorem prmreclem2 15668
Description: Lemma for prmrec 15673. 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 6718 . . . 4 ({0, 1} ↑𝑚 (1...𝐾)) ∈ V
2 fveq2 6229 . . . . . . . 8 (𝑥 = 𝑦 → (𝑄𝑥) = (𝑄𝑦))
32eqeq1d 2653 . . . . . . 7 (𝑥 = 𝑦 → ((𝑄𝑥) = 1 ↔ (𝑄𝑦) = 1))
43elrab 3396 . . . . . 6 (𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ↔ (𝑦𝑀 ∧ (𝑄𝑦) = 1))
5 prmrec.4 . . . . . . . . . . . . . . . . . . . 20 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
6 ssrab2 3720 . . . . . . . . . . . . . . . . . . . 20 {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ⊆ (1...𝑁)
75, 6eqsstri 3668 . . . . . . . . . . . . . . . . . . 19 𝑀 ⊆ (1...𝑁)
8 simprl 809 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → 𝑦𝑀)
98ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦𝑀)
107, 9sseldi 3634 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ (1...𝑁))
11 elfznn 12408 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
1210, 11syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℕ)
13 simpr 476 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
14 prmuz2 15455 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ‘2))
1513, 14syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ (ℤ‘2))
16 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
1716prmreclem1 15667 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
1817simp3d 1095 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2))))
1912, 15, 18sylc 65 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
20 simprr 811 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → (𝑄𝑦) = 1)
2120ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑄𝑦) = 1)
2221oveq1d 6705 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄𝑦)↑2) = (1↑2))
23 sq1 12998 . . . . . . . . . . . . . . . . . . . . 21 (1↑2) = 1
2422, 23syl6eq 2701 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄𝑦)↑2) = 1)
2524oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄𝑦)↑2)) = (𝑦 / 1))
2612nncnd 11074 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℂ)
2726div1d 10831 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / 1) = 𝑦)
2825, 27eqtrd 2685 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄𝑦)↑2)) = 𝑦)
2928breq2d 4697 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ↔ (𝑛↑2) ∥ 𝑦))
3012nnzd 11519 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℤ)
31 2nn0 11347 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ0
3231a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 2 ∈ ℕ0)
33 pcdvdsb 15620 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 2 ∈ ℕ0) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
3413, 30, 32, 33syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
3529, 34bitr4d 271 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ↔ 2 ≤ (𝑛 pCnt 𝑦)))
3619, 35mtbid 313 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ 2 ≤ (𝑛 pCnt 𝑦))
3713, 12pccld 15602 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℕ0)
3837nn0red 11390 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℝ)
39 2re 11128 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
40 ltnle 10155 . . . . . . . . . . . . . . . 16 (((𝑛 pCnt 𝑦) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
4138, 39, 40sylancl 695 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
4236, 41mpbird 247 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < 2)
43 df-2 11117 . . . . . . . . . . . . . 14 2 = (1 + 1)
4442, 43syl6breq 4726 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < (1 + 1))
4537nn0zd 11518 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℤ)
46 1z 11445 . . . . . . . . . . . . . 14 1 ∈ ℤ
47 zleltp1 11466 . . . . . . . . . . . . . 14 (((𝑛 pCnt 𝑦) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
4845, 46, 47sylancl 695 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
4944, 48mpbird 247 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ≤ 1)
50 nn0uz 11760 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
5137, 50syl6eleq 2740 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (ℤ‘0))
52 elfz5 12372 . . . . . . . . . . . . 13 (((𝑛 pCnt 𝑦) ∈ (ℤ‘0) ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
5351, 46, 52sylancl 695 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
5449, 53mpbird 247 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (0...1))
55 0z 11426 . . . . . . . . . . . . 13 0 ∈ ℤ
56 fzpr 12434 . . . . . . . . . . . . 13 (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
5755, 56ax-mp 5 . . . . . . . . . . . 12 (0...(0 + 1)) = {0, (0 + 1)}
58 1e0p1 11590 . . . . . . . . . . . . 13 1 = (0 + 1)
5958oveq2i 6701 . . . . . . . . . . . 12 (0...1) = (0...(0 + 1))
6058preq2i 4304 . . . . . . . . . . . 12 {0, 1} = {0, (0 + 1)}
6157, 59, 603eqtr4i 2683 . . . . . . . . . . 11 (0...1) = {0, 1}
6254, 61syl6eleq 2740 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ {0, 1})
63 c0ex 10072 . . . . . . . . . . . 12 0 ∈ V
6463prid1 4329 . . . . . . . . . . 11 0 ∈ {0, 1}
6564a1i 11 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ ¬ 𝑛 ∈ ℙ) → 0 ∈ {0, 1})
6662, 65ifclda 4153 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ {0, 1})
67 eqid 2651 . . . . . . . . 9 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))
6866, 67fmptd 6425 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
69 prex 4939 . . . . . . . . 9 {0, 1} ∈ V
70 ovex 6718 . . . . . . . . 9 (1...𝐾) ∈ V
7169, 70elmap 7928 . . . . . . . 8 ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑𝑚 (1...𝐾)) ↔ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
7268, 71sylibr 224 . . . . . . 7 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑𝑚 (1...𝐾)))
7372ex 449 . . . . . 6 (𝜑 → ((𝑦𝑀 ∧ (𝑄𝑦) = 1) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑𝑚 (1...𝐾))))
744, 73syl5bi 232 . . . . 5 (𝜑 → (𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑𝑚 (1...𝐾))))
75 fveq2 6229 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑄𝑥) = (𝑄𝑧))
7675eqeq1d 2653 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑄𝑥) = 1 ↔ (𝑄𝑧) = 1))
7776elrab 3396 . . . . . . 7 (𝑧 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ↔ (𝑧𝑀 ∧ (𝑄𝑧) = 1))
784, 77anbi12i 733 . . . . . 6 ((𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∧ 𝑧 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1}) ↔ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1)))
79 ovex 6718 . . . . . . . . . . . 12 (𝑛 pCnt 𝑦) ∈ V
8079, 63ifex 4189 . . . . . . . . . . 11 if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ V
8180, 67fnmpti 6060 . . . . . . . . . 10 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) Fn (1...𝐾)
82 ovex 6718 . . . . . . . . . . . 12 (𝑛 pCnt 𝑧) ∈ V
8382, 63ifex 4189 . . . . . . . . . . 11 if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) ∈ V
84 eqid 2651 . . . . . . . . . . 11 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))
8583, 84fnmpti 6060 . . . . . . . . . 10 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) Fn (1...𝐾)
86 eqfnfv 6351 . . . . . . . . . 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 708 . . . . . . . . 9 ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝))
88 eleq1 2718 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
89 oveq1 6697 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → (𝑛 pCnt 𝑦) = (𝑝 pCnt 𝑦))
9088, 89ifbieq1d 4142 . . . . . . . . . . . 12 (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
91 ovex 6718 . . . . . . . . . . . . 13 (𝑝 pCnt 𝑦) ∈ V
9291, 63ifex 4189 . . . . . . . . . . . 12 if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) ∈ V
9390, 67, 92fvmpt 6321 . . . . . . . . . . 11 (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
94 oveq1 6697 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → (𝑛 pCnt 𝑧) = (𝑝 pCnt 𝑧))
9588, 94ifbieq1d 4142 . . . . . . . . . . . 12 (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
96 ovex 6718 . . . . . . . . . . . . 13 (𝑝 pCnt 𝑧) ∈ V
9796, 63ifex 4189 . . . . . . . . . . . 12 if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∈ V
9895, 84, 97fvmpt 6321 . . . . . . . . . . 11 (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
9993, 98eqeq12d 2666 . . . . . . . . . 10 (𝑝 ∈ (1...𝐾) → (((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
10099ralbiia 3008 . . . . . . . . 9 (∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
10187, 100bitri 264 . . . . . . . 8 ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
102 simprll 819 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑦𝑀)
103 breq2 4689 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 → (𝑝𝑛𝑝𝑦))
104103notbid 307 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑦 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑦))
105104ralbidv 3015 . . . . . . . . . . . . . . 15 (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
106105, 5elrab2 3399 . . . . . . . . . . . . . 14 (𝑦𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
107106simprbi 479 . . . . . . . . . . . . 13 (𝑦𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
108102, 107syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
109 simprrl 821 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑧𝑀)
110 breq2 4689 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑧 → (𝑝𝑛𝑝𝑧))
111110notbid 307 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑧 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑧))
112111ralbidv 3015 . . . . . . . . . . . . . . 15 (𝑛 = 𝑧 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧))
113112, 5elrab2 3399 . . . . . . . . . . . . . 14 (𝑧𝑀 ↔ (𝑧 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧))
114113simprbi 479 . . . . . . . . . . . . 13 (𝑧𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧)
115109, 114syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧)
116 r19.26 3093 . . . . . . . . . . . . 13 (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧) ↔ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧))
117 eldifi 3765 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
118 fz1ssnn 12410 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) ⊆ ℕ
1197, 118sstri 3645 . . . . . . . . . . . . . . . . . 18 𝑀 ⊆ ℕ
120119, 102sseldi 3634 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑦 ∈ ℕ)
121 pceq0 15622 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝𝑦))
122117, 120, 121syl2anr 494 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝𝑦))
123119, 109sseldi 3634 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑧 ∈ ℕ)
124 pceq0 15622 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℙ ∧ 𝑧 ∈ ℕ) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝𝑧))
125117, 123, 124syl2anr 494 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝𝑧))
126122, 125anbi12d 747 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) ↔ (¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧)))
127 eqtr3 2672 . . . . . . . . . . . . . . 15 (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
128126, 127syl6bir 244 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
129128ralimdva 2991 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
130116, 129syl5bir 233 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ((∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
131108, 115, 130mp2and 715 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
132131biantrud 527 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))))
133 incom 3838 . . . . . . . . . . . . . . 15 (ℙ ∩ (1...𝐾)) = ((1...𝐾) ∩ ℙ)
134133uneq1i 3796 . . . . . . . . . . . . . 14 ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ))
135 inundif 4079 . . . . . . . . . . . . . 14 (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
136134, 135eqtri 2673 . . . . . . . . . . . . 13 ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
137136raleqi 3172 . . . . . . . . . . . 12 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
138 ralunb 3827 . . . . . . . . . . . 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 266 . . . . . . . . . . 11 (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
140 eldifn 3766 . . . . . . . . . . . . . . 15 (𝑝 ∈ ((1...𝐾) ∖ ℙ) → ¬ 𝑝 ∈ ℙ)
141 iffalse 4128 . . . . . . . . . . . . . . . 16 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = 0)
142 iffalse 4128 . . . . . . . . . . . . . . . 16 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = 0)
143141, 142eqtr4d 2688 . . . . . . . . . . . . . . 15 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
144140, 143syl 17 . . . . . . . . . . . . . 14 (𝑝 ∈ ((1...𝐾) ∖ ℙ) → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
145144rgen 2951 . . . . . . . . . . . . 13 𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)
146145biantru 525 . . . . . . . . . . . 12 (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
147 elinel1 3832 . . . . . . . . . . . . . 14 (𝑝 ∈ (ℙ ∩ (1...𝐾)) → 𝑝 ∈ ℙ)
148 iftrue 4125 . . . . . . . . . . . . . . 15 (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = (𝑝 pCnt 𝑦))
149 iftrue 4125 . . . . . . . . . . . . . . 15 (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = (𝑝 pCnt 𝑧))
150148, 149eqeq12d 2666 . . . . . . . . . . . . . 14 (𝑝 ∈ ℙ → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
151147, 150syl 17 . . . . . . . . . . . . 13 (𝑝 ∈ (ℙ ∩ (1...𝐾)) → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
152151ralbiia 3008 . . . . . . . . . . . 12 (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
153146, 152bitr3i 266 . . . . . . . . . . 11 ((∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
154139, 153bitri 264 . . . . . . . . . 10 (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
155 inundif 4079 . . . . . . . . . . . 12 ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾))) = ℙ
156155raleqi 3172 . . . . . . . . . . 11 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
157 ralunb 3827 . . . . . . . . . . 11 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
158156, 157bitr3i 266 . . . . . . . . . 10 (∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
159132, 154, 1583bitr4g 303 . . . . . . . . 9 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
160120nnnn0d 11389 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑦 ∈ ℕ0)
161123nnnn0d 11389 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑧 ∈ ℕ0)
162 pc11 15631 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑧 ∈ ℕ0) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
163160, 161, 162syl2anc 694 . . . . . . . . 9 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
164159, 163bitr4d 271 . . . . . . . 8 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ 𝑦 = 𝑧))
165101, 164syl5bb 272 . . . . . . 7 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧))
166165ex 449 . . . . . 6 (𝜑 → (((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1)) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
16778, 166syl5bi 232 . . . . 5 (𝜑 → ((𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∧ 𝑧 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1}) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
16874, 167dom2d 8038 . . . 4 (𝜑 → (({0, 1} ↑𝑚 (1...𝐾)) ∈ V → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑𝑚 (1...𝐾))))
1691, 168mpi 20 . . 3 (𝜑 → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑𝑚 (1...𝐾)))
170 fzfi 12811 . . . . . . 7 (1...𝑁) ∈ Fin
171 ssfi 8221 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ⊆ (1...𝑁)) → {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ∈ Fin)
172170, 6, 171mp2an 708 . . . . . 6 {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ∈ Fin
1735, 172eqeltri 2726 . . . . 5 𝑀 ∈ Fin
174 ssrab2 3720 . . . . 5 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀
175 ssfi 8221 . . . . 5 ((𝑀 ∈ Fin ∧ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀) → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin)
176173, 174, 175mp2an 708 . . . 4 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin
177 prfi 8276 . . . . 5 {0, 1} ∈ Fin
178 fzfid 12812 . . . . 5 (𝜑 → (1...𝐾) ∈ Fin)
179 mapfi 8303 . . . . 5 (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → ({0, 1} ↑𝑚 (1...𝐾)) ∈ Fin)
180177, 178, 179sylancr 696 . . . 4 (𝜑 → ({0, 1} ↑𝑚 (1...𝐾)) ∈ Fin)
181 hashdom 13206 . . . 4 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ ({0, 1} ↑𝑚 (1...𝐾)) ∈ Fin) → ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (#‘({0, 1} ↑𝑚 (1...𝐾))) ↔ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑𝑚 (1...𝐾))))
182176, 180, 181sylancr 696 . . 3 (𝜑 → ((#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (#‘({0, 1} ↑𝑚 (1...𝐾))) ↔ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑𝑚 (1...𝐾))))
183169, 182mpbird 247 . 2 (𝜑 → (#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (#‘({0, 1} ↑𝑚 (1...𝐾))))
184 hashmap 13260 . . . 4 (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → (#‘({0, 1} ↑𝑚 (1...𝐾))) = ((#‘{0, 1})↑(#‘(1...𝐾))))
185177, 178, 184sylancr 696 . . 3 (𝜑 → (#‘({0, 1} ↑𝑚 (1...𝐾))) = ((#‘{0, 1})↑(#‘(1...𝐾))))
186 prhash2ex 13225 . . . . 5 (#‘{0, 1}) = 2
187186a1i 11 . . . 4 (𝜑 → (#‘{0, 1}) = 2)
188 prmrec.2 . . . . . 6 (𝜑𝐾 ∈ ℕ)
189188nnnn0d 11389 . . . . 5 (𝜑𝐾 ∈ ℕ0)
190 hashfz1 13174 . . . . 5 (𝐾 ∈ ℕ0 → (#‘(1...𝐾)) = 𝐾)
191189, 190syl 17 . . . 4 (𝜑 → (#‘(1...𝐾)) = 𝐾)
192187, 191oveq12d 6708 . . 3 (𝜑 → ((#‘{0, 1})↑(#‘(1...𝐾))) = (2↑𝐾))
193185, 192eqtrd 2685 . 2 (𝜑 → (#‘({0, 1} ↑𝑚 (1...𝐾))) = (2↑𝐾))
194183, 193breqtrd 4711 1 (𝜑 → (#‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (2↑𝐾))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941  {crab 2945  Vcvv 3231  cdif 3604  cun 3605  cin 3606  wss 3607  ifcif 4119  {cpr 4212   class class class wbr 4685  cmpt 4762   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  𝑚 cmap 7899  cdom 7995  Fincfn 7997  supcsup 8387  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112  cle 10113   / cdiv 10722  cn 11058  2c2 11108  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  cexp 12900  #chash 13157  cdvds 15027  cprime 15432   pCnt cpc 15588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-fz 12365  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-dvds 15028  df-gcd 15264  df-prm 15433  df-pc 15589
This theorem is referenced by:  prmreclem3  15669
  Copyright terms: Public domain W3C validator