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

Theorem prmreclem5 16958
Description: Lemma for prmrec 16960. Here we show the inequality 𝑁 / 2 < ♯𝑀 by decomposing the set (1...𝑁) into the disjoint union of the set 𝑀 of those numbers that are not divisible by any "large" primes (above 𝐾) and the indexed union over 𝐾 < 𝑘 of the numbers 𝑊𝑘 that divide the prime 𝑘. By prmreclem4 16957 the second of these has size less than 𝑁 times the prime reciprocal series, which is less than 1 / 2 by assumption, we find that the complementary part 𝑀 must be at least 𝑁 / 2 large. (Contributed by Mario Carneiro, 6-Aug-2014.)
Hypotheses
Ref Expression
prmrec.1 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
prmrec.2 (𝜑𝐾 ∈ ℕ)
prmrec.3 (𝜑𝑁 ∈ ℕ)
prmrec.4 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
prmrec.5 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
prmrec.6 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
prmrec.7 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)})
Assertion
Ref Expression
prmreclem5 (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁)))
Distinct variable groups:   𝑘,𝑛,𝑝,𝐹   𝑘,𝐾,𝑛,𝑝   𝑘,𝑀,𝑛,𝑝   𝜑,𝑘,𝑛,𝑝   𝑘,𝑊   𝑘,𝑁,𝑛,𝑝
Allowed substitution hints:   𝑊(𝑛,𝑝)

