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

Theorem prmreclem5 15404
Description: Lemma for prmrec 15406. 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 15403 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 10878 . . 3 (𝜑𝑁 ∈ ℝ)
32rehalfcld 11122 . 2 (𝜑 → (𝑁 / 2) ∈ ℝ)
4 fzfi 12584 . . . . . 6 (1...𝑁) ∈ Fin
5 prmrec.4 . . . . . . 7 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛}
6 ssrab2 3645 . . . . . . 7 {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛} ⊆ (1...𝑁)
75, 6eqsstri 3593 . . . . . 6 𝑀 ⊆ (1...𝑁)
8 ssfi 8038 . . . . . 6 (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
94, 7, 8mp2an 703 . . . . 5 𝑀 ∈ Fin
10 hashcl 12957 . . . . 5 (𝑀 ∈ Fin → (#‘𝑀) ∈ ℕ0)
119, 10ax-mp 5 . . . 4 (#‘𝑀) ∈ ℕ0
1211nn0rei 11146 . . 3 (#‘𝑀) ∈ ℝ
1312a1i 11 . 2 (𝜑 → (#‘𝑀) ∈ ℝ)
14 2nn 11028 . . . . 5 2 ∈ ℕ
15 prmrec.2 . . . . . 6 (𝜑𝐾 ∈ ℕ)
1615nnnn0d 11194 . . . . 5 (𝜑𝐾 ∈ ℕ0)
17 nnexpcl 12686 . . . . 5 ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ0) → (2↑𝐾) ∈ ℕ)
1814, 16, 17sylancr 693 . . . 4 (𝜑 → (2↑𝐾) ∈ ℕ)
1918nnred 10878 . . 3 (𝜑 → (2↑𝐾) ∈ ℝ)
201nnrpd 11698 . . . . 5 (𝜑𝑁 ∈ ℝ+)
2120rpsqrtcld 13940 . . . 4 (𝜑 → (√‘𝑁) ∈ ℝ+)
2221rpred 11700 . . 3 (𝜑 → (√‘𝑁) ∈ ℝ)
2319, 22remulcld 9922 . 2 (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
242recnd 9920 . . . . . 6 (𝜑𝑁 ∈ ℂ)
25242halvesd 11121 . . . . 5 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁)
267a1i 11 . . . . . . . . 9 (𝜑𝑀 ⊆ (1...𝑁))
2715peano2nnd 10880 . . . . . . . . . . . . 13 (𝜑 → (𝐾 + 1) ∈ ℕ)
28 elfzuz 12160 . . . . . . . . . . . . 13 (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ‘(𝐾 + 1)))
29 eluznn 11586 . . . . . . . . . . . . 13 (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
3027, 28, 29syl2an 492 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
31 eleq1 2671 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
32 breq1 4576 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝𝑛𝑘𝑛))
3331, 32anbi12d 742 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑛)))
3433rabbidv 3159 . . . . . . . . . . . . . . 15 (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
35 prmrec.7 . . . . . . . . . . . . . . 15 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)})
36 ovex 6551 . . . . . . . . . . . . . . . 16 (1...𝑁) ∈ V
3736rabex 4731 . . . . . . . . . . . . . . 15 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ∈ V
3834, 35, 37fvmpt 6172 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
3938adantl 480 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
40 ssrab2 3645 . . . . . . . . . . . . 13 {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ⊆ (1...𝑁)
4139, 40syl6eqss 3613 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝑊𝑘) ⊆ (1...𝑁))
4230, 41syldan 485 . . . . . . . . . . 11 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊𝑘) ⊆ (1...𝑁))
4342ralrimiva 2944 . . . . . . . . . 10 (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
44 iunss 4487 . . . . . . . . . 10 ( 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
4543, 44sylibr 222 . . . . . . . . 9 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁))
4626, 45unssd 3746 . . . . . . . 8 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ⊆ (1...𝑁))
47 breq1 4576 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → (𝑝𝑛𝑞𝑛))
4847notbid 306 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑞 → (¬ 𝑝𝑛 ↔ ¬ 𝑞𝑛))
4948cbvralv 3142 . . . . . . . . . . . . . . . 16 (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑛)
50 breq2 4577 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑥 → (𝑞𝑛𝑞𝑥))
5150notbid 306 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑥 → (¬ 𝑞𝑛 ↔ ¬ 𝑞𝑥))
5251ralbidv 2964 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
5349, 52syl5bb 270 . . . . . . . . . . . . . . 15 (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
5453, 5elrab2 3328 . . . . . . . . . . . . . 14 (𝑥𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥))
55 elun1 3737 . . . . . . . . . . . . . 14 (𝑥𝑀𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
5654, 55sylbir 223 . . . . . . . . . . . . 13 ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
5756ex 448 . . . . . . . . . . . 12 (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
5857adantl 480 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
59 dfrex2 2974 . . . . . . . . . . . 12 (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥)
60 eldifn 3690 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ (ℙ ∖ (1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾))
6160ad2antrl 759 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → ¬ 𝑞 ∈ (1...𝐾))
62 eldifi 3689 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑞 ∈ (ℙ ∖ (1...𝐾)) → 𝑞 ∈ ℙ)
6362ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℙ)
64 prmnn 15168 . . . . . . . . . . . . . . . . . . . . . 22 (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℕ)
66 nnuz 11551 . . . . . . . . . . . . . . . . . . . . 21 ℕ = (ℤ‘1)
6765, 66syl6eleq 2693 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ (ℤ‘1))
6815nnzd 11309 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐾 ∈ ℤ)
6968ad2antrr 757 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 ∈ ℤ)
70 elfz5 12156 . . . . . . . . . . . . . . . . . . . 20 ((𝑞 ∈ (ℤ‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞𝐾))
7167, 69, 70syl2anc 690 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞𝐾))
7261, 71mtbid 312 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → ¬ 𝑞𝐾)
7315nnred 10878 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐾 ∈ ℝ)
7473ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 ∈ ℝ)
7565nnred 10878 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℝ)
7674, 75ltnled 10031 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞𝐾))
7772, 76mpbird 245 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝐾 < 𝑞)
78 prmz 15169 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
7963, 78syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ℤ)
80 zltp1le 11256 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
8169, 79, 80syl2anc 690 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
8277, 81mpbid 220 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 + 1) ≤ 𝑞)
83 elfznn 12192 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
8483ad2antlr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ ℕ)
8584nnred 10878 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ ℝ)
862ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑁 ∈ ℝ)
87 simprr 791 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑥)
88 dvdsle 14812 . . . . . . . . . . . . . . . . . . 19 ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞𝑥𝑞𝑥))
8979, 84, 88syl2anc 690 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞𝑥𝑞𝑥))
9087, 89mpd 15 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑥)
91 elfzle2 12167 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (1...𝑁) → 𝑥𝑁)
9291ad2antlr 758 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥𝑁)
9375, 85, 86, 90, 92letrd 10041 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞𝑁)
9468peano2zd 11313 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐾 + 1) ∈ ℤ)
9594ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝐾 + 1) ∈ ℤ)
961nnzd 11309 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℤ)
9796ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑁 ∈ ℤ)
98 elfz 12154 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞𝑞𝑁)))
9979, 95, 97, 98syl3anc 1317 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞𝑞𝑁)))
10082, 93, 99mpbir2and 958 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁))
101 simplr 787 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (1...𝑁))
10263, 87jca 552 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞𝑥))
10350anbi2d 735 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑥)))
104103elrab 3326 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑞 ∈ ℙ ∧ 𝑞𝑥)))
105101, 102, 104sylanbrc 694 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
106 eleq1 2671 . . . . . . . . . . . . . . . . . . . 20 (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ))
107106, 47anbi12d 742 . . . . . . . . . . . . . . . . . . 19 (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞𝑛)))
108107rabbidv 3159 . . . . . . . . . . . . . . . . . 18 (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
10936rabex 4731 . . . . . . . . . . . . . . . . . 18 {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)} ∈ V
110108, 35, 109fvmpt 6172 . . . . . . . . . . . . . . . . 17 (𝑞 ∈ ℕ → (𝑊𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
11165, 110syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → (𝑊𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞𝑛)})
112105, 111eleqtrrd 2686 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (𝑊𝑞))
113 fveq2 6084 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑞 → (𝑊𝑘) = (𝑊𝑞))
114113eliuni 4452 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊𝑞)) → 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
115100, 112, 114syl2anc 690 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
116 elun2 3738 . . . . . . . . . . . . . 14 (𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
117115, 116syl 17 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞𝑥)) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
118117rexlimdvaa 3009 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
11959, 118syl5bir 231 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞𝑥𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
12058, 119pm2.61d 168 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
121120ex 448 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (1...𝑁) → 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
122121ssrdv 3569 . . . . . . . 8 (𝜑 → (1...𝑁) ⊆ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
12346, 122eqssd 3580 . . . . . . 7 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = (1...𝑁))
124123fveq2d 6088 . . . . . 6 (𝜑 → (#‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = (#‘(1...𝑁)))
1251nnnn0d 11194 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
126 hashfz1 12944 . . . . . . 7 (𝑁 ∈ ℕ0 → (#‘(1...𝑁)) = 𝑁)
127125, 126syl 17 . . . . . 6 (𝜑 → (#‘(1...𝑁)) = 𝑁)
128124, 127eqtr2d 2640 . . . . 5 (𝜑𝑁 = (#‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
1299a1i 11 . . . . . 6 (𝜑𝑀 ∈ Fin)
130 ssfi 8038 . . . . . . 7 (((1...𝑁) ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ⊆ (1...𝑁)) → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin)
1314, 45, 130sylancr 693 . . . . . 6 (𝜑 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin)
132 breq1 4576 . . . . . . . . . . . . . . . . 17 (𝑝 = 𝑘 → (𝑝𝑥𝑘𝑥))
133132notbid 306 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑘 → (¬ 𝑝𝑥 ↔ ¬ 𝑘𝑥))
134 breq2 4577 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑥 → (𝑝𝑛𝑝𝑥))
135134notbid 306 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑥 → (¬ 𝑝𝑛 ↔ ¬ 𝑝𝑥))
136135ralbidv 2964 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥))
137136, 5elrab2 3328 . . . . . . . . . . . . . . . . . 18 (𝑥𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥))
138137simprbi 478 . . . . . . . . . . . . . . . . 17 (𝑥𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥)
139138ad2antlr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝𝑥)
140 simprr 791 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ)
141 noel 3873 . . . . . . . . . . . . . . . . . 18 ¬ 𝑘 ∈ ∅
142 simprl 789 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁))
143142biantrud 526 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))))
144 elin 3753 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))
145143, 144syl6bbr 276 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁))))
14673ltp1d 10799 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐾 < (𝐾 + 1))
147 fzdisj 12190 . . . . . . . . . . . . . . . . . . . . . 22 (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
148146, 147syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
149148ad2antrr 757 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
150149eleq2d 2668 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅))
151145, 150bitrd 266 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅))
152141, 151mtbiri 315 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾))
153140, 152eldifd 3546 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾)))
154133, 139, 153rspcdva 3283 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘𝑥)
155154expr 640 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘𝑥))
156 imnan 436 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℙ → ¬ 𝑘𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘𝑥))
157155, 156sylib 206 . . . . . . . . . . . . 13 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘𝑥))
15830adantlr 746 . . . . . . . . . . . . . . . 16 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
159158, 38syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)})
160159eleq2d 2668 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)}))
161 breq2 4577 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑥 → (𝑘𝑛𝑘𝑥))
162161anbi2d 735 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
163162elrab 3326 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
164163simprbi 478 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘𝑥))
165160, 164syl6bi 241 . . . . . . . . . . . . 13 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊𝑘) → (𝑘 ∈ ℙ ∧ 𝑘𝑥)))
166157, 165mtod 187 . . . . . . . . . . . 12 (((𝜑𝑥𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊𝑘))
167166nrexdv 2979 . . . . . . . . . . 11 ((𝜑𝑥𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊𝑘))
168 eliun 4450 . . . . . . . . . . 11 (𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊𝑘))
169167, 168sylnibr 317 . . . . . . . . . 10 ((𝜑𝑥𝑀) → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))
170169ex 448 . . . . . . . . 9 (𝜑 → (𝑥𝑀 → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
171 imnan 436 . . . . . . . . 9 ((𝑥𝑀 → ¬ 𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ↔ ¬ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
172170, 171sylib 206 . . . . . . . 8 (𝜑 → ¬ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
173 elin 3753 . . . . . . . 8 (𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ↔ (𝑥𝑀𝑥 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
174172, 173sylnibr 317 . . . . . . 7 (𝜑 → ¬ 𝑥 ∈ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)))
175174eq0rdv 3926 . . . . . 6 (𝜑 → (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = ∅)
176 hashun 12980 . . . . . 6 ((𝑀 ∈ Fin ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin ∧ (𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = ∅) → (#‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = ((#‘𝑀) + (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
177129, 131, 175, 176syl3anc 1317 . . . . 5 (𝜑 → (#‘(𝑀 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) = ((#‘𝑀) + (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
17825, 128, 1773eqtrd 2643 . . . 4 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((#‘𝑀) + (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))))
179 hashcl 12957 . . . . . . 7 ( 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) ∈ Fin → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℕ0)
180131, 179syl 17 . . . . . 6 (𝜑 → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℕ0)
181180nn0red 11195 . . . . 5 (𝜑 → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ∈ ℝ)
182 fzfid 12585 . . . . . . . 8 (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
18327, 29sylan 486 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
184 nnrecre 10900 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
185 0re 9892 . . . . . . . . . . 11 0 ∈ ℝ
186 ifcl 4075 . . . . . . . . . . 11 (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
187184, 185, 186sylancl 692 . . . . . . . . . 10 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
188183, 187syl 17 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
18928, 188sylan2 489 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝐾 + 1)...𝑁)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
190182, 189fsumrecl 14254 . . . . . . 7 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
1912, 190remulcld 9922 . . . . . 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 15403 . . . . . . 7 (𝜑 → (𝑁 ∈ (ℤ𝐾) → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
196 eluz 11529 . . . . . . . . . 10 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (ℤ𝑁) ↔ 𝑁𝐾))
19796, 68, 196syl2anc 690 . . . . . . . . 9 (𝜑 → (𝐾 ∈ (ℤ𝑁) ↔ 𝑁𝐾))
198 nnleltp1 11261 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁𝐾𝑁 < (𝐾 + 1)))
1991, 15, 198syl2anc 690 . . . . . . . . 9 (𝜑 → (𝑁𝐾𝑁 < (𝐾 + 1)))
200 fzn 12179 . . . . . . . . . 10 (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
20194, 96, 200syl2anc 690 . . . . . . . . 9 (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
202197, 199, 2013bitrd 292 . . . . . . . 8 (𝜑 → (𝐾 ∈ (ℤ𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅))
203 0le0 10953 . . . . . . . . . 10 0 ≤ 0
20424mul01d 10082 . . . . . . . . . 10 (𝜑 → (𝑁 · 0) = 0)
205203, 204syl5breqr 4611 . . . . . . . . 9 (𝜑 → 0 ≤ (𝑁 · 0))
206 iuneq1 4460 . . . . . . . . . . . . 13 (((𝐾 + 1)...𝑁) = ∅ → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) = 𝑘 ∈ ∅ (𝑊𝑘))
207 0iun 4503 . . . . . . . . . . . . 13 𝑘 ∈ ∅ (𝑊𝑘) = ∅
208206, 207syl6eq 2655 . . . . . . . . . . . 12 (((𝐾 + 1)...𝑁) = ∅ → 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘) = ∅)
209208fveq2d 6088 . . . . . . . . . . 11 (((𝐾 + 1)...𝑁) = ∅ → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = (#‘∅))
210 hash0 12967 . . . . . . . . . . 11 (#‘∅) = 0
211209, 210syl6eq 2655 . . . . . . . . . 10 (((𝐾 + 1)...𝑁) = ∅ → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) = 0)
212 sumeq1 14209 . . . . . . . . . . . 12 (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
213 sum0 14241 . . . . . . . . . . . 12 Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
214212, 213syl6eq 2655 . . . . . . . . . . 11 (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
215214oveq2d 6539 . . . . . . . . . 10 (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
216211, 215breq12d 4586 . . . . . . . . 9 (((𝐾 + 1)...𝑁) = ∅ → ((#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0)))
217205, 216syl5ibrcom 235 . . . . . . . 8 (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
218202, 217sylbid 228 . . . . . . 7 (𝜑 → (𝐾 ∈ (ℤ𝑁) → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
219 uztric 11537 . . . . . . . 8 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝐾) ∨ 𝐾 ∈ (ℤ𝑁)))
22068, 96, 219syl2anc 690 . . . . . . 7 (𝜑 → (𝑁 ∈ (ℤ𝐾) ∨ 𝐾 ∈ (ℤ𝑁)))
221195, 218, 220mpjaod 394 . . . . . 6 (𝜑 → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
222 eqid 2605 . . . . . . . . . 10 (ℤ‘(𝐾 + 1)) = (ℤ‘(𝐾 + 1))
223 eleq1 2671 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
224 oveq2 6531 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
225223, 224ifbieq1d 4054 . . . . . . . . . . . 12 (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
226 ovex 6551 . . . . . . . . . . . . 13 (1 / 𝑘) ∈ V
227 c0ex 9886 . . . . . . . . . . . . 13 0 ∈ V
228226, 227ifex 4101 . . . . . . . . . . . 12 if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V
229225, 192, 228fvmpt 6172 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (𝐹𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
230183, 229syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → (𝐹𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
231187recnd 9920 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
232229, 231eqeltrd 2683 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (𝐹𝑘) ∈ ℂ)
233232adantl 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℂ)
23466, 27, 233iserex 14177 . . . . . . . . . . 11 (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ))
235193, 234mpbid 220 . . . . . . . . . 10 (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ )
236222, 94, 230, 188, 235isumrecl 14280 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
237 halfre 11089 . . . . . . . . . 10 (1 / 2) ∈ ℝ
238237a1i 11 . . . . . . . . 9 (𝜑 → (1 / 2) ∈ ℝ)
239 fzssuz 12204 . . . . . . . . . . 11 ((𝐾 + 1)...𝑁) ⊆ (ℤ‘(𝐾 + 1))
240239a1i 11 . . . . . . . . . 10 (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (ℤ‘(𝐾 + 1)))
241 nnrp 11670 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
242241rpreccld 11710 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
243242rpge0d 11704 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
244 breq2 4577 . . . . . . . . . . . . 13 ((1 / 𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
245 breq2 4577 . . . . . . . . . . . . 13 (0 = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
246244, 245ifboth 4069 . . . . . . . . . . . 12 ((0 ≤ (1 / 𝑘) ∧ 0 ≤ 0) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
247243, 203, 246sylancl 692 . . . . . . . . . . 11 (𝑘 ∈ ℕ → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
248183, 247syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (ℤ‘(𝐾 + 1))) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
249222, 94, 182, 240, 230, 188, 248, 235isumless 14358 . . . . . . . . 9 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
250190, 236, 238, 249, 194lelttrd 10042 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
2511nngt0d 10907 . . . . . . . . 9 (𝜑 → 0 < 𝑁)
252 ltmul2 10719 . . . . . . . . 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 1321 . . . . . . . 8 (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
254250, 253mpbid 220 . . . . . . 7 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))
255 2cn 10934 . . . . . . . . 9 2 ∈ ℂ
256 2ne0 10956 . . . . . . . . 9 2 ≠ 0
257 divrec 10546 . . . . . . . . 9 ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2)))
258255, 256, 257mp3an23 1407 . . . . . . . 8 (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2)))
25924, 258syl 17 . . . . . . 7 (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
260254, 259breqtrrd 4601 . . . . . 6 (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2))
261181, 191, 3, 221, 260lelttrd 10042 . . . . 5 (𝜑 → (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘)) < (𝑁 / 2))
262181, 3, 13, 261ltadd2dd 10043 . . . 4 (𝜑 → ((#‘𝑀) + (#‘ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊𝑘))) < ((#‘𝑀) + (𝑁 / 2)))
263178, 262eqbrtrd 4595 . . 3 (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((#‘𝑀) + (𝑁 / 2)))
2643, 13, 3ltadd1d 10465 . . 3 (𝜑 → ((𝑁 / 2) < (#‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((#‘𝑀) + (𝑁 / 2))))
265263, 264mpbird 245 . 2 (𝜑 → (𝑁 / 2) < (#‘𝑀))
266 oveq1 6530 . . . . . . . 8 (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2))
267266breq1d 4583 . . . . . . 7 (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥))
268267cbvrabv 3167 . . . . . 6 {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥}
269 breq2 4577 . . . . . . 7 (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛))
270269rabbidv 3159 . . . . . 6 (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
271268, 270syl5eq 2651 . . . . 5 (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
272271supeq1d 8208 . . . 4 (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
273272cbvmptv 4668 . . 3 (𝑥 ∈ ℕ ↦ sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < )) = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
274192, 15, 1, 5, 273prmreclem3 15402 . 2 (𝜑 → (#‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
2753, 13, 23, 265, 274ltletrd 10044 1 (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1975  wne 2775  wral 2891  wrex 2892  {crab 2895  cdif 3532  cun 3533  cin 3534  wss 3535  c0 3869  ifcif 4031   ciun 4445   class class class wbr 4573  cmpt 4633  dom cdm 5024  cfv 5786  (class class class)co 6523  Fincfn 7814  supcsup 8202  cc 9786  cr 9787  0cc0 9788  1c1 9789   + caddc 9791   · cmul 9793   < clt 9926  cle 9927   / cdiv 10529  cn 10863  2c2 10913  0cn0 11135  cz 11206  cuz 11515  ...cfz 12148  seqcseq 12614  cexp 12673  #chash 12930  csqrt 13763  cli 14005  Σcsu 14206  cdvds 14763  cprime 15165
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-inf2 8394  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865  ax-pre-sup 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-se 4984  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-isom 5795  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-om 6931  df-1st 7032  df-2nd 7033  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-2o 7421  df-oadd 7424  df-er 7602  df-map 7719  df-pm 7720  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-sup 8204  df-inf 8205  df-oi 8271  df-card 8621  df-cda 8846  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-div 10530  df-nn 10864  df-2 10922  df-3 10923  df-n0 11136  df-z 11207  df-uz 11516  df-q 11617  df-rp 11661  df-fz 12149  df-fzo 12286  df-fl 12406  df-mod 12482  df-seq 12615  df-exp 12674  df-hash 12931  df-cj 13629  df-re 13630  df-im 13631  df-sqrt 13765  df-abs 13766  df-clim 14009  df-rlim 14010  df-sum 14207  df-dvds 14764  df-gcd 14997  df-prm 15166  df-pc 15322
This theorem is referenced by:  prmreclem6  15405
  Copyright terms: Public domain W3C validator