Metamath Proof Explorer

Theorem hgt750lemd

Description: An upper bound to the summatory function of the von Mangoldt function on non-primes. (Contributed by Thierry Arnoux, 29-Dec-2021)

Ref Expression
Hypotheses hgt750lemc.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
hgt750lemd.0 ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
Assertion hgt750lemd ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) < ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 hgt750lemc.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 hgt750lemd.0 ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ≤ 𝑁 )
3 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
4 diffi ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin )
5 3 4 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ∈ Fin )
6 vmaf ⊢ Λ : ℕ ⟶ ℝ
7 6 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → Λ : ℕ ⟶ ℝ )
8 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
9 8 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
10 9 ssdifssd ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∖ ℙ ) ⊆ ℕ )
11 10 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → 𝑖 ∈ ℕ )
12 7 11 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
13 5 12 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℝ )
14 2rp ⊢ 2 ∈ ℝ+
15 14 a1i ⊢ ( 𝜑 → 2 ∈ ℝ+ )
16 15 relogcld ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℝ )
17 1nn0 ⊢ 1 ∈ ℕ0
18 4re ⊢ 4 ∈ ℝ
19 2re ⊢ 2 ∈ ℝ
20 6re ⊢ 6 ∈ ℝ
21 20 19 pm3.2i ⊢ ( 6 ∈ ℝ ∧ 2 ∈ ℝ )
22 dp2cl ⊢ ( ( 6 ∈ ℝ ∧ 2 ∈ ℝ ) → 6 2 ∈ ℝ )
23 21 22 ax-mp ⊢ 6 2 ∈ ℝ
24 19 23 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 6 2 ∈ ℝ )
25 dp2cl ⊢ ( ( 2 ∈ ℝ ∧ 6 2 ∈ ℝ ) → 2 6 2 ∈ ℝ )
26 24 25 ax-mp ⊢ 2 6 2 ∈ ℝ
27 18 26 pm3.2i ⊢ ( 4 ∈ ℝ ∧ 2 6 2 ∈ ℝ )
28 dp2cl ⊢ ( ( 4 ∈ ℝ ∧ 2 6 2 ∈ ℝ ) → 4 2 6 2 ∈ ℝ )
29 27 28 ax-mp ⊢ 4 2 6 2 ∈ ℝ
30 dpcl ⊢ ( ( 1 ∈ ℕ0 ∧ 4 2 6 2 ∈ ℝ ) → ( 1 . 4 2 6 2 ) ∈ ℝ )
31 17 29 30 mp2an ⊢ ( 1 . 4 2 6 2 ) ∈ ℝ
32 31 a1i ⊢ ( 𝜑 → ( 1 . 4 2 6 2 ) ∈ ℝ )
33 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
34 1 nnrpd ⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
35 34 rpge0d ⊢ ( 𝜑 → 0 ≤ 𝑁 )
36 33 35 resqrtcld ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ )
37 32 36 remulcld ⊢ ( 𝜑 → ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
38 0nn0 ⊢ 0 ∈ ℕ0
39 0re ⊢ 0 ∈ ℝ
40 1re ⊢ 1 ∈ ℝ
41 39 40 pm3.2i ⊢ ( 0 ∈ ℝ ∧ 1 ∈ ℝ )
42 dp2cl ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → 0 1 ∈ ℝ )
43 41 42 ax-mp ⊢ 0 1 ∈ ℝ
44 39 43 pm3.2i ⊢ ( 0 ∈ ℝ ∧ 0 1 ∈ ℝ )
45 dp2cl ⊢ ( ( 0 ∈ ℝ ∧ 0 1 ∈ ℝ ) → 0 0 1 ∈ ℝ )
46 44 45 ax-mp ⊢ 0 0 1 ∈ ℝ
47 39 46 pm3.2i ⊢ ( 0 ∈ ℝ ∧ 0 0 1 ∈ ℝ )
48 dp2cl ⊢ ( ( 0 ∈ ℝ ∧ 0 0 1 ∈ ℝ ) → 0 0 0 1 ∈ ℝ )
49 47 48 ax-mp ⊢ 0 0 0 1 ∈ ℝ
50 dpcl ⊢ ( ( 0 ∈ ℕ0 ∧ 0 0 0 1 ∈ ℝ ) → ( 0 . 0 0 0 1 ) ∈ ℝ )
51 38 49 50 mp2an ⊢ ( 0 . 0 0 0 1 ) ∈ ℝ
52 51 a1i ⊢ ( 𝜑 → ( 0 . 0 0 0 1 ) ∈ ℝ )
53 52 36 remulcld ⊢ ( 𝜑 → ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
54 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
55 chpvalz ⊢ ( 𝑁 ∈ ℤ → ( ψ ‘ 𝑁 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) )
56 54 55 syl ⊢ ( 𝜑 → ( ψ ‘ 𝑁 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) )
57 chtvalz ⊢ ( 𝑁 ∈ ℤ → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) )
58 54 57 syl ⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) )
59 inss2 ⊢ ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℙ
60 59 a1i ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℙ )
61 60 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → 𝑖 ∈ ℙ )
62 vmaprm ⊢ ( 𝑖 ∈ ℙ → ( Λ ‘ 𝑖 ) = ( log ‘ 𝑖 ) )
63 61 62 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) = ( log ‘ 𝑖 ) )
64 63 sumeq2dv ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( log ‘ 𝑖 ) )
65 58 64 eqtr4d ⊢ ( 𝜑 → ( θ ‘ 𝑁 ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) )
66 56 65 oveq12d ⊢ ( 𝜑 → ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) − Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ) )
67 infi ⊢ ( ( 1 ... 𝑁 ) ∈ Fin → ( ( 1 ... 𝑁 ) ∩ ℙ ) ∈ Fin )
68 3 67 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ∈ Fin )
69 6 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → Λ : ℕ ⟶ ℝ )
70 inss1 ⊢ ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ( 1 ... 𝑁 )
71 70 8 sstri ⊢ ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℕ
72 71 a1i ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ∩ ℙ ) ⊆ ℕ )
73 72 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → 𝑖 ∈ ℕ )
74 69 73 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
75 74 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
76 68 75 fsumcl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℂ )
77 12 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
78 5 77 fsumcl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ∈ ℂ )
79 inindif ⊢ ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∩ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ∅
80 79 a1i ⊢ ( 𝜑 → ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∩ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ∅ )
81 inundif ⊢ ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) = ( 1 ... 𝑁 )
82 81 eqcomi ⊢ ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
83 82 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) = ( ( ( 1 ... 𝑁 ) ∩ ℙ ) ∪ ( ( 1 ... 𝑁 ) ∖ ℙ ) ) )
84 6 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → Λ : ℕ ⟶ ℝ )
85 9 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ℕ )
86 84 85 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑖 ) ∈ ℝ )
87 86 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( Λ ‘ 𝑖 ) ∈ ℂ )
88 80 83 3 87 fsumsplit ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) ) )
89 76 78 88 mvrladdd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( Λ ‘ 𝑖 ) − Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∩ ℙ ) ( Λ ‘ 𝑖 ) ) = Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) )
90 66 89 eqtr2d ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) = ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) )
91 fveq2 ⊢ ( 𝑥 = 𝑁 → ( ψ ‘ 𝑥 ) = ( ψ ‘ 𝑁 ) )
92 fveq2 ⊢ ( 𝑥 = 𝑁 → ( θ ‘ 𝑥 ) = ( θ ‘ 𝑁 ) )
93 91 92 oveq12d ⊢ ( 𝑥 = 𝑁 → ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) = ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) )
94 fveq2 ⊢ ( 𝑥 = 𝑁 → ( √ ‘ 𝑥 ) = ( √ ‘ 𝑁 ) )
95 94 oveq2d ⊢ ( 𝑥 = 𝑁 → ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑥 ) ) = ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) )
96 93 95 breq12d ⊢ ( 𝑥 = 𝑁 → ( ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑥 ) ) ↔ ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) ) )
97 ax-ros336 ⊢ ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑥 ) )
98 97 a1i ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ( ( ψ ‘ 𝑥 ) − ( θ ‘ 𝑥 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑥 ) ) )
99 96 98 34 rspcdva ⊢ ( 𝜑 → ( ( ψ ‘ 𝑁 ) − ( θ ‘ 𝑁 ) ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) )
100 90 99 eqbrtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) < ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) )
101 40 a1i ⊢ ( 𝜑 → 1 ∈ ℝ )
102 log2le1 ⊢ ( log ‘ 2 ) < 1
103 102 a1i ⊢ ( 𝜑 → ( log ‘ 2 ) < 1 )
104 10nn0 ⊢ 1 0 ∈ ℕ0
105 7nn0 ⊢ 7 ∈ ℕ0
106 104 105 nn0expcli ⊢ ( 1 0 ↑ 7 ) ∈ ℕ0
107 106 nn0rei ⊢ ( 1 0 ↑ 7 ) ∈ ℝ
108 107 a1i ⊢ ( 𝜑 → ( 1 0 ↑ 7 ) ∈ ℝ )
109 52 108 remulcld ⊢ ( 𝜑 → ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) ) ∈ ℝ )
110 104 nn0rei ⊢ 1 0 ∈ ℝ
111 0z ⊢ 0 ∈ ℤ
112 3z ⊢ 3 ∈ ℤ
113 110 111 112 3pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ )
114 1lt10 ⊢ 1 < 1 0
115 3pos ⊢ 0 < 3
116 114 115 pm3.2i ⊢ ( 1 < 1 0 ∧ 0 < 3 )
117 ltexp2a ⊢ ( ( ( 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ 3 ∈ ℤ ) ∧ ( 1 < 1 0 ∧ 0 < 3 ) ) → ( 1 0 ↑ 0 ) < ( 1 0 ↑ 3 ) )
118 113 116 117 mp2an ⊢ ( 1 0 ↑ 0 ) < ( 1 0 ↑ 3 )
119 104 numexp0 ⊢ ( 1 0 ↑ 0 ) = 1
120 119 eqcomi ⊢ 1 = ( 1 0 ↑ 0 )
121 110 recni ⊢ 1 0 ∈ ℂ
122 10pos ⊢ 0 < 1 0
123 39 122 gtneii ⊢ 1 0 ≠ 0
124 4z ⊢ 4 ∈ ℤ
125 expm1 ⊢ ( ( 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ∧ 4 ∈ ℤ ) → ( 1 0 ↑ ( 4 − 1 ) ) = ( ( 1 0 ↑ 4 ) / 1 0 ) )
126 121 123 124 125 mp3an ⊢ ( 1 0 ↑ ( 4 − 1 ) ) = ( ( 1 0 ↑ 4 ) / 1 0 )
127 4m1e3 ⊢ ( 4 − 1 ) = 3
128 127 oveq2i ⊢ ( 1 0 ↑ ( 4 − 1 ) ) = ( 1 0 ↑ 3 )
129 4nn0 ⊢ 4 ∈ ℕ0
130 104 129 nn0expcli ⊢ ( 1 0 ↑ 4 ) ∈ ℕ0
131 130 nn0cni ⊢ ( 1 0 ↑ 4 ) ∈ ℂ
132 divrec2 ⊢ ( ( ( 1 0 ↑ 4 ) ∈ ℂ ∧ 1 0 ∈ ℂ ∧ 1 0 ≠ 0 ) → ( ( 1 0 ↑ 4 ) / 1 0 ) = ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) ) )
133 131 121 123 132 mp3an ⊢ ( ( 1 0 ↑ 4 ) / 1 0 ) = ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) )
134 126 128 133 3eqtr3ri ⊢ ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) ) = ( 1 0 ↑ 3 )
135 118 120 134 3brtr4i ⊢ 1 < ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) )
136 1rp ⊢ 1 ∈ ℝ+
137 136 dp0h ⊢ ( 0 . 1 ) = ( 1 / 1 0 )
138 137 oveq1i ⊢ ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) ) = ( ( 1 / 1 0 ) · ( 1 0 ↑ 4 ) )
139 135 138 breqtrri ⊢ 1 < ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) )
140 139 a1i ⊢ ( 𝜑 → 1 < ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) ) )
141 4p1e5 ⊢ ( 4 + 1 ) = 5
142 5nn0 ⊢ 5 ∈ ℕ0
143 142 nn0zi ⊢ 5 ∈ ℤ
144 38 136 141 124 143 dpexpp1 ⊢ ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) ) = ( ( 0 . 0 1 ) · ( 1 0 ↑ 5 ) )
145 38 136 rpdp2cl ⊢ 0 1 ∈ ℝ+
146 5p1e6 ⊢ ( 5 + 1 ) = 6
147 6nn0 ⊢ 6 ∈ ℕ0
148 147 nn0zi ⊢ 6 ∈ ℤ
149 38 145 146 143 148 dpexpp1 ⊢ ( ( 0 . 0 1 ) · ( 1 0 ↑ 5 ) ) = ( ( 0 . 0 0 1 ) · ( 1 0 ↑ 6 ) )
150 38 145 rpdp2cl ⊢ 0 0 1 ∈ ℝ+
151 6p1e7 ⊢ ( 6 + 1 ) = 7
152 105 nn0zi ⊢ 7 ∈ ℤ
153 38 150 151 148 152 dpexpp1 ⊢ ( ( 0 . 0 0 1 ) · ( 1 0 ↑ 6 ) ) = ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) )
154 144 149 153 3eqtrri ⊢ ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) ) = ( ( 0 . 1 ) · ( 1 0 ↑ 4 ) )
155 140 154 breqtrrdi ⊢ ( 𝜑 → 1 < ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) ) )
156 38 150 rpdp2cl ⊢ 0 0 0 1 ∈ ℝ+
157 38 156 rpdpcl ⊢ ( 0 . 0 0 0 1 ) ∈ ℝ+
158 157 a1i ⊢ ( 𝜑 → ( 0 . 0 0 0 1 ) ∈ ℝ+ )
159 2nn0 ⊢ 2 ∈ ℕ0
160 159 105 deccl ⊢ 2 7 ∈ ℕ0
161 104 160 nn0expcli ⊢ ( 1 0 ↑ 2 7 ) ∈ ℕ0
162 161 nn0rei ⊢ ( 1 0 ↑ 2 7 ) ∈ ℝ
163 162 a1i ⊢ ( 𝜑 → ( 1 0 ↑ 2 7 ) ∈ ℝ )
164 161 nn0ge0i ⊢ 0 ≤ ( 1 0 ↑ 2 7 )
165 164 a1i ⊢ ( 𝜑 → 0 ≤ ( 1 0 ↑ 2 7 ) )
166 163 165 resqrtcld ⊢ ( 𝜑 → ( √ ‘ ( 1 0 ↑ 2 7 ) ) ∈ ℝ )
167 expmul ⊢ ( ( 1 0 ∈ ℂ ∧ 7 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( 1 0 ↑ ( 7 · 2 ) ) = ( ( 1 0 ↑ 7 ) ↑ 2 ) )
168 121 105 159 167 mp3an ⊢ ( 1 0 ↑ ( 7 · 2 ) ) = ( ( 1 0 ↑ 7 ) ↑ 2 )
169 7t2e14 ⊢ ( 7 · 2 ) = 1 4
170 169 oveq2i ⊢ ( 1 0 ↑ ( 7 · 2 ) ) = ( 1 0 ↑ 1 4 )
171 168 170 eqtr3i ⊢ ( ( 1 0 ↑ 7 ) ↑ 2 ) = ( 1 0 ↑ 1 4 )
172 171 fveq2i ⊢ ( √ ‘ ( ( 1 0 ↑ 7 ) ↑ 2 ) ) = ( √ ‘ ( 1 0 ↑ 1 4 ) )
173 expgt0 ⊢ ( ( 1 0 ∈ ℝ ∧ 7 ∈ ℤ ∧ 0 < 1 0 ) → 0 < ( 1 0 ↑ 7 ) )
174 110 152 122 173 mp3an ⊢ 0 < ( 1 0 ↑ 7 )
175 39 107 174 ltleii ⊢ 0 ≤ ( 1 0 ↑ 7 )
176 sqrtsq ⊢ ( ( ( 1 0 ↑ 7 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 7 ) ) → ( √ ‘ ( ( 1 0 ↑ 7 ) ↑ 2 ) ) = ( 1 0 ↑ 7 ) )
177 107 175 176 mp2an ⊢ ( √ ‘ ( ( 1 0 ↑ 7 ) ↑ 2 ) ) = ( 1 0 ↑ 7 )
178 172 177 eqtr3i ⊢ ( √ ‘ ( 1 0 ↑ 1 4 ) ) = ( 1 0 ↑ 7 )
179 17 129 deccl ⊢ 1 4 ∈ ℕ0
180 179 nn0zi ⊢ 1 4 ∈ ℤ
181 160 nn0zi ⊢ 2 7 ∈ ℤ
182 110 180 181 3pm3.2i ⊢ ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℤ ∧ 2 7 ∈ ℤ )
183 4lt10 ⊢ 4 < 1 0
184 1lt2 ⊢ 1 < 2
185 17 159 129 105 183 184 decltc ⊢ 1 4 < 2 7
186 114 185 pm3.2i ⊢ ( 1 < 1 0 ∧ 1 4 < 2 7 )
187 ltexp2a ⊢ ( ( ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℤ ∧ 2 7 ∈ ℤ ) ∧ ( 1 < 1 0 ∧ 1 4 < 2 7 ) ) → ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 ) )
188 182 186 187 mp2an ⊢ ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 )
189 104 179 nn0expcli ⊢ ( 1 0 ↑ 1 4 ) ∈ ℕ0
190 189 nn0rei ⊢ ( 1 0 ↑ 1 4 ) ∈ ℝ
191 expgt0 ⊢ ( ( 1 0 ∈ ℝ ∧ 1 4 ∈ ℤ ∧ 0 < 1 0 ) → 0 < ( 1 0 ↑ 1 4 ) )
192 110 180 122 191 mp3an ⊢ 0 < ( 1 0 ↑ 1 4 )
193 39 190 192 ltleii ⊢ 0 ≤ ( 1 0 ↑ 1 4 )
194 190 193 pm3.2i ⊢ ( ( 1 0 ↑ 1 4 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 1 4 ) )
195 162 164 pm3.2i ⊢ ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 2 7 ) )
196 sqrtlt ⊢ ( ( ( ( 1 0 ↑ 1 4 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 1 4 ) ) ∧ ( ( 1 0 ↑ 2 7 ) ∈ ℝ ∧ 0 ≤ ( 1 0 ↑ 2 7 ) ) ) → ( ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 ) ↔ ( √ ‘ ( 1 0 ↑ 1 4 ) ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) ) )
197 194 195 196 mp2an ⊢ ( ( 1 0 ↑ 1 4 ) < ( 1 0 ↑ 2 7 ) ↔ ( √ ‘ ( 1 0 ↑ 1 4 ) ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) )
198 188 197 mpbi ⊢ ( √ ‘ ( 1 0 ↑ 1 4 ) ) < ( √ ‘ ( 1 0 ↑ 2 7 ) )
199 178 198 eqbrtrri ⊢ ( 1 0 ↑ 7 ) < ( √ ‘ ( 1 0 ↑ 2 7 ) )
200 199 a1i ⊢ ( 𝜑 → ( 1 0 ↑ 7 ) < ( √ ‘ ( 1 0 ↑ 2 7 ) ) )
201 163 165 33 35 sqrtled ⊢ ( 𝜑 → ( ( 1 0 ↑ 2 7 ) ≤ 𝑁 ↔ ( √ ‘ ( 1 0 ↑ 2 7 ) ) ≤ ( √ ‘ 𝑁 ) ) )
202 2 201 mpbid ⊢ ( 𝜑 → ( √ ‘ ( 1 0 ↑ 2 7 ) ) ≤ ( √ ‘ 𝑁 ) )
203 108 166 36 200 202 ltletrd ⊢ ( 𝜑 → ( 1 0 ↑ 7 ) < ( √ ‘ 𝑁 ) )
204 108 36 158 203 ltmul2dd ⊢ ( 𝜑 → ( ( 0 . 0 0 0 1 ) · ( 1 0 ↑ 7 ) ) < ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) )
205 101 109 53 155 204 lttrd ⊢ ( 𝜑 → 1 < ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) )
206 16 101 53 103 205 lttrd ⊢ ( 𝜑 → ( log ‘ 2 ) < ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) )
207 13 16 37 53 100 206 lt2addd ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) + ( log ‘ 2 ) ) < ( ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) ) )
208 nfv ⊢ Ⅎ 𝑖 𝜑
209 nfcv ⊢ Ⅎ 𝑖 ( log ‘ 2 )
210 2prm ⊢ 2 ∈ ℙ
211 210 a1i ⊢ ( 𝜑 → 2 ∈ ℙ )
212 elndif ⊢ ( 2 ∈ ℙ → ¬ 2 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
213 211 212 syl ⊢ ( 𝜑 → ¬ 2 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) )
214 fveq2 ⊢ ( 𝑖 = 2 → ( Λ ‘ 𝑖 ) = ( Λ ‘ 2 ) )
215 vmaprm ⊢ ( 2 ∈ ℙ → ( Λ ‘ 2 ) = ( log ‘ 2 ) )
216 210 215 ax-mp ⊢ ( Λ ‘ 2 ) = ( log ‘ 2 )
217 214 216 eqtrdi ⊢ ( 𝑖 = 2 → ( Λ ‘ 𝑖 ) = ( log ‘ 2 ) )
218 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
219 2ne0 ⊢ 2 ≠ 0
220 219 a1i ⊢ ( 𝜑 → 2 ≠ 0 )
221 218 220 logcld ⊢ ( 𝜑 → ( log ‘ 2 ) ∈ ℂ )
222 208 209 5 211 213 77 217 221 fsumsplitsn ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( ( 1 ... 𝑁 ) ∖ ℙ ) ( Λ ‘ 𝑖 ) + ( log ‘ 2 ) ) )
223 147 14 rpdp2cl ⊢ 6 2 ∈ ℝ+
224 159 223 rpdp2cl ⊢ 2 6 2 ∈ ℝ+
225 3rp ⊢ 3 ∈ ℝ+
226 147 225 rpdp2cl ⊢ 6 3 ∈ ℝ+
227 159 226 rpdp2cl ⊢ 2 6 3 ∈ ℝ+
228 1p0e1 ⊢ ( 1 + 0 ) = 1
229 4cn ⊢ 4 ∈ ℂ
230 229 addridi ⊢ ( 4 + 0 ) = 4
231 2cn ⊢ 2 ∈ ℂ
232 231 addridi ⊢ ( 2 + 0 ) = 2
233 3nn0 ⊢ 3 ∈ ℕ0
234 eqid ⊢ 6 2 = 6 2
235 eqid ⊢ 0 1 = 0 1
236 6cn ⊢ 6 ∈ ℂ
237 236 addridi ⊢ ( 6 + 0 ) = 6
238 2p1e3 ⊢ ( 2 + 1 ) = 3
239 147 159 38 17 234 235 237 238 decadd ⊢ ( 6 2 + 0 1 ) = 6 3
240 147 159 38 17 147 233 239 dpadd ⊢ ( ( 6 . 2 ) + ( 0 . 1 ) ) = ( 6 . 3 )
241 147 14 38 136 147 225 159 38 232 240 dpadd2 ⊢ ( ( 2 . 6 2 ) + ( 0 . 0 1 ) ) = ( 2 . 6 3 )
242 159 223 38 145 159 226 129 38 230 241 dpadd2 ⊢ ( ( 4 . 2 6 2 ) + ( 0 . 0 0 1 ) ) = ( 4 . 2 6 3 )
243 129 224 38 150 129 227 17 38 228 242 dpadd2 ⊢ ( ( 1 . 4 2 6 2 ) + ( 0 . 0 0 0 1 ) ) = ( 1 . 4 2 6 3 )
244 243 oveq1i ⊢ ( ( ( 1 . 4 2 6 2 ) + ( 0 . 0 0 0 1 ) ) · ( √ ‘ 𝑁 ) ) = ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) )
245 32 recnd ⊢ ( 𝜑 → ( 1 . 4 2 6 2 ) ∈ ℂ )
246 52 recnd ⊢ ( 𝜑 → ( 0 . 0 0 0 1 ) ∈ ℂ )
247 36 recnd ⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℂ )
248 245 246 247 adddird ⊢ ( 𝜑 → ( ( ( 1 . 4 2 6 2 ) + ( 0 . 0 0 0 1 ) ) · ( √ ‘ 𝑁 ) ) = ( ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) ) )
249 244 248 eqtr3id ⊢ ( 𝜑 → ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) = ( ( ( 1 . 4 2 6 2 ) · ( √ ‘ 𝑁 ) ) + ( ( 0 . 0 0 0 1 ) · ( √ ‘ 𝑁 ) ) ) )
250 207 222 249 3brtr4d ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( ( 1 ... 𝑁 ) ∖ ℙ ) ∪ { 2 } ) ( Λ ‘ 𝑖 ) < ( ( 1 . 4 2 6 3 ) · ( √ ‘ 𝑁 ) ) )