Proof of Theorem prmreclem5
Dummy variables 𝑟 𝑥 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prmrec.3 . . . 4 (𝜑𝑁 ∈ ℕ)
21nnred 12281 . . 3 (𝜑𝑁 ∈ ℝ)
32rehalfcld 12513 . 2 (𝜑 → (𝑁 / 2) ∈ ℝ)
4 fzfi 14013 . . . . . 6 (1...𝑁) ∈ Fin
5 prmrec.4 . . . . . . 7 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
65ssrab3 4082 . . . . . 6 𝑀 ⊆ (1...𝑁)
7 ssfi 9213 . . . . . 6 (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
84, 6, 7mp2an 692 . . . . 5 𝑀 ∈ Fin
9 hashcl 14395 . . . . 5 (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ0)
108, 9ax-mp 5 . . . 4 (♯‘𝑀) ∈ ℕ0
1110nn0rei 12537 . . 3 (♯‘𝑀) ∈ ℝ
1211a1i 11 . 2 (𝜑 → (♯‘𝑀) ∈ ℝ)
13 2nn 12339 . . . . 5 2 ∈ ℕ
14 prmrec.2 . . . . . 6 (𝜑𝐾 ∈ ℕ)
1514nnnn0d 12587 . . . . 5 (𝜑𝐾 ∈ ℕ0)
16 nnexpcl 14115 . . . . 5 ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (2↑𝐾) ∈ ℕ)
1713, 15, 16sylancr 587 . . . 4 (𝜑 → (2↑𝐾) ∈ ℕ)
1817nnred 12281 . . 3 (𝜑 → (2↑𝐾) ∈ ℝ)
191nnrpd 13075 . . . . 5 (𝜑𝑁 ∈ ℝ+)
2019rpsqrtcld 15450 . . . 4 (𝜑 → (√‘𝑁) ∈ ℝ+)
2120rpred 13077 . . 3 (𝜑 → (√‘𝑁) ∈ ℝ)
2218, 21remulcld 11291 . 2 (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
232recnd 11289 . . . . . 6 (𝜑𝑁 ∈ ℂ)
24232halvesd 12512 . . . . 5 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁)
256a1i 11 . . . . . . . . 9 (𝜑𝑀 ⊆ (1...𝑁))
2614peano2nnd 12283 . . . . . . . . . . . . 13 (𝜑 → (𝐾 + 1) ∈ ℕ)
27 elfzuz 13560 . . . . . . . . . . . . 13 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
28 eluznn 12960 . . . . . . . . . . . . 13 (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
2926, 27, 28syl2an 596 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
30 eleq1w 2824 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
31 breq1 5146 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝𝑛𝑘𝑛))
3230, 31anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑛)))
3332rabbidv 3444 . . . . . . . . . . . . . . 15 (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
34 prmrec.7 . . . . . . . . . . . . . . 15 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)})
35 ovex 7464 . . . . . . . . . . . . . . . 16 (1...𝑁) ∈ V
3635rabex 5339 . . . . . . . . . . . . . . 15 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ∈ V
3733, 34, 36fvmpt 7016 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
3837adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
39 ssrab2 4080 . . . . . . . . . . . . 13 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ⊆ (1...𝑁)
4038, 39eqsstrdi 4028 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) ⊆ (1...𝑁))
4129, 40syldan 591 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊𝑘) ⊆ (1...𝑁))
4241ralrimiva 3146 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
43 iunss 5045 . . . . . . . . . 10 ( 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
4442, 43sylibr 234 . . . . . . . . 9 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
4525, 44unssd 4192 . . . . . . . 8 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ⊆ (1...𝑁))
46 breq1 5146 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑝𝑛𝑞𝑛))
4746notbid 318 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → (¬ 𝑝𝑛 ↔ ¬ 𝑞𝑛))
4847cbvralvw 3237 . . . . . . . . . . . . . 14 (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑛)
49 breq2 5147 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → (𝑞𝑛𝑞𝑥))
5049notbid 318 . . . . . . . . . . . . . . 15 (𝑛 = 𝑥 → (¬ 𝑞𝑛 ↔ ¬ 𝑞𝑥))
5150ralbidv 3178 . . . . . . . . . . . . . 14 (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
5248, 51bitrid 283 . . . . . . . . . . . . 13 (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
5352, 5elrab2 3695 . . . . . . . . . . . 12 (𝑥𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
54 elun1 4182 . . . . . . . . . . . 12 (𝑥𝑀𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
5553, 54sylbir 235 . . . . . . . . . . 11 ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
5655ex 412 . . . . . . . . . 10 (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
5756adantl 481 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
58 dfrex2 3073 . . . . . . . . . 10 (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥)
5914nnzd 12640 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ ℤ)
6059peano2zd 12725 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 + 1) ∈ ℤ)
6160ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 + 1) ∈ ℤ)
621nnzd 12640 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℤ)
6362ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑁 ∈ ℤ)
64 eldifi 4131 . . . . . . . . . . . . . . . 16 (𝑞 ∈ (ℙ ∖ (1...𝐾)) → 𝑞 ∈ ℙ)
6564ad2antrl 728 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℙ)
66 prmz 16712 . . . . . . . . . . . . . . 15 (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
6765, 66syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℤ)
68 eldifn 4132 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ (ℙ ∖ (1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾))
6968ad2antrl 728 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → ¬ 𝑞 ∈ (1...𝐾))
70 prmnn 16711 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
7165, 70syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℕ)
72 nnuz 12921 . . . . . . . . . . . . . . . . . . 19 ℕ = (ℤ‘1)
7371, 72eleqtrdi 2851 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ (ℤ‘1))
7459ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 ∈ ℤ)
75 elfz5 13556 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ (ℤ‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞𝐾))
7673, 74, 75syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞𝐾))
7769, 76mtbid 324 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → ¬ 𝑞𝐾)
7814nnred 12281 . . . . . . . . . . . . . . . . . 18 (𝜑𝐾 ∈ ℝ)
7978ad2antrr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 ∈ ℝ)
8071nnred 12281 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℝ)
8179, 80ltnled 11408 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞𝐾))
8277, 81mpbird 257 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 < 𝑞)
83 zltp1le 12667 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
8474, 67, 83syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
8582, 84mpbid 232 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 + 1) ≤ 𝑞)
86 elfznn 13593 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
8786ad2antlr 727 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ ℕ)
8887nnred 12281 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ ℝ)
892ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑁 ∈ ℝ)
90 simprr 773 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑥)
91 dvdsle 16347 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞𝑥𝑞𝑥))
9267, 87, 91syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞𝑥𝑞𝑥))
9390, 92mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑥)
94 elfzle2 13568 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...𝑁) → 𝑥𝑁)
9594ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥𝑁)
9680, 88, 89, 93, 95letrd 11418 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑁)
9761, 63, 67, 85, 96elfzd 13555 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁))
9849anbi2d 630 . . . . . . . . . . . . . . 15 (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑥)))
99 simplr 769 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (1...𝑁))
10065, 90jca 511 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞𝑥))
10198, 99, 100elrabd 3694 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
102 eleq1w 2824 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ))
103102, 46anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑛)))
104103rabbidv 3444 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
10535rabex 5339 . . . . . . . . . . . . . . . 16 {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)} ∈ V
106104, 34, 105fvmpt 7016 . . . . . . . . . . . . . . 15 (𝑞 ∈ ℕ → (𝑊𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
10771, 106syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑊𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
108101, 107eleqtrrd 2844 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (𝑊𝑞))
109 fveq2 6906 . . . . . . . . . . . . . 14 (𝑘 = 𝑞 → (𝑊𝑘) = (𝑊𝑞))
110109eliuni 4997 . . . . . . . . . . . . 13 ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊𝑞)) → 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
11197, 108, 110syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
112 elun2 4183 . . . . . . . . . . . 12 (𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
113111, 112syl 17 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
114113rexlimdvaa 3156 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
11558, 114biimtrrid 243 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
11657, 115pm2.61d 179 . . . . . . . 8 ((𝜑𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
11745, 116eqelssd 4005 . . . . . . 7 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = (1...𝑁))
118117fveq2d 6910 . . . . . 6 (𝜑 → (♯‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = (♯‘(1...𝑁)))
1191nnnn0d 12587 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
120 hashfz1 14385 . . . . . . 7 (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
121119, 120syl 17 . . . . . 6 (𝜑 → (♯‘(1...𝑁)) = 𝑁)
122118, 121eqtr2d 2778 . . . . 5 (𝜑𝑁 = (♯‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
1238a1i 11 . . . . . 6 (𝜑𝑀 ∈ Fin)
124 ssfi 9213 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁)) → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin)
1254, 44, 124sylancr 587 . . . . . 6 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin)
126 breq1 5146 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝𝑥𝑘𝑥))
127126notbid 318 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑘 → (¬ 𝑝𝑥 ↔ ¬ 𝑘𝑥))
128 breq2 5147 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑥 → (𝑝𝑛𝑝𝑥))
129128notbid 318 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑥 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑥))
130129ralbidv 3178 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥))
131130, 5elrab2 3695 . . . . . . . . . . . . . . . . . 18 (𝑥𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥))
132131simprbi 496 . . . . . . . . . . . . . . . . 17 (𝑥𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥)
133132ad2antlr 727 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥)
134 simprr 773 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ)
135 noel 4338 . . . . . . . . . . . . . . . . . 18 ¬ 𝑘 ∈ ∅
136 simprl 771 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁))
137136biantrud 531 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))))
138 elin 3967 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))
139137, 138bitr4di 289 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁))))
14078ltp1d 12198 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐾 < (𝐾 + 1))
141 fzdisj 13591 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
142140, 141syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
143142ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
144143eleq2d 2827 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅))
145139, 144bitrd 279 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅))
146135, 145mtbiri 327 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾))
147134, 146eldifd 3962 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾)))
148127, 133, 147rspcdva 3623 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘𝑥)
149148expr 456 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘𝑥))
150 imnan 399 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℙ → ¬ 𝑘𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘𝑥))
151149, 150sylib 218 . . . . . . . . . . . . 13 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘𝑥))
15229adantlr 715 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
153152, 37syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
154153eleq2d 2827 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)}))
155 breq2 5147 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑥 → (𝑘𝑛𝑘𝑥))
156155anbi2d 630 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
157156elrab 3692 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
158157simprbi 496 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘𝑥))
159154, 158biimtrdi 253 . . . . . . . . . . . . 13 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊𝑘) → (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
160151, 159mtod 198 . . . . . . . . . . . 12 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊𝑘))
161160nrexdv 3149 . . . . . . . . . . 11 ((𝜑𝑥𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊𝑘))
162 eliun 4995 . . . . . . . . . . 11 (𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊𝑘))
163161, 162sylnibr 329 . . . . . . . . . 10 ((𝜑𝑥𝑀) → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
164163ex 412 . . . . . . . . 9 (𝜑 → (𝑥𝑀 → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
165 imnan 399 . . . . . . . . 9 ((𝑥𝑀 → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ↔ ¬ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
166164, 165sylib 218 . . . . . . . 8 (𝜑 → ¬ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
167 elin 3967 . . . . . . . 8 (𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ↔ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
168166, 167sylnibr 329 . . . . . . 7 (𝜑 → ¬ 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
169168eq0rdv 4407 . . . . . 6 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = ∅)
170 hashun 14421 . . . . . 6 ((𝑀 ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin ∧ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = ∅) → (♯‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = ((♯‘𝑀) + (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
171123, 125, 169, 170syl3anc 1373 . . . . 5 (𝜑 → (♯‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = ((♯‘𝑀) + (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
17224, 122, 1713eqtrd 2781 . . . 4 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((♯‘𝑀) + (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
173 hashcl 14395 . . . . . . 7 ( 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℕ0)
174125, 173syl 17 . . . . . 6 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℕ0)
175174nn0red 12588 . . . . 5 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℝ)
176 fzfid 14014 . . . . . . . 8 (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
17726, 28sylan 580 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
178 nnrecre 12308 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
179 0re 11263 . . . . . . . . . . 11 0 ∈ ℝ
180 ifcl 4571 . . . . . . . . . . 11 (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
181178, 179, 180sylancl 586 . . . . . . . . . 10 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
182177, 181syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
18327, 182sylan2 593 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
184176, 183fsumrecl 15770 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
1852, 184remulcld 11291 . . . . . 6 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
186 prmrec.1 . . . . . . . 8 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
187 prmrec.5 . . . . . . . 8 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
188 prmrec.6 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
189186, 14, 1, 5, 187, 188, 34prmreclem4 16957 . . . . . . 7 (𝜑 → (𝑁 ∈ (ℤ𝐾) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
190 eluz 12892 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (ℤ𝑁) ↔ 𝑁𝐾))
19162, 59, 190syl2anc 584 . . . . . . . . 9 (𝜑 → (𝐾 ∈ (ℤ𝑁) ↔ 𝑁𝐾))
192 nnleltp1 12673 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁𝐾𝑁 < (𝐾 + 1)))
1931, 14, 192syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑁𝐾𝑁 < (𝐾 + 1)))
194 fzn 13580 . . . . . . . . . 10 (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
19560, 62, 194syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
196191, 193, 1953bitrd 305 . . . . . . . 8 (𝜑 → (𝐾 ∈ (ℤ𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅))
197 0le0 12367 . . . . . . . . . 10 0 ≤ 0
19823mul01d 11460 . . . . . . . . . 10 (𝜑 → (𝑁 · 0) = 0)
199197, 198breqtrrid 5181 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑁 · 0))
200 iuneq1 5008 . . . . . . . . . . . . 13 (((𝐾 + 1)...𝑁) = ∅ → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) = 𝑘 ∈ ∅ (𝑊𝑘))
201 0iun 5063 . . . . . . . . . . . . 13 𝑘 ∈ ∅ (𝑊𝑘) = ∅
202200, 201eqtrdi 2793 . . . . . . . . . . . 12 (((𝐾 + 1)...𝑁) = ∅ → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) = ∅)
203202fveq2d 6910 . . . . . . . . . . 11 (((𝐾 + 1)...𝑁) = ∅ → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = (♯‘∅))
204 hash0 14406 . . . . . . . . . . 11 (♯‘∅) = 0
205203, 204eqtrdi 2793 . . . . . . . . . 10 (((𝐾 + 1)...𝑁) = ∅ → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = 0)
206 sumeq1 15725 . . . . . . . . . . . 12 (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
207 sum0 15757 . . . . . . . . . . . 12 Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
208206, 207eqtrdi 2793 . . . . . . . . . . 11 (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
209208oveq2d 7447 . . . . . . . . . 10 (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
210205, 209breq12d 5156 . . . . . . . . 9 (((𝐾 + 1)...𝑁) = ∅ → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0)))
211199, 210syl5ibrcom 247 . . . . . . . 8 (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
212196, 211sylbid 240 . . . . . . 7 (𝜑 → (𝐾 ∈ (ℤ𝑁) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
213 uztric 12902 . . . . . . . 8 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝐾) ∨ 𝐾 ∈ (ℤ𝑁)))
21459, 62, 213syl2anc 584 . . . . . . 7 (𝜑 → (𝑁 ∈ (ℤ𝐾) ∨ 𝐾 ∈ (ℤ𝑁)))
215189, 212, 214mpjaod 861 . . . . . 6 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
216 eqid 2737 . . . . . . . . . 10 (ℤ‘(𝐾 + 1)) = (ℤ‘(𝐾 + 1))
217 eleq1w 2824 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
218 oveq2 7439 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
219217, 218ifbieq1d 4550 . . . . . . . . . . . 12 (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
220 ovex 7464 . . . . . . . . . . . . 13 (1 / 𝑘) ∈ V
221 c0ex 11255 . . . . . . . . . . . . 13 0 ∈ V
222220, 221ifex 4576 . . . . . . . . . . . 12 if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V
223219, 186, 222fvmpt 7016 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (𝐹𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
224177, 223syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → (𝐹𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
225181recnd 11289 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
226223, 225eqeltrd 2841 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝐹𝑘) ∈ ℂ)
227226adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
22872, 26, 227iserex 15693 . . . . . . . . . . 11 (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ))
229187, 228mpbid 232 . . . . . . . . . 10 (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ )
230216, 60, 224, 182, 229isumrecl 15801 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
231 halfre 12480 . . . . . . . . . 10 (1 / 2) ∈ ℝ
232231a1i 11 . . . . . . . . 9 (𝜑 → (1 / 2) ∈ ℝ)
233 fzssuz 13605 . . . . . . . . . . 11 ((𝐾 + 1)...𝑁) ⊆ (ℤ‘(𝐾 + 1))
234233a1i 11 . . . . . . . . . 10 (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (ℤ‘(𝐾 + 1)))
235 nnrp 13046 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
236235rpreccld 13087 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
237236rpge0d 13081 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
238 breq2 5147 . . . . . . . . . . . . 13 ((1 / 𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
239 breq2 5147 . . . . . . . . . . . . 13 (0 = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
240238, 239ifboth 4565 . . . . . . . . . . . 12 ((0 ≤ (1 / 𝑘) ∧ 0 ≤ 0) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
241237, 197, 240sylancl 586 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
242177, 241syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
243216, 60, 176, 234, 224, 182, 242, 229isumless 15881 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
244184, 230, 232, 243, 188lelttrd 11419 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
2451nngt0d 12315 . . . . . . . . 9 (𝜑 → 0 < 𝑁)
246 ltmul2 12118 . . . . . . . . 9 ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ ∧ (1 / 2) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
247184, 232, 2, 245, 246syl112anc 1376 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
248244, 247mpbid 232 . . . . . . 7 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))
249 2cn 12341 . . . . . . . . 9 2 ∈ ℂ
250 2ne0 12370 . . . . . . . . 9 2 ≠ 0
251 divrec 11938 . . . . . . . . 9 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2)))
252249, 250, 251mp3an23 1455 . . . . . . . 8 (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2)))
25323, 252syl 17 . . . . . . 7 (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
254248, 253breqtrrd 5171 . . . . . 6 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2))
255175, 185, 3, 215, 254lelttrd 11419 . . . . 5 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) < (𝑁 / 2))
256175, 3, 12, 255ltadd2dd 11420 . . . 4 (𝜑 → ((♯‘𝑀) + (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) < ((♯‘𝑀) + (𝑁 / 2)))
257172, 256eqbrtrd 5165 . . 3 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2)))
2583, 12, 3ltadd1d 11856 . . 3 (𝜑 → ((𝑁 / 2) < (♯‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2))))
259257, 258mpbird 257 . 2 (𝜑 → (𝑁 / 2) < (♯‘𝑀))
260 oveq1 7438 . . . . . . . 8 (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2))
261260breq1d 5153 . . . . . . 7 (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥))
262261cbvrabv 3447 . . . . . 6 {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥}
263 breq2 5147 . . . . . . 7 (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛))
264263rabbidv 3444 . . . . . 6 (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
265262, 264eqtrid 2789 . . . . 5 (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
266265supeq1d 9486 . . . 4 (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
267266cbvmptv 5255 . . 3 (𝑥 ∈ ℕ ↦ sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < )) = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
268186, 14, 1, 5, 267prmreclem3 16956 . 2 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
2693, 12, 22, 259, 268ltletrd 11421 1 (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  {crab 3436  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333  ifcif 4525   ciun 4991   class class class wbr 5143  cmpt 5225  dom cdm 5685  cfv 6561  (class class class)co 7431  Fincfn 8985  supcsup 9480  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296   / cdiv 11920  cn 12266  2c2 12321  0cn0 12526  cz 12613  cuz 12878  ...cfz 13547  seqcseq 14042  cexp 14102  chash 14369  csqrt 15272  cli 15520  Σcsu 15722  cdvds 16290  cprime 16708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525  df-sum 15723  df-dvds 16291  df-gcd 16532  df-prm 16709  df-pc 16875
This theorem is referenced by:  prmreclem6  16959
  Copyright terms: Public domain W3C validator