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

Theorem prmreclem2 16263
 Description: Lemma for prmrec 16268. 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 7178 . . . 4 ({0, 1} ↑m (1...𝐾)) ∈ V
2 fveqeq2 6664 . . . . . . 7 (𝑥 = 𝑦 → ((𝑄𝑥) = 1 ↔ (𝑄𝑦) = 1))
32elrab 3630 . . . . . 6 (𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ↔ (𝑦𝑀 ∧ (𝑄𝑦) = 1))
4 prmrec.4 . . . . . . . . . . . . . . . . . . . 20 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
54ssrab3 4011 . . . . . . . . . . . . . . . . . . 19 𝑀 ⊆ (1...𝑁)
6 simprl 770 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → 𝑦𝑀)
76ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦𝑀)
85, 7sseldi 3915 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ (1...𝑁))
9 elfznn 12951 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
108, 9syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℕ)
11 simpr 488 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ ℙ)
12 prmuz2 16050 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℙ → 𝑛 ∈ (ℤ‘2))
1311, 12syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑛 ∈ (ℤ‘2))
14 prmreclem2.5 . . . . . . . . . . . . . . . . . . 19 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
1514prmreclem1 16262 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → ((𝑄𝑦) ∈ ℕ ∧ ((𝑄𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))))
1615simp3d 1141 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑛 ∈ (ℤ‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2))))
1710, 13, 16sylc 65 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)))
18 simprr 772 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → (𝑄𝑦) = 1)
1918ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑄𝑦) = 1)
2019oveq1d 7160 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄𝑦)↑2) = (1↑2))
21 sq1 13574 . . . . . . . . . . . . . . . . . . . . 21 (1↑2) = 1
2220, 21eqtrdi 2849 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑄𝑦)↑2) = 1)
2322oveq2d 7161 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄𝑦)↑2)) = (𝑦 / 1))
2410nncnd 11659 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℂ)
2524div1d 11415 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / 1) = 𝑦)
2623, 25eqtrd 2833 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑦 / ((𝑄𝑦)↑2)) = 𝑦)
2726breq2d 5046 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ↔ (𝑛↑2) ∥ 𝑦))
2810nnzd 12094 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 𝑦 ∈ ℤ)
29 2nn0 11920 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ0
3029a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → 2 ∈ ℕ0)
31 pcdvdsb 16215 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ 2 ∈ ℕ0) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
3211, 28, 30, 31syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (2 ≤ (𝑛 pCnt 𝑦) ↔ (𝑛↑2) ∥ 𝑦))
3327, 32bitr4d 285 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛↑2) ∥ (𝑦 / ((𝑄𝑦)↑2)) ↔ 2 ≤ (𝑛 pCnt 𝑦)))
3417, 33mtbid 327 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ¬ 2 ≤ (𝑛 pCnt 𝑦))
3511, 10pccld 16197 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℕ0)
3635nn0red 11964 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℝ)
37 2re 11717 . . . . . . . . . . . . . . . 16 2 ∈ ℝ
38 ltnle 10727 . . . . . . . . . . . . . . . 16 (((𝑛 pCnt 𝑦) ∈ ℝ ∧ 2 ∈ ℝ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
3936, 37, 38sylancl 589 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) < 2 ↔ ¬ 2 ≤ (𝑛 pCnt 𝑦)))
4034, 39mpbird 260 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < 2)
41 df-2 11706 . . . . . . . . . . . . . 14 2 = (1 + 1)
4240, 41breqtrdi 5075 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) < (1 + 1))
4335nn0zd 12093 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ ℤ)
44 1z 12020 . . . . . . . . . . . . . 14 1 ∈ ℤ
45 zleltp1 12041 . . . . . . . . . . . . . 14 (((𝑛 pCnt 𝑦) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
4643, 44, 45sylancl 589 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ≤ 1 ↔ (𝑛 pCnt 𝑦) < (1 + 1)))
4742, 46mpbird 260 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ≤ 1)
48 nn0uz 12288 . . . . . . . . . . . . . 14 0 = (ℤ‘0)
4935, 48eleqtrdi 2900 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (ℤ‘0))
50 elfz5 12914 . . . . . . . . . . . . 13 (((𝑛 pCnt 𝑦) ∈ (ℤ‘0) ∧ 1 ∈ ℤ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
5149, 44, 50sylancl 589 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → ((𝑛 pCnt 𝑦) ∈ (0...1) ↔ (𝑛 pCnt 𝑦) ≤ 1))
5247, 51mpbird 260 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ (0...1))
53 0z 12000 . . . . . . . . . . . . 13 0 ∈ ℤ
54 fzpr 12977 . . . . . . . . . . . . 13 (0 ∈ ℤ → (0...(0 + 1)) = {0, (0 + 1)})
5553, 54ax-mp 5 . . . . . . . . . . . 12 (0...(0 + 1)) = {0, (0 + 1)}
56 1e0p1 12148 . . . . . . . . . . . . 13 1 = (0 + 1)
5756oveq2i 7156 . . . . . . . . . . . 12 (0...1) = (0...(0 + 1))
5856preq2i 4636 . . . . . . . . . . . 12 {0, 1} = {0, (0 + 1)}
5955, 57, 583eqtr4i 2831 . . . . . . . . . . 11 (0...1) = {0, 1}
6052, 59eleqtrdi 2900 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt 𝑦) ∈ {0, 1})
61 c0ex 10642 . . . . . . . . . . . 12 0 ∈ V
6261prid1 4661 . . . . . . . . . . 11 0 ∈ {0, 1}
6362a1i 11 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) ∧ ¬ 𝑛 ∈ ℙ) → 0 ∈ {0, 1})
6460, 63ifclda 4462 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) ∧ 𝑛 ∈ (1...𝐾)) → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ {0, 1})
6564fmpttd 6866 . . . . . . . 8 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
66 prex 5302 . . . . . . . . 9 {0, 1} ∈ V
67 ovex 7178 . . . . . . . . 9 (1...𝐾) ∈ V
6866, 67elmap 8436 . . . . . . . 8 ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑m (1...𝐾)) ↔ (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)):(1...𝐾)⟶{0, 1})
6965, 68sylibr 237 . . . . . . 7 ((𝜑 ∧ (𝑦𝑀 ∧ (𝑄𝑦) = 1)) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑m (1...𝐾)))
7069ex 416 . . . . . 6 (𝜑 → ((𝑦𝑀 ∧ (𝑄𝑦) = 1) → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑m (1...𝐾))))
713, 70syl5bi 245 . . . . 5 (𝜑 → (𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} → (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) ∈ ({0, 1} ↑m (1...𝐾))))
72 fveqeq2 6664 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑄𝑥) = 1 ↔ (𝑄𝑧) = 1))
7372elrab 3630 . . . . . . 7 (𝑧 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ↔ (𝑧𝑀 ∧ (𝑄𝑧) = 1))
743, 73anbi12i 629 . . . . . 6 ((𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∧ 𝑧 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1}) ↔ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1)))
75 ovex 7178 . . . . . . . . . . . 12 (𝑛 pCnt 𝑦) ∈ V
7675, 61ifex 4476 . . . . . . . . . . 11 if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) ∈ V
77 eqid 2798 . . . . . . . . . . 11 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))
7876, 77fnmpti 6471 . . . . . . . . . 10 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) Fn (1...𝐾)
79 ovex 7178 . . . . . . . . . . . 12 (𝑛 pCnt 𝑧) ∈ V
8079, 61ifex 4476 . . . . . . . . . . 11 if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) ∈ V
81 eqid 2798 . . . . . . . . . . 11 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))
8280, 81fnmpti 6471 . . . . . . . . . 10 (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) Fn (1...𝐾)
83 eqfnfv 6789 . . . . . . . . . 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))‘𝑝)))
8478, 82, 83mp2an 691 . . . . . . . . 9 ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝))
85 eleq1w 2872 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → (𝑛 ∈ ℙ ↔ 𝑝 ∈ ℙ))
86 oveq1 7152 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → (𝑛 pCnt 𝑦) = (𝑝 pCnt 𝑦))
8785, 86ifbieq1d 4451 . . . . . . . . . . . 12 (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
88 ovex 7178 . . . . . . . . . . . . 13 (𝑝 pCnt 𝑦) ∈ V
8988, 61ifex 4476 . . . . . . . . . . . 12 if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) ∈ V
9087, 77, 89fvmpt 6755 . . . . . . . . . . 11 (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0))
91 oveq1 7152 . . . . . . . . . . . . 13 (𝑛 = 𝑝 → (𝑛 pCnt 𝑧) = (𝑝 pCnt 𝑧))
9285, 91ifbieq1d 4451 . . . . . . . . . . . 12 (𝑛 = 𝑝 → if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
93 ovex 7178 . . . . . . . . . . . . 13 (𝑝 pCnt 𝑧) ∈ V
9493, 61ifex 4476 . . . . . . . . . . . 12 if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∈ V
9592, 81, 94fvmpt 6755 . . . . . . . . . . 11 (𝑝 ∈ (1...𝐾) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
9690, 95eqeq12d 2814 . . . . . . . . . 10 (𝑝 ∈ (1...𝐾) → (((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
9796ralbiia 3132 . . . . . . . . 9 (∀𝑝 ∈ (1...𝐾)((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0))‘𝑝) = ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0))‘𝑝) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
9884, 97bitri 278 . . . . . . . 8 ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
99 simprll 778 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑦𝑀)
100 breq2 5038 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 → (𝑝𝑛𝑝𝑦))
101100notbid 321 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑦 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑦))
102101ralbidv 3162 . . . . . . . . . . . . . . 15 (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
103102, 4elrab2 3633 . . . . . . . . . . . . . 14 (𝑦𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦))
104103simprbi 500 . . . . . . . . . . . . 13 (𝑦𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
10599, 104syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦)
106 simprrl 780 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑧𝑀)
107 breq2 5038 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑧 → (𝑝𝑛𝑝𝑧))
108107notbid 321 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑧 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑧))
109108ralbidv 3162 . . . . . . . . . . . . . . 15 (𝑛 = 𝑧 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧))
110109, 4elrab2 3633 . . . . . . . . . . . . . 14 (𝑧𝑀 ↔ (𝑧 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧))
111110simprbi 500 . . . . . . . . . . . . 13 (𝑧𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧)
112106, 111syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧)
113 r19.26 3137 . . . . . . . . . . . . 13 (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧) ↔ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧))
114 eldifi 4057 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
115 fz1ssnn 12953 . . . . . . . . . . . . . . . . . . 19 (1...𝑁) ⊆ ℕ
1165, 115sstri 3926 . . . . . . . . . . . . . . . . . 18 𝑀 ⊆ ℕ
117116, 99sseldi 3915 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑦 ∈ ℕ)
118 pceq0 16217 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℙ ∧ 𝑦 ∈ ℕ) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝𝑦))
119114, 117, 118syl2anr 599 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑦) = 0 ↔ ¬ 𝑝𝑦))
120116, 106sseldi 3915 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑧 ∈ ℕ)
121 pceq0 16217 . . . . . . . . . . . . . . . . 17 ((𝑝 ∈ ℙ ∧ 𝑧 ∈ ℕ) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝𝑧))
122114, 120, 121syl2anr 599 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 pCnt 𝑧) = 0 ↔ ¬ 𝑝𝑧))
123119, 122anbi12d 633 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) ↔ (¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧)))
124 eqtr3 2820 . . . . . . . . . . . . . . 15 (((𝑝 pCnt 𝑦) = 0 ∧ (𝑝 pCnt 𝑧) = 0) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
125123, 124syl6bir 257 . . . . . . . . . . . . . 14 (((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧) → (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
126125ralimdva 3144 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾))(¬ 𝑝𝑦 ∧ ¬ 𝑝𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
127113, 126syl5bir 246 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ((∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑦 ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑧) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
128105, 112, 127mp2and 698 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
129128biantrud 535 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))))
130 incom 4131 . . . . . . . . . . . . . . 15 (ℙ ∩ (1...𝐾)) = ((1...𝐾) ∩ ℙ)
131130uneq1i 4089 . . . . . . . . . . . . . 14 ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ))
132 inundif 4388 . . . . . . . . . . . . . 14 (((1...𝐾) ∩ ℙ) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
133131, 132eqtri 2821 . . . . . . . . . . . . 13 ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ)) = (1...𝐾)
134133raleqi 3363 . . . . . . . . . . . 12 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
135 ralunb 4121 . . . . . . . . . . . 12 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ ((1...𝐾) ∖ ℙ))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
136134, 135bitr3i 280 . . . . . . . . . . 11 (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
137 eldifn 4058 . . . . . . . . . . . . . . 15 (𝑝 ∈ ((1...𝐾) ∖ ℙ) → ¬ 𝑝 ∈ ℙ)
138 iffalse 4437 . . . . . . . . . . . . . . . 16 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = 0)
139 iffalse 4437 . . . . . . . . . . . . . . . 16 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = 0)
140138, 139eqtr4d 2836 . . . . . . . . . . . . . . 15 𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
141137, 140syl 17 . . . . . . . . . . . . . 14 (𝑝 ∈ ((1...𝐾) ∖ ℙ) → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0))
142141rgen 3116 . . . . . . . . . . . . 13 𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)
143142biantru 533 . . . . . . . . . . . 12 (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)))
144 elinel1 4125 . . . . . . . . . . . . . 14 (𝑝 ∈ (ℙ ∩ (1...𝐾)) → 𝑝 ∈ ℙ)
145 iftrue 4434 . . . . . . . . . . . . . . 15 (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = (𝑝 pCnt 𝑦))
146 iftrue 4434 . . . . . . . . . . . . . . 15 (𝑝 ∈ ℙ → if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) = (𝑝 pCnt 𝑧))
147145, 146eqeq12d 2814 . . . . . . . . . . . . . 14 (𝑝 ∈ ℙ → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
148144, 147syl 17 . . . . . . . . . . . . 13 (𝑝 ∈ (ℙ ∩ (1...𝐾)) → (if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
149148ralbiia 3132 . . . . . . . . . . . 12 (∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
150143, 149bitr3i 280 . . . . . . . . . . 11 ((∀𝑝 ∈ (ℙ ∩ (1...𝐾))if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ∧ ∀𝑝 ∈ ((1...𝐾) ∖ ℙ)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0)) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
151136, 150bitri 278 . . . . . . . . . 10 (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
152 inundif 4388 . . . . . . . . . . . 12 ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾))) = ℙ
153152raleqi 3363 . . . . . . . . . . 11 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧))
154 ralunb 4121 . . . . . . . . . . 11 (∀𝑝 ∈ ((ℙ ∩ (1...𝐾)) ∪ (ℙ ∖ (1...𝐾)))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
155153, 154bitr3i 280 . . . . . . . . . 10 (∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ↔ (∀𝑝 ∈ (ℙ ∩ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾))(𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
156129, 151, 1553bitr4g 317 . . . . . . . . 9 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
157117nnnn0d 11963 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑦 ∈ ℕ0)
158120nnnn0d 11963 . . . . . . . . . 10 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → 𝑧 ∈ ℕ0)
159 pc11 16226 . . . . . . . . . 10 ((𝑦 ∈ ℕ0𝑧 ∈ ℕ0) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
160157, 158, 159syl2anc 587 . . . . . . . . 9 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (𝑦 = 𝑧 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑦) = (𝑝 pCnt 𝑧)))
161156, 160bitr4d 285 . . . . . . . 8 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → (∀𝑝 ∈ (1...𝐾)if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑦), 0) = if(𝑝 ∈ ℙ, (𝑝 pCnt 𝑧), 0) ↔ 𝑦 = 𝑧))
16298, 161syl5bb 286 . . . . . . 7 ((𝜑 ∧ ((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1))) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧))
163162ex 416 . . . . . 6 (𝜑 → (((𝑦𝑀 ∧ (𝑄𝑦) = 1) ∧ (𝑧𝑀 ∧ (𝑄𝑧) = 1)) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
16474, 163syl5bi 245 . . . . 5 (𝜑 → ((𝑦 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∧ 𝑧 ∈ {𝑥𝑀 ∣ (𝑄𝑥) = 1}) → ((𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑦), 0)) = (𝑛 ∈ (1...𝐾) ↦ if(𝑛 ∈ ℙ, (𝑛 pCnt 𝑧), 0)) ↔ 𝑦 = 𝑧)))
16571, 164dom2d 8551 . . . 4 (𝜑 → (({0, 1} ↑m (1...𝐾)) ∈ V → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑m (1...𝐾))))
1661, 165mpi 20 . . 3 (𝜑 → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑m (1...𝐾)))
167 fzfi 13355 . . . . . . 7 (1...𝑁) ∈ Fin
168 ssrab2 4009 . . . . . . 7 {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ⊆ (1...𝑁)
169 ssfi 8740 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ⊆ (1...𝑁)) → {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ∈ Fin)
170167, 168, 169mp2an 691 . . . . . 6 {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ∈ Fin
1714, 170eqeltri 2886 . . . . 5 𝑀 ∈ Fin
172 ssrab2 4009 . . . . 5 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀
173 ssfi 8740 . . . . 5 ((𝑀 ∈ Fin ∧ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ⊆ 𝑀) → {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin)
174171, 172, 173mp2an 691 . . . 4 {𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin
175 prfi 8795 . . . . 5 {0, 1} ∈ Fin
176 fzfid 13356 . . . . 5 (𝜑 → (1...𝐾) ∈ Fin)
177 mapfi 8822 . . . . 5 (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → ({0, 1} ↑m (1...𝐾)) ∈ Fin)
178175, 176, 177sylancr 590 . . . 4 (𝜑 → ({0, 1} ↑m (1...𝐾)) ∈ Fin)
179 hashdom 13756 . . . 4 (({𝑥𝑀 ∣ (𝑄𝑥) = 1} ∈ Fin ∧ ({0, 1} ↑m (1...𝐾)) ∈ Fin) → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (♯‘({0, 1} ↑m (1...𝐾))) ↔ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑m (1...𝐾))))
180174, 178, 179sylancr 590 . . 3 (𝜑 → ((♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (♯‘({0, 1} ↑m (1...𝐾))) ↔ {𝑥𝑀 ∣ (𝑄𝑥) = 1} ≼ ({0, 1} ↑m (1...𝐾))))
181166, 180mpbird 260 . 2 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (♯‘({0, 1} ↑m (1...𝐾))))
182 hashmap 13812 . . . 4 (({0, 1} ∈ Fin ∧ (1...𝐾) ∈ Fin) → (♯‘({0, 1} ↑m (1...𝐾))) = ((♯‘{0, 1})↑(♯‘(1...𝐾))))
183175, 176, 182sylancr 590 . . 3 (𝜑 → (♯‘({0, 1} ↑m (1...𝐾))) = ((♯‘{0, 1})↑(♯‘(1...𝐾))))
184 prhash2ex 13776 . . . . 5 (♯‘{0, 1}) = 2
185184a1i 11 . . . 4 (𝜑 → (♯‘{0, 1}) = 2)
186 prmrec.2 . . . . . 6 (𝜑𝐾 ∈ ℕ)
187186nnnn0d 11963 . . . . 5 (𝜑𝐾 ∈ ℕ0)
188 hashfz1 13722 . . . . 5 (𝐾 ∈ ℕ0 → (♯‘(1...𝐾)) = 𝐾)
189187, 188syl 17 . . . 4 (𝜑 → (♯‘(1...𝐾)) = 𝐾)
190185, 189oveq12d 7163 . . 3 (𝜑 → ((♯‘{0, 1})↑(♯‘(1...𝐾))) = (2↑𝐾))
191183, 190eqtrd 2833 . 2 (𝜑 → (♯‘({0, 1} ↑m (1...𝐾))) = (2↑𝐾))
192181, 191breqtrd 5060 1 (𝜑 → (♯‘{𝑥𝑀 ∣ (𝑄𝑥) = 1}) ≤ (2↑𝐾))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  {crab 3110  Vcvv 3442   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ifcif 4428  {cpr 4530   class class class wbr 5034   ↦ cmpt 5114   Fn wfn 6327  ⟶wf 6328  ‘cfv 6332  (class class class)co 7145   ↑m cmap 8407   ≼ cdom 8508  Fincfn 8510  supcsup 8906  ℝcr 10543  0cc0 10544  1c1 10545   + caddc 10547   < clt 10682   ≤ cle 10683   / cdiv 11304  ℕcn 11643  2c2 11698  ℕ0cn0 11903  ℤcz 11989  ℤ≥cuz 12251  ...cfz 12905  ↑cexp 13445  ♯chash 13706   ∥ cdvds 15619  ℙcprime 16025   pCnt cpc 16183 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621  ax-pre-sup 10622 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-2o 8104  df-oadd 8107  df-er 8290  df-map 8409  df-pm 8410  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-sup 8908  df-inf 8909  df-dju 9332  df-card 9370  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-div 11305  df-nn 11644  df-2 11706  df-3 11707  df-n0 11904  df-xnn0 11976  df-z 11990  df-uz 12252  df-q 12357  df-rp 12398  df-fz 12906  df-fl 13177  df-mod 13253  df-seq 13385  df-exp 13446  df-hash 13707  df-cj 14470  df-re 14471  df-im 14472  df-sqrt 14606  df-abs 14607  df-dvds 15620  df-gcd 15854  df-prm 16026  df-pc 16184 This theorem is referenced by:  prmreclem3  16264
 Copyright terms: Public domain W3C validator