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

Theorem prmreclem5 15567
 Description: Lemma for prmrec 15569. 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 15566 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 10995 . . 3 (𝜑𝑁 ∈ ℝ)
32rehalfcld 11239 . 2 (𝜑 → (𝑁 / 2) ∈ ℝ)
4 fzfi 12727 . . . . . 6 (1...𝑁) ∈ Fin
5 prmrec.4 . . . . . . 7 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
6 ssrab2 3672 . . . . . . 7 {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ⊆ (1...𝑁)
75, 6eqsstri 3620 . . . . . 6 𝑀 ⊆ (1...𝑁)
8 ssfi 8140 . . . . . 6 (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
94, 7, 8mp2an 707 . . . . 5 𝑀 ∈ Fin
10 hashcl 13103 . . . . 5 (𝑀 ∈ Fin → (#‘𝑀) ∈ ℕ0)
119, 10ax-mp 5 . . . 4 (#‘𝑀) ∈ ℕ0
1211nn0rei 11263 . . 3 (#‘𝑀) ∈ ℝ
1312a1i 11 . 2 (𝜑 → (#‘𝑀) ∈ ℝ)
14 2nn 11145 . . . . 5 2 ∈ ℕ
15 prmrec.2 . . . . . 6 (𝜑𝐾 ∈ ℕ)
1615nnnn0d 11311 . . . . 5 (𝜑𝐾 ∈ ℕ0)
17 nnexpcl 12829 . . . . 5 ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (2↑𝐾) ∈ ℕ)
1814, 16, 17sylancr 694 . . . 4 (𝜑 → (2↑𝐾) ∈ ℕ)
1918nnred 10995 . . 3 (𝜑 → (2↑𝐾) ∈ ℝ)
201nnrpd 11830 . . . . 5 (𝜑𝑁 ∈ ℝ+)
2120rpsqrtcld 14100 . . . 4 (𝜑 → (√‘𝑁) ∈ ℝ+)
2221rpred 11832 . . 3 (𝜑 → (√‘𝑁) ∈ ℝ)
2319, 22remulcld 10030 . 2 (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
242recnd 10028 . . . . . 6 (𝜑𝑁 ∈ ℂ)
25242halvesd 11238 . . . . 5 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁)
267a1i 11 . . . . . . . . 9 (𝜑𝑀 ⊆ (1...𝑁))
2715peano2nnd 10997 . . . . . . . . . . . . 13 (𝜑 → (𝐾 + 1) ∈ ℕ)
28 elfzuz 12296 . . . . . . . . . . . . 13 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
29 eluznn 11718 . . . . . . . . . . . . 13 (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
3027, 28, 29syl2an 494 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
31 eleq1 2686 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
32 breq1 4626 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝𝑛𝑘𝑛))
3331, 32anbi12d 746 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑛)))
3433rabbidv 3181 . . . . . . . . . . . . . . 15 (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
35 prmrec.7 . . . . . . . . . . . . . . 15 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)})
36 ovex 6643 . . . . . . . . . . . . . . . 16 (1...𝑁) ∈ V
3736rabex 4783 . . . . . . . . . . . . . . 15 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ∈ V
3834, 35, 37fvmpt 6249 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
3938adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
40 ssrab2 3672 . . . . . . . . . . . . 13 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ⊆ (1...𝑁)
4139, 40syl6eqss 3640 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) ⊆ (1...𝑁))
4230, 41syldan 487 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊𝑘) ⊆ (1...𝑁))
4342ralrimiva 2962 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
44 iunss 4534 . . . . . . . . . 10 ( 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
4543, 44sylibr 224 . . . . . . . . 9 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
4626, 45unssd 3773 . . . . . . . 8 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ⊆ (1...𝑁))
47 breq1 4626 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (𝑝𝑛𝑞𝑛))
4847notbid 308 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → (¬ 𝑝𝑛 ↔ ¬ 𝑞𝑛))
4948cbvralv 3163 . . . . . . . . . . . . . . . 16 (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑛)
50 breq2 4627 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑥 → (𝑞𝑛𝑞𝑥))
5150notbid 308 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑥 → (¬ 𝑞𝑛 ↔ ¬ 𝑞𝑥))
5251ralbidv 2982 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
5349, 52syl5bb 272 . . . . . . . . . . . . . . 15 (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
5453, 5elrab2 3353 . . . . . . . . . . . . . 14 (𝑥𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
55 elun1 3764 . . . . . . . . . . . . . 14 (𝑥𝑀𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
5654, 55sylbir 225 . . . . . . . . . . . . 13 ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
5756ex 450 . . . . . . . . . . . 12 (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
5857adantl 482 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
59 dfrex2 2992 . . . . . . . . . . . 12 (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥)
60 eldifn 3717 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ (ℙ ∖ (1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾))
6160ad2antrl 763 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → ¬ 𝑞 ∈ (1...𝐾))
62 eldifi 3716 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 ∈ (ℙ ∖ (1...𝐾)) → 𝑞 ∈ ℙ)
6362ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℙ)
64 prmnn 15331 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℕ)
66 nnuz 11683 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
6765, 66syl6eleq 2708 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ (ℤ‘1))
6815nnzd 11441 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐾 ∈ ℤ)
6968ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 ∈ ℤ)
70 elfz5 12292 . . . . . . . . . . . . . . . . . . . 20 ((𝑞 ∈ (ℤ‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞𝐾))
7167, 69, 70syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞𝐾))
7261, 71mtbid 314 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → ¬ 𝑞𝐾)
7315nnred 10995 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ ℝ)
7473ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 ∈ ℝ)
7565nnred 10995 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℝ)
7674, 75ltnled 10144 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞𝐾))
7772, 76mpbird 247 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 < 𝑞)
78 prmz 15332 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
7963, 78syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℤ)
80 zltp1le 11387 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
8169, 79, 80syl2anc 692 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
8277, 81mpbid 222 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 + 1) ≤ 𝑞)
83 elfznn 12328 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
8483ad2antlr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ ℕ)
8584nnred 10995 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ ℝ)
862ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑁 ∈ ℝ)
87 simprr 795 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑥)
88 dvdsle 14975 . . . . . . . . . . . . . . . . . . 19 ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞𝑥𝑞𝑥))
8979, 84, 88syl2anc 692 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞𝑥𝑞𝑥))
9087, 89mpd 15 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑥)
91 elfzle2 12303 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑁) → 𝑥𝑁)
9291ad2antlr 762 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥𝑁)
9375, 85, 86, 90, 92letrd 10154 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑁)
9468peano2zd 11445 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐾 + 1) ∈ ℤ)
9594ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 + 1) ∈ ℤ)
961nnzd 11441 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℤ)
9796ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑁 ∈ ℤ)
98 elfz 12290 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞𝑞𝑁)))
9979, 95, 97, 98syl3anc 1323 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞𝑞𝑁)))
10082, 93, 99mpbir2and 956 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁))
101 simplr 791 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (1...𝑁))
10263, 87jca 554 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞𝑥))
10350anbi2d 739 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑥)))
104103elrab 3351 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑞 ∈ ℙ ∧ 𝑞𝑥)))
105101, 102, 104sylanbrc 697 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
106 eleq1 2686 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ))
107106, 47anbi12d 746 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑛)))
108107rabbidv 3181 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
10936rabex 4783 . . . . . . . . . . . . . . . . . 18 {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)} ∈ V
110108, 35, 109fvmpt 6249 . . . . . . . . . . . . . . . . 17 (𝑞 ∈ ℕ → (𝑊𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
11165, 110syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑊𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
112105, 111eleqtrrd 2701 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (𝑊𝑞))
113 fveq2 6158 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑞 → (𝑊𝑘) = (𝑊𝑞))
114113eliuni 4499 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊𝑞)) → 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
115100, 112, 114syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
116 elun2 3765 . . . . . . . . . . . . . 14 (𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
117115, 116syl 17 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
118117rexlimdvaa 3027 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
11959, 118syl5bir 233 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
12058, 119pm2.61d 170 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
121120ex 450 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1...𝑁) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
122121ssrdv 3594 . . . . . . . 8 (𝜑 → (1...𝑁) ⊆ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
12346, 122eqssd 3605 . . . . . . 7 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = (1...𝑁))
124123fveq2d 6162 . . . . . 6 (𝜑 → (#‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = (#‘(1...𝑁)))
1251nnnn0d 11311 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
126 hashfz1 13090 . . . . . . 7 (𝑁 ∈ ℕ0 → (#‘(1...𝑁)) = 𝑁)
127125, 126syl 17 . . . . . 6 (𝜑 → (#‘(1...𝑁)) = 𝑁)
128124, 127eqtr2d 2656 . . . . 5 (𝜑𝑁 = (#‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
1299a1i 11 . . . . . 6 (𝜑𝑀 ∈ Fin)
130 ssfi 8140 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁)) → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin)
1314, 45, 130sylancr 694 . . . . . 6 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin)
132 breq1 4626 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝𝑥𝑘𝑥))
133132notbid 308 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑘 → (¬ 𝑝𝑥 ↔ ¬ 𝑘𝑥))
134 breq2 4627 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑥 → (𝑝𝑛𝑝𝑥))
135134notbid 308 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑥 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑥))
136135ralbidv 2982 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥))
137136, 5elrab2 3353 . . . . . . . . . . . . . . . . . 18 (𝑥𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥))
138137simprbi 480 . . . . . . . . . . . . . . . . 17 (𝑥𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥)
139138ad2antlr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥)
140 simprr 795 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ)
141 noel 3901 . . . . . . . . . . . . . . . . . 18 ¬ 𝑘 ∈ ∅
142 simprl 793 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁))
143142biantrud 528 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))))
144 elin 3780 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))
145143, 144syl6bbr 278 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁))))
14673ltp1d 10914 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐾 < (𝐾 + 1))
147 fzdisj 12326 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
149148ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
150149eleq2d 2684 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅))
151145, 150bitrd 268 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅))
152141, 151mtbiri 317 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾))
153140, 152eldifd 3571 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾)))
154133, 139, 153rspcdva 3305 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘𝑥)
155154expr 642 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘𝑥))
156 imnan 438 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℙ → ¬ 𝑘𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘𝑥))
157155, 156sylib 208 . . . . . . . . . . . . 13 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘𝑥))
15830adantlr 750 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
159158, 38syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
160159eleq2d 2684 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)}))
161 breq2 4627 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑥 → (𝑘𝑛𝑘𝑥))
162161anbi2d 739 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
163162elrab 3351 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
164163simprbi 480 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘𝑥))
165160, 164syl6bi 243 . . . . . . . . . . . . 13 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊𝑘) → (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
166157, 165mtod 189 . . . . . . . . . . . 12 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊𝑘))
167166nrexdv 2997 . . . . . . . . . . 11 ((𝜑𝑥𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊𝑘))
168 eliun 4497 . . . . . . . . . . 11 (𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊𝑘))
169167, 168sylnibr 319 . . . . . . . . . 10 ((𝜑𝑥𝑀) → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
170169ex 450 . . . . . . . . 9 (𝜑 → (𝑥𝑀 → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
171 imnan 438 . . . . . . . . 9 ((𝑥𝑀 → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ↔ ¬ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
172170, 171sylib 208 . . . . . . . 8 (𝜑 → ¬ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
173 elin 3780 . . . . . . . 8 (𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ↔ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
174172, 173sylnibr 319 . . . . . . 7 (𝜑 → ¬ 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
175174eq0rdv 3957 . . . . . 6 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = ∅)
176 hashun 13127 . . . . . 6 ((𝑀 ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin ∧ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = ∅) → (#‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = ((#‘𝑀) + (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
177129, 131, 175, 176syl3anc 1323 . . . . 5 (𝜑 → (#‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = ((#‘𝑀) + (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
17825, 128, 1773eqtrd 2659 . . . 4 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((#‘𝑀) + (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
179 hashcl 13103 . . . . . . 7 ( 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℕ0)
180131, 179syl 17 . . . . . 6 (𝜑 → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℕ0)
181180nn0red 11312 . . . . 5 (𝜑 → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℝ)
182 fzfid 12728 . . . . . . . 8 (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
18327, 29sylan 488 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
184 nnrecre 11017 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
185 0re 10000 . . . . . . . . . . 11 0 ∈ ℝ
186 ifcl 4108 . . . . . . . . . . 11 (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
187184, 185, 186sylancl 693 . . . . . . . . . 10 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
188183, 187syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
18928, 188sylan2 491 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
190182, 189fsumrecl 14414 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
1912, 190remulcld 10030 . . . . . 6 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
192 prmrec.1 . . . . . . . 8 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
193 prmrec.5 . . . . . . . 8 (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
194 prmrec.6 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
195192, 15, 1, 5, 193, 194, 35prmreclem4 15566 . . . . . . 7 (𝜑 → (𝑁 ∈ (ℤ𝐾) → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
196 eluz 11661 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (ℤ𝑁) ↔ 𝑁𝐾))
19796, 68, 196syl2anc 692 . . . . . . . . 9 (𝜑 → (𝐾 ∈ (ℤ𝑁) ↔ 𝑁𝐾))
198 nnleltp1 11392 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁𝐾𝑁 < (𝐾 + 1)))
1991, 15, 198syl2anc 692 . . . . . . . . 9 (𝜑 → (𝑁𝐾𝑁 < (𝐾 + 1)))
200 fzn 12315 . . . . . . . . . 10 (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
20194, 96, 200syl2anc 692 . . . . . . . . 9 (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
202197, 199, 2013bitrd 294 . . . . . . . 8 (𝜑 → (𝐾 ∈ (ℤ𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅))
203 0le0 11070 . . . . . . . . . 10 0 ≤ 0
20424mul01d 10195 . . . . . . . . . 10 (𝜑 → (𝑁 · 0) = 0)
205203, 204syl5breqr 4661 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑁 · 0))
206 iuneq1 4507 . . . . . . . . . . . . 13 (((𝐾 + 1)...𝑁) = ∅ → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) = 𝑘 ∈ ∅ (𝑊𝑘))
207 0iun 4550 . . . . . . . . . . . . 13 𝑘 ∈ ∅ (𝑊𝑘) = ∅
208206, 207syl6eq 2671 . . . . . . . . . . . 12 (((𝐾 + 1)...𝑁) = ∅ → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) = ∅)
209208fveq2d 6162 . . . . . . . . . . 11 (((𝐾 + 1)...𝑁) = ∅ → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = (#‘∅))
210 hash0 13114 . . . . . . . . . . 11 (#‘∅) = 0
211209, 210syl6eq 2671 . . . . . . . . . 10 (((𝐾 + 1)...𝑁) = ∅ → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = 0)
212 sumeq1 14369 . . . . . . . . . . . 12 (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
213 sum0 14401 . . . . . . . . . . . 12 Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
214212, 213syl6eq 2671 . . . . . . . . . . 11 (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
215214oveq2d 6631 . . . . . . . . . 10 (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
216211, 215breq12d 4636 . . . . . . . . 9 (((𝐾 + 1)...𝑁) = ∅ → ((#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0)))
217205, 216syl5ibrcom 237 . . . . . . . 8 (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
218202, 217sylbid 230 . . . . . . 7 (𝜑 → (𝐾 ∈ (ℤ𝑁) → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
219 uztric 11669 . . . . . . . 8 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝐾) ∨ 𝐾 ∈ (ℤ𝑁)))
22068, 96, 219syl2anc 692 . . . . . . 7 (𝜑 → (𝑁 ∈ (ℤ𝐾) ∨ 𝐾 ∈ (ℤ𝑁)))
221195, 218, 220mpjaod 396 . . . . . 6 (𝜑 → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
222 eqid 2621 . . . . . . . . . 10 (ℤ‘(𝐾 + 1)) = (ℤ‘(𝐾 + 1))
223 eleq1 2686 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
224 oveq2 6623 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
225223, 224ifbieq1d 4087 . . . . . . . . . . . 12 (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
226 ovex 6643 . . . . . . . . . . . . 13 (1 / 𝑘) ∈ V
227 c0ex 9994 . . . . . . . . . . . . 13 0 ∈ V
228226, 227ifex 4134 . . . . . . . . . . . 12 if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V
229225, 192, 228fvmpt 6249 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (𝐹𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
230183, 229syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → (𝐹𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
231187recnd 10028 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
232229, 231eqeltrd 2698 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝐹𝑘) ∈ ℂ)
233232adantl 482 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
23466, 27, 233iserex 14337 . . . . . . . . . . 11 (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ))
235193, 234mpbid 222 . . . . . . . . . 10 (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ )
236222, 94, 230, 188, 235isumrecl 14443 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
237 halfre 11206 . . . . . . . . . 10 (1 / 2) ∈ ℝ
238237a1i 11 . . . . . . . . 9 (𝜑 → (1 / 2) ∈ ℝ)
239 fzssuz 12340 . . . . . . . . . . 11 ((𝐾 + 1)...𝑁) ⊆ (ℤ‘(𝐾 + 1))
240239a1i 11 . . . . . . . . . 10 (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (ℤ‘(𝐾 + 1)))
241 nnrp 11802 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
242241rpreccld 11842 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
243242rpge0d 11836 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
244 breq2 4627 . . . . . . . . . . . . 13 ((1 / 𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
245 breq2 4627 . . . . . . . . . . . . 13 (0 = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
246244, 245ifboth 4102 . . . . . . . . . . . 12 ((0 ≤ (1 / 𝑘) ∧ 0 ≤ 0) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
247243, 203, 246sylancl 693 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
248183, 247syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
249222, 94, 182, 240, 230, 188, 248, 235isumless 14521 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
250190, 236, 238, 249, 194lelttrd 10155 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
2511nngt0d 11024 . . . . . . . . 9 (𝜑 → 0 < 𝑁)
252 ltmul2 10834 . . . . . . . . 9 ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ ∧ (1 / 2) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
253190, 238, 2, 251, 252syl112anc 1327 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
254250, 253mpbid 222 . . . . . . 7 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))
255 2cn 11051 . . . . . . . . 9 2 ∈ ℂ
256 2ne0 11073 . . . . . . . . 9 2 ≠ 0
257 divrec 10661 . . . . . . . . 9 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2)))
258255, 256, 257mp3an23 1413 . . . . . . . 8 (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2)))
25924, 258syl 17 . . . . . . 7 (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
260254, 259breqtrrd 4651 . . . . . 6 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2))
261181, 191, 3, 221, 260lelttrd 10155 . . . . 5 (𝜑 → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) < (𝑁 / 2))
262181, 3, 13, 261ltadd2dd 10156 . . . 4 (𝜑 → ((#‘𝑀) + (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) < ((#‘𝑀) + (𝑁 / 2)))
263178, 262eqbrtrd 4645 . . 3 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((#‘𝑀) + (𝑁 / 2)))
2643, 13, 3ltadd1d 10580 . . 3 (𝜑 → ((𝑁 / 2) < (#‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((#‘𝑀) + (𝑁 / 2))))
265263, 264mpbird 247 . 2 (𝜑 → (𝑁 / 2) < (#‘𝑀))
266 oveq1 6622 . . . . . . . 8 (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2))
267266breq1d 4633 . . . . . . 7 (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥))
268267cbvrabv 3189 . . . . . 6 {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥}
269 breq2 4627 . . . . . . 7 (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛))
270269rabbidv 3181 . . . . . 6 (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
271268, 270syl5eq 2667 . . . . 5 (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
272271supeq1d 8312 . . . 4 (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
273272cbvmptv 4720 . . 3 (𝑥 ∈ ℕ ↦ sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < )) = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
274192, 15, 1, 5, 273prmreclem3 15565 . 2 (𝜑 → (#‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
2753, 13, 23, 265, 274ltletrd 10157 1 (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2908  ∃wrex 2909  {crab 2912   ∖ cdif 3557   ∪ cun 3558   ∩ cin 3559   ⊆ wss 3560  ∅c0 3897  ifcif 4064  ∪ ciun 4492   class class class wbr 4623   ↦ cmpt 4683  dom cdm 5084  ‘cfv 5857  (class class class)co 6615  Fincfn 7915  supcsup 8306  ℂcc 9894  ℝcr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901   < clt 10034   ≤ cle 10035   / cdiv 10644  ℕcn 10980  2c2 11030  ℕ0cn0 11252  ℤcz 11337  ℤ≥cuz 11647  ...cfz 12284  seqcseq 12757  ↑cexp 12816  #chash 13073  √csqrt 13923   ⇝ cli 14165  Σcsu 14366   ∥ cdvds 14926  ℙcprime 15328 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-n0 11253  df-xnn0 11324  df-z 11338  df-uz 11648  df-q 11749  df-rp 11793  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-seq 12758  df-exp 12817  df-hash 13074  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-clim 14169  df-rlim 14170  df-sum 14367  df-dvds 14927  df-gcd 15160  df-prm 15329  df-pc 15485 This theorem is referenced by:  prmreclem6  15568
 Copyright terms: Public domain W3C validator