| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzfid 14015 | . . . . 5
⊢ (𝜑 → (1...𝑁) ∈ Fin) | 
| 2 |  | diffi 9216 | . . . . 5
⊢
((1...𝑁) ∈ Fin
→ ((1...𝑁) ∖
ℙ) ∈ Fin) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ∈
Fin) | 
| 4 |  | vmaf 27163 | . . . . . 6
⊢
Λ:ℕ⟶ℝ | 
| 5 | 4 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ ℙ)) →
Λ:ℕ⟶ℝ) | 
| 6 |  | fz1ssnn 13596 | . . . . . . . 8
⊢
(1...𝑁) ⊆
ℕ | 
| 7 | 6 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) | 
| 8 | 7 | ssdifssd 4146 | . . . . . 6
⊢ (𝜑 → ((1...𝑁) ∖ ℙ) ⊆
ℕ) | 
| 9 | 8 | sselda 3982 | . . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ ℙ)) → 𝑖 ∈
ℕ) | 
| 10 | 5, 9 | ffvelcdmd 7104 | . . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ ℙ)) →
(Λ‘𝑖) ∈
ℝ) | 
| 11 | 3, 10 | fsumrecl 15771 | . . 3
⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) ∈
ℝ) | 
| 12 |  | 2rp 13040 | . . . . 5
⊢ 2 ∈
ℝ+ | 
| 13 | 12 | a1i 11 | . . . 4
⊢ (𝜑 → 2 ∈
ℝ+) | 
| 14 | 13 | relogcld 26666 | . . 3
⊢ (𝜑 → (log‘2) ∈
ℝ) | 
| 15 |  | 1nn0 12544 | . . . . . 6
⊢ 1 ∈
ℕ0 | 
| 16 |  | 4re 12351 | . . . . . . . 8
⊢ 4 ∈
ℝ | 
| 17 |  | 2re 12341 | . . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 18 |  | 6re 12357 | . . . . . . . . . . . 12
⊢ 6 ∈
ℝ | 
| 19 | 18, 17 | pm3.2i 470 | . . . . . . . . . . 11
⊢ (6 ∈
ℝ ∧ 2 ∈ ℝ) | 
| 20 |  | dp2cl 32863 | . . . . . . . . . . 11
⊢ ((6
∈ ℝ ∧ 2 ∈ ℝ) → _62 ∈ ℝ) | 
| 21 | 19, 20 | ax-mp 5 | . . . . . . . . . 10
⊢ _62 ∈ ℝ | 
| 22 | 17, 21 | pm3.2i 470 | . . . . . . . . 9
⊢ (2 ∈
ℝ ∧ _62 ∈
ℝ) | 
| 23 |  | dp2cl 32863 | . . . . . . . . 9
⊢ ((2
∈ ℝ ∧ _62 ∈
ℝ) → _2_62 ∈ ℝ) | 
| 24 | 22, 23 | ax-mp 5 | . . . . . . . 8
⊢ _2_62 ∈ ℝ | 
| 25 | 16, 24 | pm3.2i 470 | . . . . . . 7
⊢ (4 ∈
ℝ ∧ _2_62 ∈ ℝ) | 
| 26 |  | dp2cl 32863 | . . . . . . 7
⊢ ((4
∈ ℝ ∧ _2_62 ∈ ℝ) → _4_2_62
∈ ℝ) | 
| 27 | 25, 26 | ax-mp 5 | . . . . . 6
⊢ _4_2_62
∈ ℝ | 
| 28 |  | dpcl 32874 | . . . . . 6
⊢ ((1
∈ ℕ0 ∧ _4_2_62
∈ ℝ) → (1._4_2_62) ∈ ℝ) | 
| 29 | 15, 27, 28 | mp2an 692 | . . . . 5
⊢ (1._4_2_62)
∈ ℝ | 
| 30 | 29 | a1i 11 | . . . 4
⊢ (𝜑 → (1._4_2_62)
∈ ℝ) | 
| 31 |  | hgt750lemc.n | . . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 32 | 31 | nnred 12282 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 33 | 31 | nnrpd 13076 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℝ+) | 
| 34 | 33 | rpge0d 13082 | . . . . 5
⊢ (𝜑 → 0 ≤ 𝑁) | 
| 35 | 32, 34 | resqrtcld 15457 | . . . 4
⊢ (𝜑 → (√‘𝑁) ∈
ℝ) | 
| 36 | 30, 35 | remulcld 11292 | . . 3
⊢ (𝜑 → ((1._4_2_62)
· (√‘𝑁))
∈ ℝ) | 
| 37 |  | 0nn0 12543 | . . . . . 6
⊢ 0 ∈
ℕ0 | 
| 38 |  | 0re 11264 | . . . . . . . 8
⊢ 0 ∈
ℝ | 
| 39 |  | 1re 11262 | . . . . . . . . . . . 12
⊢ 1 ∈
ℝ | 
| 40 | 38, 39 | pm3.2i 470 | . . . . . . . . . . 11
⊢ (0 ∈
ℝ ∧ 1 ∈ ℝ) | 
| 41 |  | dp2cl 32863 | . . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ) → _01 ∈ ℝ) | 
| 42 | 40, 41 | ax-mp 5 | . . . . . . . . . 10
⊢ _01 ∈ ℝ | 
| 43 | 38, 42 | pm3.2i 470 | . . . . . . . . 9
⊢ (0 ∈
ℝ ∧ _01 ∈
ℝ) | 
| 44 |  | dp2cl 32863 | . . . . . . . . 9
⊢ ((0
∈ ℝ ∧ _01 ∈
ℝ) → _0_01 ∈ ℝ) | 
| 45 | 43, 44 | ax-mp 5 | . . . . . . . 8
⊢ _0_01 ∈ ℝ | 
| 46 | 38, 45 | pm3.2i 470 | . . . . . . 7
⊢ (0 ∈
ℝ ∧ _0_01 ∈ ℝ) | 
| 47 |  | dp2cl 32863 | . . . . . . 7
⊢ ((0
∈ ℝ ∧ _0_01 ∈ ℝ) → _0_0_01
∈ ℝ) | 
| 48 | 46, 47 | ax-mp 5 | . . . . . 6
⊢ _0_0_01
∈ ℝ | 
| 49 |  | dpcl 32874 | . . . . . 6
⊢ ((0
∈ ℕ0 ∧ _0_0_01
∈ ℝ) → (0._0_0_01) ∈ ℝ) | 
| 50 | 37, 48, 49 | mp2an 692 | . . . . 5
⊢ (0._0_0_01)
∈ ℝ | 
| 51 | 50 | a1i 11 | . . . 4
⊢ (𝜑 → (0._0_0_01)
∈ ℝ) | 
| 52 | 51, 35 | remulcld 11292 | . . 3
⊢ (𝜑 → ((0._0_0_01)
· (√‘𝑁))
∈ ℝ) | 
| 53 | 31 | nnzd 12642 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 54 |  | chpvalz 34644 | . . . . . . 7
⊢ (𝑁 ∈ ℤ →
(ψ‘𝑁) =
Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖)) | 
| 55 | 53, 54 | syl 17 | . . . . . 6
⊢ (𝜑 → (ψ‘𝑁) = Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖)) | 
| 56 |  | chtvalz 34645 | . . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(θ‘𝑁) =
Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖)) | 
| 57 | 53, 56 | syl 17 | . . . . . . 7
⊢ (𝜑 → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖)) | 
| 58 |  | inss2 4237 | . . . . . . . . . . 11
⊢
((1...𝑁) ∩
ℙ) ⊆ ℙ | 
| 59 | 58 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ((1...𝑁) ∩ ℙ) ⊆
ℙ) | 
| 60 | 59 | sselda 3982 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) → 𝑖 ∈ ℙ) | 
| 61 |  | vmaprm 27161 | . . . . . . . . 9
⊢ (𝑖 ∈ ℙ →
(Λ‘𝑖) =
(log‘𝑖)) | 
| 62 | 60, 61 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) →
(Λ‘𝑖) =
(log‘𝑖)) | 
| 63 | 62 | sumeq2dv 15739 | . . . . . . 7
⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(log‘𝑖)) | 
| 64 | 57, 63 | eqtr4d 2779 | . . . . . 6
⊢ (𝜑 → (θ‘𝑁) = Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖)) | 
| 65 | 55, 64 | oveq12d 7450 | . . . . 5
⊢ (𝜑 → ((ψ‘𝑁) − (θ‘𝑁)) = (Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) − Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖))) | 
| 66 |  | infi 9303 | . . . . . . . 8
⊢
((1...𝑁) ∈ Fin
→ ((1...𝑁) ∩
ℙ) ∈ Fin) | 
| 67 | 1, 66 | syl 17 | . . . . . . 7
⊢ (𝜑 → ((1...𝑁) ∩ ℙ) ∈
Fin) | 
| 68 | 4 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) →
Λ:ℕ⟶ℝ) | 
| 69 |  | inss1 4236 | . . . . . . . . . . . 12
⊢
((1...𝑁) ∩
ℙ) ⊆ (1...𝑁) | 
| 70 | 69, 6 | sstri 3992 | . . . . . . . . . . 11
⊢
((1...𝑁) ∩
ℙ) ⊆ ℕ | 
| 71 | 70 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → ((1...𝑁) ∩ ℙ) ⊆
ℕ) | 
| 72 | 71 | sselda 3982 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) → 𝑖 ∈ ℕ) | 
| 73 | 68, 72 | ffvelcdmd 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) →
(Λ‘𝑖) ∈
ℝ) | 
| 74 | 73 | recnd 11290 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∩ ℙ)) →
(Λ‘𝑖) ∈
ℂ) | 
| 75 | 67, 74 | fsumcl 15770 | . . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) ∈
ℂ) | 
| 76 | 10 | recnd 11290 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ ℙ)) →
(Λ‘𝑖) ∈
ℂ) | 
| 77 | 3, 76 | fsumcl 15770 | . . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) ∈
ℂ) | 
| 78 |  | inindif 4374 | . . . . . . . 8
⊢
(((1...𝑁) ∩
ℙ) ∩ ((1...𝑁)
∖ ℙ)) = ∅ | 
| 79 | 78 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (((1...𝑁) ∩ ℙ) ∩ ((1...𝑁) ∖ ℙ)) =
∅) | 
| 80 |  | inundif 4478 | . . . . . . . . 9
⊢
(((1...𝑁) ∩
ℙ) ∪ ((1...𝑁)
∖ ℙ)) = (1...𝑁) | 
| 81 | 80 | eqcomi 2745 | . . . . . . . 8
⊢
(1...𝑁) =
(((1...𝑁) ∩ ℙ)
∪ ((1...𝑁) ∖
ℙ)) | 
| 82 | 81 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (1...𝑁) = (((1...𝑁) ∩ ℙ) ∪ ((1...𝑁) ∖
ℙ))) | 
| 83 | 4 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) →
Λ:ℕ⟶ℝ) | 
| 84 | 7 | sselda 3982 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → 𝑖 ∈ ℕ) | 
| 85 | 83, 84 | ffvelcdmd 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (Λ‘𝑖) ∈ ℝ) | 
| 86 | 85 | recnd 11290 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑁)) → (Λ‘𝑖) ∈ ℂ) | 
| 87 | 79, 82, 1, 86 | fsumsplit 15778 | . . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) = (Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖) + Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖))) | 
| 88 | 75, 77, 87 | mvrladdd 11677 | . . . . 5
⊢ (𝜑 → (Σ𝑖 ∈ (1...𝑁)(Λ‘𝑖) − Σ𝑖 ∈ ((1...𝑁) ∩ ℙ)(Λ‘𝑖)) = Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖)) | 
| 89 | 65, 88 | eqtr2d 2777 | . . . 4
⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) = ((ψ‘𝑁) − (θ‘𝑁))) | 
| 90 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (ψ‘𝑥) = (ψ‘𝑁)) | 
| 91 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (θ‘𝑥) = (θ‘𝑁)) | 
| 92 | 90, 91 | oveq12d 7450 | . . . . . 6
⊢ (𝑥 = 𝑁 → ((ψ‘𝑥) − (θ‘𝑥)) = ((ψ‘𝑁) − (θ‘𝑁))) | 
| 93 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (√‘𝑥) = (√‘𝑁)) | 
| 94 | 93 | oveq2d 7448 | . . . . . 6
⊢ (𝑥 = 𝑁 → ((1._4_2_62)
· (√‘𝑥))
= ((1._4_2_62)
· (√‘𝑁))) | 
| 95 | 92, 94 | breq12d 5155 | . . . . 5
⊢ (𝑥 = 𝑁 → (((ψ‘𝑥) − (θ‘𝑥)) < ((1._4_2_62)
· (√‘𝑥))
↔ ((ψ‘𝑁)
− (θ‘𝑁))
< ((1._4_2_62)
· (√‘𝑁)))) | 
| 96 |  | ax-ros336 34662 | . . . . . 6
⊢
∀𝑥 ∈
ℝ+ ((ψ‘𝑥) − (θ‘𝑥)) < ((1._4_2_62)
· (√‘𝑥)) | 
| 97 | 96 | a1i 11 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℝ+
((ψ‘𝑥) −
(θ‘𝑥)) <
((1._4_2_62)
· (√‘𝑥))) | 
| 98 | 95, 97, 33 | rspcdva 3622 | . . . 4
⊢ (𝜑 → ((ψ‘𝑁) − (θ‘𝑁)) < ((1._4_2_62)
· (√‘𝑁))) | 
| 99 | 89, 98 | eqbrtrd 5164 | . . 3
⊢ (𝜑 → Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) < ((1._4_2_62)
· (√‘𝑁))) | 
| 100 | 39 | a1i 11 | . . . 4
⊢ (𝜑 → 1 ∈
ℝ) | 
| 101 |  | log2le1 26994 | . . . . 5
⊢
(log‘2) < 1 | 
| 102 | 101 | a1i 11 | . . . 4
⊢ (𝜑 → (log‘2) <
1) | 
| 103 |  | 10nn0 12753 | . . . . . . . . 9
⊢ ;10 ∈
ℕ0 | 
| 104 |  | 7nn0 12550 | . . . . . . . . 9
⊢ 7 ∈
ℕ0 | 
| 105 | 103, 104 | nn0expcli 14130 | . . . . . . . 8
⊢ (;10↑7) ∈
ℕ0 | 
| 106 | 105 | nn0rei 12539 | . . . . . . 7
⊢ (;10↑7) ∈
ℝ | 
| 107 | 106 | a1i 11 | . . . . . 6
⊢ (𝜑 → (;10↑7) ∈ ℝ) | 
| 108 | 51, 107 | remulcld 11292 | . . . . 5
⊢ (𝜑 → ((0._0_0_01)
· (;10↑7)) ∈
ℝ) | 
| 109 | 103 | nn0rei 12539 | . . . . . . . . . . 11
⊢ ;10 ∈ ℝ | 
| 110 |  | 0z 12626 | . . . . . . . . . . 11
⊢ 0 ∈
ℤ | 
| 111 |  | 3z 12652 | . . . . . . . . . . 11
⊢ 3 ∈
ℤ | 
| 112 | 109, 110,
111 | 3pm3.2i 1339 | . . . . . . . . . 10
⊢ (;10 ∈ ℝ ∧ 0 ∈
ℤ ∧ 3 ∈ ℤ) | 
| 113 |  | 1lt10 12874 | . . . . . . . . . . 11
⊢ 1 <
;10 | 
| 114 |  | 3pos 12372 | . . . . . . . . . . 11
⊢ 0 <
3 | 
| 115 | 113, 114 | pm3.2i 470 | . . . . . . . . . 10
⊢ (1 <
;10 ∧ 0 <
3) | 
| 116 |  | ltexp2a 14207 | . . . . . . . . . 10
⊢ (((;10 ∈ ℝ ∧ 0 ∈
ℤ ∧ 3 ∈ ℤ) ∧ (1 < ;10 ∧ 0 < 3)) → (;10↑0) < (;10↑3)) | 
| 117 | 112, 115,
116 | mp2an 692 | . . . . . . . . 9
⊢ (;10↑0) < (;10↑3) | 
| 118 | 103 | numexp0 17114 | . . . . . . . . . 10
⊢ (;10↑0) = 1 | 
| 119 | 118 | eqcomi 2745 | . . . . . . . . 9
⊢ 1 =
(;10↑0) | 
| 120 | 109 | recni 11276 | . . . . . . . . . . 11
⊢ ;10 ∈ ℂ | 
| 121 |  | 10pos 12752 | . . . . . . . . . . . 12
⊢ 0 <
;10 | 
| 122 | 38, 121 | gtneii 11374 | . . . . . . . . . . 11
⊢ ;10 ≠ 0 | 
| 123 |  | 4z 12653 | . . . . . . . . . . 11
⊢ 4 ∈
ℤ | 
| 124 |  | expm1 14154 | . . . . . . . . . . 11
⊢ ((;10 ∈ ℂ ∧ ;10 ≠ 0 ∧ 4 ∈ ℤ)
→ (;10↑(4 − 1)) =
((;10↑4) / ;10)) | 
| 125 | 120, 122,
123, 124 | mp3an 1462 | . . . . . . . . . 10
⊢ (;10↑(4 − 1)) = ((;10↑4) / ;10) | 
| 126 |  | 4m1e3 12396 | . . . . . . . . . . 11
⊢ (4
− 1) = 3 | 
| 127 | 126 | oveq2i 7443 | . . . . . . . . . 10
⊢ (;10↑(4 − 1)) = (;10↑3) | 
| 128 |  | 4nn0 12547 | . . . . . . . . . . . . 13
⊢ 4 ∈
ℕ0 | 
| 129 | 103, 128 | nn0expcli 14130 | . . . . . . . . . . . 12
⊢ (;10↑4) ∈
ℕ0 | 
| 130 | 129 | nn0cni 12540 | . . . . . . . . . . 11
⊢ (;10↑4) ∈
ℂ | 
| 131 |  | divrec2 11940 | . . . . . . . . . . 11
⊢ (((;10↑4) ∈ ℂ ∧ ;10 ∈ ℂ ∧ ;10 ≠ 0) → ((;10↑4) / ;10) = ((1 / ;10) · (;10↑4))) | 
| 132 | 130, 120,
122, 131 | mp3an 1462 | . . . . . . . . . 10
⊢ ((;10↑4) / ;10) = ((1 / ;10) · (;10↑4)) | 
| 133 | 125, 127,
132 | 3eqtr3ri 2773 | . . . . . . . . 9
⊢ ((1 /
;10) · (;10↑4)) = (;10↑3) | 
| 134 | 117, 119,
133 | 3brtr4i 5172 | . . . . . . . 8
⊢ 1 <
((1 / ;10) · (;10↑4)) | 
| 135 |  | 1rp 13039 | . . . . . . . . . 10
⊢ 1 ∈
ℝ+ | 
| 136 | 135 | dp0h 32885 | . . . . . . . . 9
⊢ (0.1) =
(1 / ;10) | 
| 137 | 136 | oveq1i 7442 | . . . . . . . 8
⊢ ((0.1)
· (;10↑4)) = ((1 /
;10) · (;10↑4)) | 
| 138 | 134, 137 | breqtrri 5169 | . . . . . . 7
⊢ 1 <
((0.1) · (;10↑4)) | 
| 139 | 138 | a1i 11 | . . . . . 6
⊢ (𝜑 → 1 < ((0.1) ·
(;10↑4))) | 
| 140 |  | 4p1e5 12413 | . . . . . . . 8
⊢ (4 + 1) =
5 | 
| 141 |  | 5nn0 12548 | . . . . . . . . 9
⊢ 5 ∈
ℕ0 | 
| 142 | 141 | nn0zi 12644 | . . . . . . . 8
⊢ 5 ∈
ℤ | 
| 143 | 37, 135, 140, 123, 142 | dpexpp1 32891 | . . . . . . 7
⊢ ((0.1)
· (;10↑4)) = ((0._01) · (;10↑5)) | 
| 144 | 37, 135 | rpdp2cl 32865 | . . . . . . . 8
⊢ _01 ∈
ℝ+ | 
| 145 |  | 5p1e6 12414 | . . . . . . . 8
⊢ (5 + 1) =
6 | 
| 146 |  | 6nn0 12549 | . . . . . . . . 9
⊢ 6 ∈
ℕ0 | 
| 147 | 146 | nn0zi 12644 | . . . . . . . 8
⊢ 6 ∈
ℤ | 
| 148 | 37, 144, 145, 142, 147 | dpexpp1 32891 | . . . . . . 7
⊢ ((0._01) · (;10↑5)) = ((0._0_01)
· (;10↑6)) | 
| 149 | 37, 144 | rpdp2cl 32865 | . . . . . . . 8
⊢ _0_01 ∈ ℝ+ | 
| 150 |  | 6p1e7 12415 | . . . . . . . 8
⊢ (6 + 1) =
7 | 
| 151 | 104 | nn0zi 12644 | . . . . . . . 8
⊢ 7 ∈
ℤ | 
| 152 | 37, 149, 150, 147, 151 | dpexpp1 32891 | . . . . . . 7
⊢ ((0._0_01) · (;10↑6)) = ((0._0_0_01)
· (;10↑7)) | 
| 153 | 143, 148,
152 | 3eqtrri 2769 | . . . . . 6
⊢ ((0._0_0_01)
· (;10↑7)) = ((0.1)
· (;10↑4)) | 
| 154 | 139, 153 | breqtrrdi 5184 | . . . . 5
⊢ (𝜑 → 1 < ((0._0_0_01)
· (;10↑7))) | 
| 155 | 37, 149 | rpdp2cl 32865 | . . . . . . . 8
⊢ _0_0_01
∈ ℝ+ | 
| 156 | 37, 155 | rpdpcl 32886 | . . . . . . 7
⊢ (0._0_0_01)
∈ ℝ+ | 
| 157 | 156 | a1i 11 | . . . . . 6
⊢ (𝜑 → (0._0_0_01)
∈ ℝ+) | 
| 158 |  | 2nn0 12545 | . . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 | 
| 159 | 158, 104 | deccl 12750 | . . . . . . . . . . 11
⊢ ;27 ∈
ℕ0 | 
| 160 | 103, 159 | nn0expcli 14130 | . . . . . . . . . 10
⊢ (;10↑;27) ∈ ℕ0 | 
| 161 | 160 | nn0rei 12539 | . . . . . . . . 9
⊢ (;10↑;27) ∈ ℝ | 
| 162 | 161 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (;10↑;27) ∈ ℝ) | 
| 163 | 160 | nn0ge0i 12555 | . . . . . . . . 9
⊢ 0 ≤
(;10↑;27) | 
| 164 | 163 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ (;10↑;27)) | 
| 165 | 162, 164 | resqrtcld 15457 | . . . . . . 7
⊢ (𝜑 → (√‘(;10↑;27)) ∈ ℝ) | 
| 166 |  | expmul 14149 | . . . . . . . . . . . . 13
⊢ ((;10 ∈ ℂ ∧ 7 ∈
ℕ0 ∧ 2 ∈ ℕ0) → (;10↑(7 · 2)) = ((;10↑7)↑2)) | 
| 167 | 120, 104,
158, 166 | mp3an 1462 | . . . . . . . . . . . 12
⊢ (;10↑(7 · 2)) = ((;10↑7)↑2) | 
| 168 |  | 7t2e14 12844 | . . . . . . . . . . . . 13
⊢ (7
· 2) = ;14 | 
| 169 | 168 | oveq2i 7443 | . . . . . . . . . . . 12
⊢ (;10↑(7 · 2)) = (;10↑;14) | 
| 170 | 167, 169 | eqtr3i 2766 | . . . . . . . . . . 11
⊢ ((;10↑7)↑2) = (;10↑;14) | 
| 171 | 170 | fveq2i 6908 | . . . . . . . . . 10
⊢
(√‘((;10↑7)↑2)) = (√‘(;10↑;14)) | 
| 172 |  | expgt0 14137 | . . . . . . . . . . . . 13
⊢ ((;10 ∈ ℝ ∧ 7 ∈
ℤ ∧ 0 < ;10) → 0
< (;10↑7)) | 
| 173 | 109, 151,
121, 172 | mp3an 1462 | . . . . . . . . . . . 12
⊢ 0 <
(;10↑7) | 
| 174 | 38, 106, 173 | ltleii 11385 | . . . . . . . . . . 11
⊢ 0 ≤
(;10↑7) | 
| 175 |  | sqrtsq 15309 | . . . . . . . . . . 11
⊢ (((;10↑7) ∈ ℝ ∧ 0 ≤
(;10↑7)) →
(√‘((;10↑7)↑2)) = (;10↑7)) | 
| 176 | 106, 174,
175 | mp2an 692 | . . . . . . . . . 10
⊢
(√‘((;10↑7)↑2)) = (;10↑7) | 
| 177 | 171, 176 | eqtr3i 2766 | . . . . . . . . 9
⊢
(√‘(;10↑;14)) = (;10↑7) | 
| 178 | 15, 128 | deccl 12750 | . . . . . . . . . . . . 13
⊢ ;14 ∈
ℕ0 | 
| 179 | 178 | nn0zi 12644 | . . . . . . . . . . . 12
⊢ ;14 ∈ ℤ | 
| 180 | 159 | nn0zi 12644 | . . . . . . . . . . . 12
⊢ ;27 ∈ ℤ | 
| 181 | 109, 179,
180 | 3pm3.2i 1339 | . . . . . . . . . . 11
⊢ (;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ) | 
| 182 |  | 4lt10 12871 | . . . . . . . . . . . . 13
⊢ 4 <
;10 | 
| 183 |  | 1lt2 12438 | . . . . . . . . . . . . 13
⊢ 1 <
2 | 
| 184 | 15, 158, 128, 104, 182, 183 | decltc 12764 | . . . . . . . . . . . 12
⊢ ;14 < ;27 | 
| 185 | 113, 184 | pm3.2i 470 | . . . . . . . . . . 11
⊢ (1 <
;10 ∧ ;14 < ;27) | 
| 186 |  | ltexp2a 14207 | . . . . . . . . . . 11
⊢ (((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ ;27 ∈ ℤ) ∧ (1 < ;10 ∧ ;14 < ;27)) → (;10↑;14) < (;10↑;27)) | 
| 187 | 181, 185,
186 | mp2an 692 | . . . . . . . . . 10
⊢ (;10↑;14) < (;10↑;27) | 
| 188 | 103, 178 | nn0expcli 14130 | . . . . . . . . . . . . 13
⊢ (;10↑;14) ∈ ℕ0 | 
| 189 | 188 | nn0rei 12539 | . . . . . . . . . . . 12
⊢ (;10↑;14) ∈ ℝ | 
| 190 |  | expgt0 14137 | . . . . . . . . . . . . . 14
⊢ ((;10 ∈ ℝ ∧ ;14 ∈ ℤ ∧ 0 < ;10) → 0 < (;10↑;14)) | 
| 191 | 109, 179,
121, 190 | mp3an 1462 | . . . . . . . . . . . . 13
⊢ 0 <
(;10↑;14) | 
| 192 | 38, 189, 191 | ltleii 11385 | . . . . . . . . . . . 12
⊢ 0 ≤
(;10↑;14) | 
| 193 | 189, 192 | pm3.2i 470 | . . . . . . . . . . 11
⊢ ((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14)) | 
| 194 | 161, 163 | pm3.2i 470 | . . . . . . . . . . 11
⊢ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27)) | 
| 195 |  | sqrtlt 15301 | . . . . . . . . . . 11
⊢ ((((;10↑;14) ∈ ℝ ∧ 0 ≤ (;10↑;14)) ∧ ((;10↑;27) ∈ ℝ ∧ 0 ≤ (;10↑;27))) → ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27)))) | 
| 196 | 193, 194,
195 | mp2an 692 | . . . . . . . . . 10
⊢ ((;10↑;14) < (;10↑;27) ↔ (√‘(;10↑;14)) < (√‘(;10↑;27))) | 
| 197 | 187, 196 | mpbi 230 | . . . . . . . . 9
⊢
(√‘(;10↑;14)) < (√‘(;10↑;27)) | 
| 198 | 177, 197 | eqbrtrri 5165 | . . . . . . . 8
⊢ (;10↑7) < (√‘(;10↑;27)) | 
| 199 | 198 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (;10↑7) < (√‘(;10↑;27))) | 
| 200 |  | hgt750lemd.0 | . . . . . . . 8
⊢ (𝜑 → (;10↑;27) ≤ 𝑁) | 
| 201 | 162, 164,
32, 34 | sqrtled 15466 | . . . . . . . 8
⊢ (𝜑 → ((;10↑;27) ≤ 𝑁 ↔ (√‘(;10↑;27)) ≤ (√‘𝑁))) | 
| 202 | 200, 201 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (√‘(;10↑;27)) ≤ (√‘𝑁)) | 
| 203 | 107, 165,
35, 199, 202 | ltletrd 11422 | . . . . . 6
⊢ (𝜑 → (;10↑7) < (√‘𝑁)) | 
| 204 | 107, 35, 157, 203 | ltmul2dd 13134 | . . . . 5
⊢ (𝜑 → ((0._0_0_01)
· (;10↑7)) <
((0._0_0_01)
· (√‘𝑁))) | 
| 205 | 100, 108,
52, 154, 204 | lttrd 11423 | . . . 4
⊢ (𝜑 → 1 < ((0._0_0_01)
· (√‘𝑁))) | 
| 206 | 14, 100, 52, 102, 205 | lttrd 11423 | . . 3
⊢ (𝜑 → (log‘2) <
((0._0_0_01)
· (√‘𝑁))) | 
| 207 | 11, 14, 36, 52, 99, 206 | lt2addd 11887 | . 2
⊢ (𝜑 → (Σ𝑖 ∈ ((1...𝑁) ∖ ℙ)(Λ‘𝑖) + (log‘2)) <
(((1._4_2_62)
· (√‘𝑁))
+ ((0._0_0_01)
· (√‘𝑁)))) | 
| 208 |  | nfv 1913 | . . 3
⊢
Ⅎ𝑖𝜑 | 
| 209 |  | nfcv 2904 | . . 3
⊢
Ⅎ𝑖(log‘2) | 
| 210 |  | 2prm 16730 | . . . 4
⊢ 2 ∈
ℙ | 
| 211 | 210 | a1i 11 | . . 3
⊢ (𝜑 → 2 ∈
ℙ) | 
| 212 |  | elndif 4132 | . . . 4
⊢ (2 ∈
ℙ → ¬ 2 ∈ ((1...𝑁) ∖ ℙ)) | 
| 213 | 211, 212 | syl 17 | . . 3
⊢ (𝜑 → ¬ 2 ∈ ((1...𝑁) ∖
ℙ)) | 
| 214 |  | fveq2 6905 | . . . 4
⊢ (𝑖 = 2 →
(Λ‘𝑖) =
(Λ‘2)) | 
| 215 |  | vmaprm 27161 | . . . . 5
⊢ (2 ∈
ℙ → (Λ‘2) = (log‘2)) | 
| 216 | 210, 215 | ax-mp 5 | . . . 4
⊢
(Λ‘2) = (log‘2) | 
| 217 | 214, 216 | eqtrdi 2792 | . . 3
⊢ (𝑖 = 2 →
(Λ‘𝑖) =
(log‘2)) | 
| 218 |  | 2cnd 12345 | . . . 4
⊢ (𝜑 → 2 ∈
ℂ) | 
| 219 |  | 2ne0 12371 | . . . . 5
⊢ 2 ≠
0 | 
| 220 | 219 | a1i 11 | . . . 4
⊢ (𝜑 → 2 ≠ 0) | 
| 221 | 218, 220 | logcld 26613 | . . 3
⊢ (𝜑 → (log‘2) ∈
ℂ) | 
| 222 | 208, 209,
3, 211, 213, 76, 217, 221 | fsumsplitsn 15781 | . 2
⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖) =
(Σ𝑖 ∈
((1...𝑁) ∖
ℙ)(Λ‘𝑖)
+ (log‘2))) | 
| 223 | 146, 12 | rpdp2cl 32865 | . . . . . 6
⊢ _62 ∈
ℝ+ | 
| 224 | 158, 223 | rpdp2cl 32865 | . . . . 5
⊢ _2_62 ∈ ℝ+ | 
| 225 |  | 3rp 13041 | . . . . . . 7
⊢ 3 ∈
ℝ+ | 
| 226 | 146, 225 | rpdp2cl 32865 | . . . . . 6
⊢ _63 ∈
ℝ+ | 
| 227 | 158, 226 | rpdp2cl 32865 | . . . . 5
⊢ _2_63 ∈ ℝ+ | 
| 228 |  | 1p0e1 12391 | . . . . 5
⊢ (1 + 0) =
1 | 
| 229 |  | 4cn 12352 | . . . . . . 7
⊢ 4 ∈
ℂ | 
| 230 | 229 | addridi 11449 | . . . . . 6
⊢ (4 + 0) =
4 | 
| 231 |  | 2cn 12342 | . . . . . . . 8
⊢ 2 ∈
ℂ | 
| 232 | 231 | addridi 11449 | . . . . . . 7
⊢ (2 + 0) =
2 | 
| 233 |  | 3nn0 12546 | . . . . . . . 8
⊢ 3 ∈
ℕ0 | 
| 234 |  | eqid 2736 | . . . . . . . . 9
⊢ ;62 = ;62 | 
| 235 |  | eqid 2736 | . . . . . . . . 9
⊢ ;01 = ;01 | 
| 236 |  | 6cn 12358 | . . . . . . . . . 10
⊢ 6 ∈
ℂ | 
| 237 | 236 | addridi 11449 | . . . . . . . . 9
⊢ (6 + 0) =
6 | 
| 238 |  | 2p1e3 12409 | . . . . . . . . 9
⊢ (2 + 1) =
3 | 
| 239 | 146, 158,
37, 15, 234, 235, 237, 238 | decadd 12789 | . . . . . . . 8
⊢ (;62 + ;01) = ;63 | 
| 240 | 146, 158,
37, 15, 146, 233, 239 | dpadd 32894 | . . . . . . 7
⊢ ((6.2) +
(0.1)) = (6.3) | 
| 241 | 146, 12, 37, 135, 146, 225, 158, 37, 232, 240 | dpadd2 32893 | . . . . . 6
⊢ ((2._62) + (0._01)) = (2._63) | 
| 242 | 158, 223,
37, 144, 158, 226, 128, 37, 230, 241 | dpadd2 32893 | . . . . 5
⊢ ((4._2_62) + (0._0_01))
= (4._2_63) | 
| 243 | 128, 224,
37, 149, 128, 227, 15, 37, 228, 242 | dpadd2 32893 | . . . 4
⊢ ((1._4_2_62) +
(0._0_0_01))
= (1._4_2_63) | 
| 244 | 243 | oveq1i 7442 | . . 3
⊢
(((1._4_2_62) +
(0._0_0_01))
· (√‘𝑁))
= ((1._4_2_63)
· (√‘𝑁)) | 
| 245 | 30 | recnd 11290 | . . . 4
⊢ (𝜑 → (1._4_2_62)
∈ ℂ) | 
| 246 | 51 | recnd 11290 | . . . 4
⊢ (𝜑 → (0._0_0_01)
∈ ℂ) | 
| 247 | 35 | recnd 11290 | . . . 4
⊢ (𝜑 → (√‘𝑁) ∈
ℂ) | 
| 248 | 245, 246,
247 | adddird 11287 | . . 3
⊢ (𝜑 → (((1._4_2_62) +
(0._0_0_01))
· (√‘𝑁))
= (((1._4_2_62)
· (√‘𝑁))
+ ((0._0_0_01)
· (√‘𝑁)))) | 
| 249 | 244, 248 | eqtr3id 2790 | . 2
⊢ (𝜑 → ((1._4_2_63)
· (√‘𝑁))
= (((1._4_2_62)
· (√‘𝑁))
+ ((0._0_0_01)
· (√‘𝑁)))) | 
| 250 | 207, 222,
249 | 3brtr4d 5174 | 1
⊢ (𝜑 → Σ𝑖 ∈ (((1...𝑁) ∖ ℙ) ∪
{2})(Λ‘𝑖) <
((1._4_2_63)
· (√‘𝑁))) |