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

Theorem prmreclem5 16244
Description: Lemma for prmrec 16246. 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 16243 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 11641 . . 3 (𝜑𝑁 ∈ ℝ)
32rehalfcld 11872 . 2 (𝜑 → (𝑁 / 2) ∈ ℝ)
4 fzfi 13328 . . . . . 6 (1...𝑁) ∈ Fin
5 prmrec.4 . . . . . . 7 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
65ssrab3 4054 . . . . . 6 𝑀 ⊆ (1...𝑁)
7 ssfi 8726 . . . . . 6 (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
84, 6, 7mp2an 688 . . . . 5 𝑀 ∈ Fin
9 hashcl 13705 . . . . 5 (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ0)
108, 9ax-mp 5 . . . 4 (♯‘𝑀) ∈ ℕ0
1110nn0rei 11896 . . 3 (♯‘𝑀) ∈ ℝ
1211a1i 11 . 2 (𝜑 → (♯‘𝑀) ∈ ℝ)
13 2nn 11698 . . . . 5 2 ∈ ℕ
14 prmrec.2 . . . . . 6 (𝜑𝐾 ∈ ℕ)
1514nnnn0d 11943 . . . . 5 (𝜑𝐾 ∈ ℕ0)
16 nnexpcl 13430 . . . . 5 ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (2↑𝐾) ∈ ℕ)
1713, 15, 16sylancr 587 . . . 4 (𝜑 → (2↑𝐾) ∈ ℕ)
1817nnred 11641 . . 3 (𝜑 → (2↑𝐾) ∈ ℝ)
191nnrpd 12417 . . . . 5 (𝜑𝑁 ∈ ℝ+)
2019rpsqrtcld 14759 . . . 4 (𝜑 → (√‘𝑁) ∈ ℝ+)
2120rpred 12419 . . 3 (𝜑 → (√‘𝑁) ∈ ℝ)
2218, 21remulcld 10659 . 2 (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
232recnd 10657 . . . . . 6 (𝜑𝑁 ∈ ℂ)
24232halvesd 11871 . . . . 5 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁)
256a1i 11 . . . . . . . . 9 (𝜑𝑀 ⊆ (1...𝑁))
2614peano2nnd 11643 . . . . . . . . . . . . 13 (𝜑 → (𝐾 + 1) ∈ ℕ)
27 elfzuz 12892 . . . . . . . . . . . . 13 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
28 eluznn 12306 . . . . . . . . . . . . 13 (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
2926, 27, 28syl2an 595 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
30 eleq1w 2892 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
31 breq1 5060 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝𝑛𝑘𝑛))
3230, 31anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑛)))
3332rabbidv 3478 . . . . . . . . . . . . . . 15 (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
34 prmrec.7 . . . . . . . . . . . . . . 15 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)})
35 ovex 7178 . . . . . . . . . . . . . . . 16 (1...𝑁) ∈ V
3635rabex 5226 . . . . . . . . . . . . . . 15 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ∈ V
3733, 34, 36fvmpt 6761 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
3837adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
39 ssrab2 4053 . . . . . . . . . . . . 13 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ⊆ (1...𝑁)
4038, 39eqsstrdi 4018 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) ⊆ (1...𝑁))
4129, 40syldan 591 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊𝑘) ⊆ (1...𝑁))
4241ralrimiva 3179 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
43 iunss 4960 . . . . . . . . . 10 ( 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
4442, 43sylibr 235 . . . . . . . . 9 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
4525, 44unssd 4159 . . . . . . . 8 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ⊆ (1...𝑁))
46 breq1 5060 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → (𝑝𝑛𝑞𝑛))
4746notbid 319 . . . . . . . . . . . . . . 15 (𝑝 = 𝑞 → (¬ 𝑝𝑛 ↔ ¬ 𝑞𝑛))
4847cbvralvw 3447 . . . . . . . . . . . . . 14 (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑛)
49 breq2 5061 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → (𝑞𝑛𝑞𝑥))
5049notbid 319 . . . . . . . . . . . . . . 15 (𝑛 = 𝑥 → (¬ 𝑞𝑛 ↔ ¬ 𝑞𝑥))
5150ralbidv 3194 . . . . . . . . . . . . . 14 (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
5248, 51syl5bb 284 . . . . . . . . . . . . 13 (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
5352, 5elrab2 3680 . . . . . . . . . . . 12 (𝑥𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
54 elun1 4149 . . . . . . . . . . . 12 (𝑥𝑀𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
5553, 54sylbir 236 . . . . . . . . . . 11 ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
5655ex 413 . . . . . . . . . 10 (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
5756adantl 482 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
58 dfrex2 3236 . . . . . . . . . 10 (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥)
59 eldifn 4101 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ (ℙ ∖ (1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾))
6059ad2antrl 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → ¬ 𝑞 ∈ (1...𝐾))
61 eldifi 4100 . . . . . . . . . . . . . . . . . . . . 21 (𝑞 ∈ (ℙ ∖ (1...𝐾)) → 𝑞 ∈ ℙ)
6261ad2antrl 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℙ)
63 prmnn 16006 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
6462, 63syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℕ)
65 nnuz 12269 . . . . . . . . . . . . . . . . . . 19 ℕ = (ℤ‘1)
6664, 65eleqtrdi 2920 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ (ℤ‘1))
6714nnzd 12074 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ ℤ)
6867ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 ∈ ℤ)
69 elfz5 12888 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ (ℤ‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞𝐾))
7066, 68, 69syl2anc 584 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞𝐾))
7160, 70mtbid 325 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → ¬ 𝑞𝐾)
7214nnred 11641 . . . . . . . . . . . . . . . . . 18 (𝜑𝐾 ∈ ℝ)
7372ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 ∈ ℝ)
7464nnred 11641 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℝ)
7573, 74ltnled 10775 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞𝐾))
7671, 75mpbird 258 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 < 𝑞)
77 prmz 16007 . . . . . . . . . . . . . . . . 17 (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
7862, 77syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℤ)
79 zltp1le 12020 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
8068, 78, 79syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
8176, 80mpbid 233 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 + 1) ≤ 𝑞)
82 elfznn 12924 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
8382ad2antlr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ ℕ)
8483nnred 11641 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ ℝ)
852ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑁 ∈ ℝ)
86 simprr 769 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑥)
87 dvdsle 15648 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞𝑥𝑞𝑥))
8878, 83, 87syl2anc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞𝑥𝑞𝑥))
8986, 88mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑥)
90 elfzle2 12899 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...𝑁) → 𝑥𝑁)
9190ad2antlr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥𝑁)
9274, 84, 85, 89, 91letrd 10785 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑁)
9367peano2zd 12078 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 + 1) ∈ ℤ)
9493ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 + 1) ∈ ℤ)
951nnzd 12074 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℤ)
9695ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑁 ∈ ℤ)
97 elfz 12886 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞𝑞𝑁)))
9878, 94, 96, 97syl3anc 1363 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞𝑞𝑁)))
9981, 92, 98mpbir2and 709 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁))
10049anbi2d 628 . . . . . . . . . . . . . . 15 (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑥)))
101 simplr 765 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (1...𝑁))
10262, 86jca 512 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞𝑥))
103100, 101, 102elrabd 3679 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
104 eleq1w 2892 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ))
105104, 46anbi12d 630 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑛)))
106105rabbidv 3478 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
10735rabex 5226 . . . . . . . . . . . . . . . 16 {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)} ∈ V
108106, 34, 107fvmpt 6761 . . . . . . . . . . . . . . 15 (𝑞 ∈ ℕ → (𝑊𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
10964, 108syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑊𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
110103, 109eleqtrrd 2913 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (𝑊𝑞))
111 fveq2 6663 . . . . . . . . . . . . . 14 (𝑘 = 𝑞 → (𝑊𝑘) = (𝑊𝑞))
112111eliuni 4916 . . . . . . . . . . . . 13 ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊𝑞)) → 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
11399, 110, 112syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
114 elun2 4150 . . . . . . . . . . . 12 (𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
115113, 114syl 17 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
116115rexlimdvaa 3282 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
11758, 116syl5bir 244 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
11857, 117pm2.61d 180 . . . . . . . 8 ((𝜑𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
11945, 118eqelssd 3985 . . . . . . 7 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = (1...𝑁))
120119fveq2d 6667 . . . . . 6 (𝜑 → (♯‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = (♯‘(1...𝑁)))
1211nnnn0d 11943 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
122 hashfz1 13694 . . . . . . 7 (𝑁 ∈ ℕ0 → (♯‘(1...𝑁)) = 𝑁)
123121, 122syl 17 . . . . . 6 (𝜑 → (♯‘(1...𝑁)) = 𝑁)
124120, 123eqtr2d 2854 . . . . 5 (𝜑𝑁 = (♯‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
1258a1i 11 . . . . . 6 (𝜑𝑀 ∈ Fin)
126 ssfi 8726 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁)) → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin)
1274, 44, 126sylancr 587 . . . . . 6 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin)
128 breq1 5060 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝𝑥𝑘𝑥))
129128notbid 319 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑘 → (¬ 𝑝𝑥 ↔ ¬ 𝑘𝑥))
130 breq2 5061 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑥 → (𝑝𝑛𝑝𝑥))
131130notbid 319 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑥 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑥))
132131ralbidv 3194 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥))
133132, 5elrab2 3680 . . . . . . . . . . . . . . . . . 18 (𝑥𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥))
134133simprbi 497 . . . . . . . . . . . . . . . . 17 (𝑥𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥)
135134ad2antlr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥)
136 simprr 769 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ)
137 noel 4293 . . . . . . . . . . . . . . . . . 18 ¬ 𝑘 ∈ ∅
138 simprl 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁))
139138biantrud 532 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))))
140 elin 4166 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))
141139, 140syl6bbr 290 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁))))
14272ltp1d 11558 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐾 < (𝐾 + 1))
143 fzdisj 12922 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
144142, 143syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
145144ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
146145eleq2d 2895 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅))
147141, 146bitrd 280 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅))
148137, 147mtbiri 328 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾))
149136, 148eldifd 3944 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾)))
150129, 135, 149rspcdva 3622 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘𝑥)
151150expr 457 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘𝑥))
152 imnan 400 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℙ → ¬ 𝑘𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘𝑥))
153151, 152sylib 219 . . . . . . . . . . . . 13 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘𝑥))
15429adantlr 711 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
155154, 37syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
156155eleq2d 2895 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)}))
157 breq2 5061 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑥 → (𝑘𝑛𝑘𝑥))
158157anbi2d 628 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
159158elrab 3677 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
160159simprbi 497 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘𝑥))
161156, 160syl6bi 254 . . . . . . . . . . . . 13 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊𝑘) → (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
162153, 161mtod 199 . . . . . . . . . . . 12 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊𝑘))
163162nrexdv 3267 . . . . . . . . . . 11 ((𝜑𝑥𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊𝑘))
164 eliun 4914 . . . . . . . . . . 11 (𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊𝑘))
165163, 164sylnibr 330 . . . . . . . . . 10 ((𝜑𝑥𝑀) → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
166165ex 413 . . . . . . . . 9 (𝜑 → (𝑥𝑀 → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
167 imnan 400 . . . . . . . . 9 ((𝑥𝑀 → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ↔ ¬ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
168166, 167sylib 219 . . . . . . . 8 (𝜑 → ¬ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
169 elin 4166 . . . . . . . 8 (𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ↔ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
170168, 169sylnibr 330 . . . . . . 7 (𝜑 → ¬ 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
171170eq0rdv 4354 . . . . . 6 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = ∅)
172 hashun 13731 . . . . . 6 ((𝑀 ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin ∧ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = ∅) → (♯‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = ((♯‘𝑀) + (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
173125, 127, 171, 172syl3anc 1363 . . . . 5 (𝜑 → (♯‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = ((♯‘𝑀) + (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
17424, 124, 1733eqtrd 2857 . . . 4 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((♯‘𝑀) + (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
175 hashcl 13705 . . . . . . 7 ( 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℕ0)
176127, 175syl 17 . . . . . 6 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℕ0)
177176nn0red 11944 . . . . 5 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℝ)
178 fzfid 13329 . . . . . . . 8 (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
17926, 28sylan 580 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
180 nnrecre 11667 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
181 0re 10631 . . . . . . . . . . 11 0 ∈ ℝ
182 ifcl 4507 . . . . . . . . . . 11 (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
183180, 181, 182sylancl 586 . . . . . . . . . 10 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
184179, 183syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
18527, 184sylan2 592 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
186178, 185fsumrecl 15079 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
1872, 186remulcld 10659 . . . . . 6 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
188 prmrec.1 . . . . . . . 8 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
189 prmrec.5 . . . . . . . 8 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
190 prmrec.6 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
191188, 14, 1, 5, 189, 190, 34prmreclem4 16243 . . . . . . 7 (𝜑 → (𝑁 ∈ (ℤ𝐾) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
192 eluz 12245 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (ℤ𝑁) ↔ 𝑁𝐾))
19395, 67, 192syl2anc 584 . . . . . . . . 9 (𝜑 → (𝐾 ∈ (ℤ𝑁) ↔ 𝑁𝐾))
194 nnleltp1 12025 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁𝐾𝑁 < (𝐾 + 1)))
1951, 14, 194syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑁𝐾𝑁 < (𝐾 + 1)))
196 fzn 12911 . . . . . . . . . 10 (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
19793, 95, 196syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
198193, 195, 1973bitrd 306 . . . . . . . 8 (𝜑 → (𝐾 ∈ (ℤ𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅))
199 0le0 11726 . . . . . . . . . 10 0 ≤ 0
20023mul01d 10827 . . . . . . . . . 10 (𝜑 → (𝑁 · 0) = 0)
201199, 200breqtrrid 5095 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑁 · 0))
202 iuneq1 4926 . . . . . . . . . . . . 13 (((𝐾 + 1)...𝑁) = ∅ → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) = 𝑘 ∈ ∅ (𝑊𝑘))
203 0iun 4977 . . . . . . . . . . . . 13 𝑘 ∈ ∅ (𝑊𝑘) = ∅
204202, 203syl6eq 2869 . . . . . . . . . . . 12 (((𝐾 + 1)...𝑁) = ∅ → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) = ∅)
205204fveq2d 6667 . . . . . . . . . . 11 (((𝐾 + 1)...𝑁) = ∅ → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = (♯‘∅))
206 hash0 13716 . . . . . . . . . . 11 (♯‘∅) = 0
207205, 206syl6eq 2869 . . . . . . . . . 10 (((𝐾 + 1)...𝑁) = ∅ → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = 0)
208 sumeq1 15033 . . . . . . . . . . . 12 (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
209 sum0 15066 . . . . . . . . . . . 12 Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
210208, 209syl6eq 2869 . . . . . . . . . . 11 (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
211210oveq2d 7161 . . . . . . . . . 10 (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
212207, 211breq12d 5070 . . . . . . . . 9 (((𝐾 + 1)...𝑁) = ∅ → ((♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0)))
213201, 212syl5ibrcom 248 . . . . . . . 8 (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
214198, 213sylbid 241 . . . . . . 7 (𝜑 → (𝐾 ∈ (ℤ𝑁) → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
215 uztric 12254 . . . . . . . 8 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝐾) ∨ 𝐾 ∈ (ℤ𝑁)))
21667, 95, 215syl2anc 584 . . . . . . 7 (𝜑 → (𝑁 ∈ (ℤ𝐾) ∨ 𝐾 ∈ (ℤ𝑁)))
217191, 214, 216mpjaod 854 . . . . . 6 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
218 eqid 2818 . . . . . . . . . 10 (ℤ‘(𝐾 + 1)) = (ℤ‘(𝐾 + 1))
219 eleq1w 2892 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
220 oveq2 7153 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
221219, 220ifbieq1d 4486 . . . . . . . . . . . 12 (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
222 ovex 7178 . . . . . . . . . . . . 13 (1 / 𝑘) ∈ V
223 c0ex 10623 . . . . . . . . . . . . 13 0 ∈ V
224222, 223ifex 4511 . . . . . . . . . . . 12 if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V
225221, 188, 224fvmpt 6761 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (𝐹𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
226179, 225syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → (𝐹𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
227183recnd 10657 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
228225, 227eqeltrd 2910 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝐹𝑘) ∈ ℂ)
229228adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
23065, 26, 229iserex 15001 . . . . . . . . . . 11 (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ))
231189, 230mpbid 233 . . . . . . . . . 10 (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ )
232218, 93, 226, 184, 231isumrecl 15108 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
233 halfre 11839 . . . . . . . . . 10 (1 / 2) ∈ ℝ
234233a1i 11 . . . . . . . . 9 (𝜑 → (1 / 2) ∈ ℝ)
235 fzssuz 12936 . . . . . . . . . . 11 ((𝐾 + 1)...𝑁) ⊆ (ℤ‘(𝐾 + 1))
236235a1i 11 . . . . . . . . . 10 (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (ℤ‘(𝐾 + 1)))
237 nnrp 12388 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
238237rpreccld 12429 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
239238rpge0d 12423 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
240 breq2 5061 . . . . . . . . . . . . 13 ((1 / 𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
241 breq2 5061 . . . . . . . . . . . . 13 (0 = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
242240, 241ifboth 4501 . . . . . . . . . . . 12 ((0 ≤ (1 / 𝑘) ∧ 0 ≤ 0) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
243239, 199, 242sylancl 586 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
244179, 243syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
245218, 93, 178, 236, 226, 184, 244, 231isumless 15188 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
246186, 232, 234, 245, 190lelttrd 10786 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
2471nngt0d 11674 . . . . . . . . 9 (𝜑 → 0 < 𝑁)
248 ltmul2 11479 . . . . . . . . 9 ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ ∧ (1 / 2) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
249186, 234, 2, 247, 248syl112anc 1366 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
250246, 249mpbid 233 . . . . . . 7 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))
251 2cn 11700 . . . . . . . . 9 2 ∈ ℂ
252 2ne0 11729 . . . . . . . . 9 2 ≠ 0
253 divrec 11302 . . . . . . . . 9 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2)))
254251, 252, 253mp3an23 1444 . . . . . . . 8 (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2)))
25523, 254syl 17 . . . . . . 7 (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
256250, 255breqtrrd 5085 . . . . . 6 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2))
257177, 187, 3, 217, 256lelttrd 10786 . . . . 5 (𝜑 → (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) < (𝑁 / 2))
258177, 3, 12, 257ltadd2dd 10787 . . . 4 (𝜑 → ((♯‘𝑀) + (♯‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) < ((♯‘𝑀) + (𝑁 / 2)))
259174, 258eqbrtrd 5079 . . 3 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2)))
2603, 12, 3ltadd1d 11221 . . 3 (𝜑 → ((𝑁 / 2) < (♯‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2))))
261259, 260mpbird 258 . 2 (𝜑 → (𝑁 / 2) < (♯‘𝑀))
262 oveq1 7152 . . . . . . . 8 (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2))
263262breq1d 5067 . . . . . . 7 (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥))
264263cbvrabv 3489 . . . . . 6 {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥}
265 breq2 5061 . . . . . . 7 (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛))
266265rabbidv 3478 . . . . . 6 (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
267264, 266syl5eq 2865 . . . . 5 (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
268267supeq1d 8898 . . . 4 (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
269268cbvmptv 5160 . . 3 (𝑥 ∈ ℕ ↦ sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < )) = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
270188, 14, 1, 5, 269prmreclem3 16242 . 2 (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
2713, 12, 22, 261, 270ltletrd 10788 1 (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  cdif 3930  cun 3931  cin 3932  wss 3933  c0 4288  ifcif 4463   ciun 4910   class class class wbr 5057  cmpt 5137  dom cdm 5548  cfv 6348  (class class class)co 7145  Fincfn 8497  supcsup 8892  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530   < clt 10663  cle 10664   / cdiv 11285  cn 11626  2c2 11680  0cn0 11885  cz 11969  cuz 12231  ...cfz 12880  seqcseq 13357  cexp 13417  chash 13678  csqrt 14580  cli 14829  Σcsu 15030  cdvds 15595  cprime 16003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886  df-xnn0 11956  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-fz 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-hash 13679  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-clim 14833  df-rlim 14834  df-sum 15031  df-dvds 15596  df-gcd 15832  df-prm 16004  df-pc 16162
This theorem is referenced by:  prmreclem6  16245
  Copyright terms: Public domain W3C validator