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
|- ( ph -> N e. NN )
hgt750lemd.0
|- ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
Assertion hgt750lemd
|- ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) < ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) )

Proof

Step Hyp Ref Expression
1 hgt750lemc.n
 |-  ( ph -> N e. NN )
2 hgt750lemd.0
 |-  ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
3 fzfid
 |-  ( ph -> ( 1 ... N ) e. Fin )
4 diffi
 |-  ( ( 1 ... N ) e. Fin -> ( ( 1 ... N ) \ Prime ) e. Fin )
5 3 4 syl
 |-  ( ph -> ( ( 1 ... N ) \ Prime ) e. Fin )
6 vmaf
 |-  Lam : NN --> RR
7 6 a1i
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ Prime ) ) -> Lam : NN --> RR )
8 fz1ssnn
 |-  ( 1 ... N ) C_ NN
9 8 a1i
 |-  ( ph -> ( 1 ... N ) C_ NN )
10 9 ssdifssd
 |-  ( ph -> ( ( 1 ... N ) \ Prime ) C_ NN )
11 10 sselda
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ Prime ) ) -> i e. NN )
12 7 11 ffvelrnd
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ Prime ) ) -> ( Lam ` i ) e. RR )
13 5 12 fsumrecl
 |-  ( ph -> sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) e. RR )
14 2rp
 |-  2 e. RR+
15 14 a1i
 |-  ( ph -> 2 e. RR+ )
16 15 relogcld
 |-  ( ph -> ( log ` 2 ) e. RR )
17 1nn0
 |-  1 e. NN0
18 4re
 |-  4 e. RR
19 2re
 |-  2 e. RR
20 6re
 |-  6 e. RR
21 20 19 pm3.2i
 |-  ( 6 e. RR /\ 2 e. RR )
22 dp2cl
 |-  ( ( 6 e. RR /\ 2 e. RR ) -> _ 6 2 e. RR )
23 21 22 ax-mp
 |-  _ 6 2 e. RR
24 19 23 pm3.2i
 |-  ( 2 e. RR /\ _ 6 2 e. RR )
25 dp2cl
 |-  ( ( 2 e. RR /\ _ 6 2 e. RR ) -> _ 2 _ 6 2 e. RR )
26 24 25 ax-mp
 |-  _ 2 _ 6 2 e. RR
27 18 26 pm3.2i
 |-  ( 4 e. RR /\ _ 2 _ 6 2 e. RR )
28 dp2cl
 |-  ( ( 4 e. RR /\ _ 2 _ 6 2 e. RR ) -> _ 4 _ 2 _ 6 2 e. RR )
29 27 28 ax-mp
 |-  _ 4 _ 2 _ 6 2 e. RR
30 dpcl
 |-  ( ( 1 e. NN0 /\ _ 4 _ 2 _ 6 2 e. RR ) -> ( 1 . _ 4 _ 2 _ 6 2 ) e. RR )
31 17 29 30 mp2an
 |-  ( 1 . _ 4 _ 2 _ 6 2 ) e. RR
32 31 a1i
 |-  ( ph -> ( 1 . _ 4 _ 2 _ 6 2 ) e. RR )
33 1 nnred
 |-  ( ph -> N e. RR )
34 1 nnrpd
 |-  ( ph -> N e. RR+ )
35 34 rpge0d
 |-  ( ph -> 0 <_ N )
36 33 35 resqrtcld
 |-  ( ph -> ( sqrt ` N ) e. RR )
37 32 36 remulcld
 |-  ( ph -> ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) e. RR )
38 0nn0
 |-  0 e. NN0
39 0re
 |-  0 e. RR
40 1re
 |-  1 e. RR
41 39 40 pm3.2i
 |-  ( 0 e. RR /\ 1 e. RR )
42 dp2cl
 |-  ( ( 0 e. RR /\ 1 e. RR ) -> _ 0 1 e. RR )
43 41 42 ax-mp
 |-  _ 0 1 e. RR
44 39 43 pm3.2i
 |-  ( 0 e. RR /\ _ 0 1 e. RR )
45 dp2cl
 |-  ( ( 0 e. RR /\ _ 0 1 e. RR ) -> _ 0 _ 0 1 e. RR )
46 44 45 ax-mp
 |-  _ 0 _ 0 1 e. RR
47 39 46 pm3.2i
 |-  ( 0 e. RR /\ _ 0 _ 0 1 e. RR )
48 dp2cl
 |-  ( ( 0 e. RR /\ _ 0 _ 0 1 e. RR ) -> _ 0 _ 0 _ 0 1 e. RR )
49 47 48 ax-mp
 |-  _ 0 _ 0 _ 0 1 e. RR
50 dpcl
 |-  ( ( 0 e. NN0 /\ _ 0 _ 0 _ 0 1 e. RR ) -> ( 0 . _ 0 _ 0 _ 0 1 ) e. RR )
51 38 49 50 mp2an
 |-  ( 0 . _ 0 _ 0 _ 0 1 ) e. RR
52 51 a1i
 |-  ( ph -> ( 0 . _ 0 _ 0 _ 0 1 ) e. RR )
53 52 36 remulcld
 |-  ( ph -> ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) e. RR )
54 1 nnzd
 |-  ( ph -> N e. ZZ )
55 chpvalz
 |-  ( N e. ZZ -> ( psi ` N ) = sum_ i e. ( 1 ... N ) ( Lam ` i ) )
56 54 55 syl
 |-  ( ph -> ( psi ` N ) = sum_ i e. ( 1 ... N ) ( Lam ` i ) )
57 chtvalz
 |-  ( N e. ZZ -> ( theta ` N ) = sum_ i e. ( ( 1 ... N ) i^i Prime ) ( log ` i ) )
58 54 57 syl
 |-  ( ph -> ( theta ` N ) = sum_ i e. ( ( 1 ... N ) i^i Prime ) ( log ` i ) )
59 inss2
 |-  ( ( 1 ... N ) i^i Prime ) C_ Prime
60 59 a1i
 |-  ( ph -> ( ( 1 ... N ) i^i Prime ) C_ Prime )
61 60 sselda
 |-  ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> i e. Prime )
62 vmaprm
 |-  ( i e. Prime -> ( Lam ` i ) = ( log ` i ) )
63 61 62 syl
 |-  ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> ( Lam ` i ) = ( log ` i ) )
64 63 sumeq2dv
 |-  ( ph -> sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) = sum_ i e. ( ( 1 ... N ) i^i Prime ) ( log ` i ) )
65 58 64 eqtr4d
 |-  ( ph -> ( theta ` N ) = sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) )
66 56 65 oveq12d
 |-  ( ph -> ( ( psi ` N ) - ( theta ` N ) ) = ( sum_ i e. ( 1 ... N ) ( Lam ` i ) - sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) ) )
67 infi
 |-  ( ( 1 ... N ) e. Fin -> ( ( 1 ... N ) i^i Prime ) e. Fin )
68 3 67 syl
 |-  ( ph -> ( ( 1 ... N ) i^i Prime ) e. Fin )
69 6 a1i
 |-  ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> Lam : NN --> RR )
70 inss1
 |-  ( ( 1 ... N ) i^i Prime ) C_ ( 1 ... N )
71 70 8 sstri
 |-  ( ( 1 ... N ) i^i Prime ) C_ NN
72 71 a1i
 |-  ( ph -> ( ( 1 ... N ) i^i Prime ) C_ NN )
73 72 sselda
 |-  ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> i e. NN )
74 69 73 ffvelrnd
 |-  ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> ( Lam ` i ) e. RR )
75 74 recnd
 |-  ( ( ph /\ i e. ( ( 1 ... N ) i^i Prime ) ) -> ( Lam ` i ) e. CC )
76 68 75 fsumcl
 |-  ( ph -> sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) e. CC )
77 12 recnd
 |-  ( ( ph /\ i e. ( ( 1 ... N ) \ Prime ) ) -> ( Lam ` i ) e. CC )
78 5 77 fsumcl
 |-  ( ph -> sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) e. CC )
79 inindif
 |-  ( ( ( 1 ... N ) i^i Prime ) i^i ( ( 1 ... N ) \ Prime ) ) = (/)
80 79 a1i
 |-  ( ph -> ( ( ( 1 ... N ) i^i Prime ) i^i ( ( 1 ... N ) \ Prime ) ) = (/) )
81 inundif
 |-  ( ( ( 1 ... N ) i^i Prime ) u. ( ( 1 ... N ) \ Prime ) ) = ( 1 ... N )
82 81 eqcomi
 |-  ( 1 ... N ) = ( ( ( 1 ... N ) i^i Prime ) u. ( ( 1 ... N ) \ Prime ) )
83 82 a1i
 |-  ( ph -> ( 1 ... N ) = ( ( ( 1 ... N ) i^i Prime ) u. ( ( 1 ... N ) \ Prime ) ) )
84 6 a1i
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> Lam : NN --> RR )
85 9 sselda
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> i e. NN )
86 84 85 ffvelrnd
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> ( Lam ` i ) e. RR )
87 86 recnd
 |-  ( ( ph /\ i e. ( 1 ... N ) ) -> ( Lam ` i ) e. CC )
88 80 83 3 87 fsumsplit
 |-  ( ph -> sum_ i e. ( 1 ... N ) ( Lam ` i ) = ( sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) + sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) ) )
89 76 78 88 mvrladdd
 |-  ( ph -> ( sum_ i e. ( 1 ... N ) ( Lam ` i ) - sum_ i e. ( ( 1 ... N ) i^i Prime ) ( Lam ` i ) ) = sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) )
90 66 89 eqtr2d
 |-  ( ph -> sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) = ( ( psi ` N ) - ( theta ` N ) ) )
91 fveq2
 |-  ( x = N -> ( psi ` x ) = ( psi ` N ) )
92 fveq2
 |-  ( x = N -> ( theta ` x ) = ( theta ` N ) )
93 91 92 oveq12d
 |-  ( x = N -> ( ( psi ` x ) - ( theta ` x ) ) = ( ( psi ` N ) - ( theta ` N ) ) )
94 fveq2
 |-  ( x = N -> ( sqrt ` x ) = ( sqrt ` N ) )
95 94 oveq2d
 |-  ( x = N -> ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` x ) ) = ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) )
96 93 95 breq12d
 |-  ( x = N -> ( ( ( psi ` x ) - ( theta ` x ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` x ) ) <-> ( ( psi ` N ) - ( theta ` N ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) ) )
97 ax-ros336
 |-  A. x e. RR+ ( ( psi ` x ) - ( theta ` x ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` x ) )
98 97 a1i
 |-  ( ph -> A. x e. RR+ ( ( psi ` x ) - ( theta ` x ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` x ) ) )
99 96 98 34 rspcdva
 |-  ( ph -> ( ( psi ` N ) - ( theta ` N ) ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) )
100 90 99 eqbrtrd
 |-  ( ph -> sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) < ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) )
101 40 a1i
 |-  ( ph -> 1 e. RR )
102 log2le1
 |-  ( log ` 2 ) < 1
103 102 a1i
 |-  ( ph -> ( log ` 2 ) < 1 )
104 10nn0
 |-  ; 1 0 e. NN0
105 7nn0
 |-  7 e. NN0
106 104 105 nn0expcli
 |-  ( ; 1 0 ^ 7 ) e. NN0
107 106 nn0rei
 |-  ( ; 1 0 ^ 7 ) e. RR
108 107 a1i
 |-  ( ph -> ( ; 1 0 ^ 7 ) e. RR )
109 52 108 remulcld
 |-  ( ph -> ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) ) e. RR )
110 104 nn0rei
 |-  ; 1 0 e. RR
111 0z
 |-  0 e. ZZ
112 3z
 |-  3 e. ZZ
113 110 111 112 3pm3.2i
 |-  ( ; 1 0 e. RR /\ 0 e. ZZ /\ 3 e. ZZ )
114 1lt10
 |-  1 < ; 1 0
115 3pos
 |-  0 < 3
116 114 115 pm3.2i
 |-  ( 1 < ; 1 0 /\ 0 < 3 )
117 ltexp2a
 |-  ( ( ( ; 1 0 e. RR /\ 0 e. ZZ /\ 3 e. ZZ ) /\ ( 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 e. CC
122 10pos
 |-  0 < ; 1 0
123 39 122 gtneii
 |-  ; 1 0 =/= 0
124 4z
 |-  4 e. ZZ
125 expm1
 |-  ( ( ; 1 0 e. CC /\ ; 1 0 =/= 0 /\ 4 e. ZZ ) -> ( ; 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 e. NN0
130 104 129 nn0expcli
 |-  ( ; 1 0 ^ 4 ) e. NN0
131 130 nn0cni
 |-  ( ; 1 0 ^ 4 ) e. CC
132 divrec2
 |-  ( ( ( ; 1 0 ^ 4 ) e. CC /\ ; 1 0 e. CC /\ ; 1 0 =/= 0 ) -> ( ( ; 1 0 ^ 4 ) / ; 1 0 ) = ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) ) )
133 131 121 123 132 mp3an
 |-  ( ( ; 1 0 ^ 4 ) / ; 1 0 ) = ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) )
134 126 128 133 3eqtr3ri
 |-  ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) ) = ( ; 1 0 ^ 3 )
135 118 120 134 3brtr4i
 |-  1 < ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) )
136 1rp
 |-  1 e. RR+
137 136 dp0h
 |-  ( 0 . 1 ) = ( 1 / ; 1 0 )
138 137 oveq1i
 |-  ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) ) = ( ( 1 / ; 1 0 ) x. ( ; 1 0 ^ 4 ) )
139 135 138 breqtrri
 |-  1 < ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) )
140 139 a1i
 |-  ( ph -> 1 < ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) ) )
141 4p1e5
 |-  ( 4 + 1 ) = 5
142 5nn0
 |-  5 e. NN0
143 142 nn0zi
 |-  5 e. ZZ
144 38 136 141 124 143 dpexpp1
 |-  ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) ) = ( ( 0 . _ 0 1 ) x. ( ; 1 0 ^ 5 ) )
145 38 136 rpdp2cl
 |-  _ 0 1 e. RR+
146 5p1e6
 |-  ( 5 + 1 ) = 6
147 6nn0
 |-  6 e. NN0
148 147 nn0zi
 |-  6 e. ZZ
149 38 145 146 143 148 dpexpp1
 |-  ( ( 0 . _ 0 1 ) x. ( ; 1 0 ^ 5 ) ) = ( ( 0 . _ 0 _ 0 1 ) x. ( ; 1 0 ^ 6 ) )
150 38 145 rpdp2cl
 |-  _ 0 _ 0 1 e. RR+
151 6p1e7
 |-  ( 6 + 1 ) = 7
152 105 nn0zi
 |-  7 e. ZZ
153 38 150 151 148 152 dpexpp1
 |-  ( ( 0 . _ 0 _ 0 1 ) x. ( ; 1 0 ^ 6 ) ) = ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) )
154 144 149 153 3eqtrri
 |-  ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) ) = ( ( 0 . 1 ) x. ( ; 1 0 ^ 4 ) )
155 140 154 breqtrrdi
 |-  ( ph -> 1 < ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) ) )
156 38 150 rpdp2cl
 |-  _ 0 _ 0 _ 0 1 e. RR+
157 38 156 rpdpcl
 |-  ( 0 . _ 0 _ 0 _ 0 1 ) e. RR+
158 157 a1i
 |-  ( ph -> ( 0 . _ 0 _ 0 _ 0 1 ) e. RR+ )
159 2nn0
 |-  2 e. NN0
160 159 105 deccl
 |-  ; 2 7 e. NN0
161 104 160 nn0expcli
 |-  ( ; 1 0 ^ ; 2 7 ) e. NN0
162 161 nn0rei
 |-  ( ; 1 0 ^ ; 2 7 ) e. RR
163 162 a1i
 |-  ( ph -> ( ; 1 0 ^ ; 2 7 ) e. RR )
164 161 nn0ge0i
 |-  0 <_ ( ; 1 0 ^ ; 2 7 )
165 164 a1i
 |-  ( ph -> 0 <_ ( ; 1 0 ^ ; 2 7 ) )
166 163 165 resqrtcld
 |-  ( ph -> ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) e. RR )
167 expmul
 |-  ( ( ; 1 0 e. CC /\ 7 e. NN0 /\ 2 e. NN0 ) -> ( ; 1 0 ^ ( 7 x. 2 ) ) = ( ( ; 1 0 ^ 7 ) ^ 2 ) )
168 121 105 159 167 mp3an
 |-  ( ; 1 0 ^ ( 7 x. 2 ) ) = ( ( ; 1 0 ^ 7 ) ^ 2 )
169 7t2e14
 |-  ( 7 x. 2 ) = ; 1 4
170 169 oveq2i
 |-  ( ; 1 0 ^ ( 7 x. 2 ) ) = ( ; 1 0 ^ ; 1 4 )
171 168 170 eqtr3i
 |-  ( ( ; 1 0 ^ 7 ) ^ 2 ) = ( ; 1 0 ^ ; 1 4 )
172 171 fveq2i
 |-  ( sqrt ` ( ( ; 1 0 ^ 7 ) ^ 2 ) ) = ( sqrt ` ( ; 1 0 ^ ; 1 4 ) )
173 expgt0
 |-  ( ( ; 1 0 e. RR /\ 7 e. ZZ /\ 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 ) e. RR /\ 0 <_ ( ; 1 0 ^ 7 ) ) -> ( sqrt ` ( ( ; 1 0 ^ 7 ) ^ 2 ) ) = ( ; 1 0 ^ 7 ) )
177 107 175 176 mp2an
 |-  ( sqrt ` ( ( ; 1 0 ^ 7 ) ^ 2 ) ) = ( ; 1 0 ^ 7 )
178 172 177 eqtr3i
 |-  ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) = ( ; 1 0 ^ 7 )
179 17 129 deccl
 |-  ; 1 4 e. NN0
180 179 nn0zi
 |-  ; 1 4 e. ZZ
181 160 nn0zi
 |-  ; 2 7 e. ZZ
182 110 180 181 3pm3.2i
 |-  ( ; 1 0 e. RR /\ ; 1 4 e. ZZ /\ ; 2 7 e. ZZ )
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 e. RR /\ ; 1 4 e. ZZ /\ ; 2 7 e. ZZ ) /\ ( 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 ) e. NN0
190 189 nn0rei
 |-  ( ; 1 0 ^ ; 1 4 ) e. RR
191 expgt0
 |-  ( ( ; 1 0 e. RR /\ ; 1 4 e. ZZ /\ 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 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 1 4 ) )
195 162 164 pm3.2i
 |-  ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 2 7 ) )
196 sqrtlt
 |-  ( ( ( ( ; 1 0 ^ ; 1 4 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 1 4 ) ) /\ ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 2 7 ) ) ) -> ( ( ; 1 0 ^ ; 1 4 ) < ( ; 1 0 ^ ; 2 7 ) <-> ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) )
197 194 195 196 mp2an
 |-  ( ( ; 1 0 ^ ; 1 4 ) < ( ; 1 0 ^ ; 2 7 ) <-> ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) )
198 188 197 mpbi
 |-  ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) )
199 178 198 eqbrtrri
 |-  ( ; 1 0 ^ 7 ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) )
200 199 a1i
 |-  ( ph -> ( ; 1 0 ^ 7 ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) )
201 163 165 33 35 sqrtled
 |-  ( ph -> ( ( ; 1 0 ^ ; 2 7 ) <_ N <-> ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) <_ ( sqrt ` N ) ) )
202 2 201 mpbid
 |-  ( ph -> ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) <_ ( sqrt ` N ) )
203 108 166 36 200 202 ltletrd
 |-  ( ph -> ( ; 1 0 ^ 7 ) < ( sqrt ` N ) )
204 108 36 158 203 ltmul2dd
 |-  ( ph -> ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( ; 1 0 ^ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) )
205 101 109 53 155 204 lttrd
 |-  ( ph -> 1 < ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) )
206 16 101 53 103 205 lttrd
 |-  ( ph -> ( log ` 2 ) < ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) )
207 13 16 37 53 100 206 lt2addd
 |-  ( ph -> ( sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) + ( log ` 2 ) ) < ( ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) ) )
208 nfv
 |-  F/ i ph
209 nfcv
 |-  F/_ i ( log ` 2 )
210 2prm
 |-  2 e. Prime
211 210 a1i
 |-  ( ph -> 2 e. Prime )
212 elndif
 |-  ( 2 e. Prime -> -. 2 e. ( ( 1 ... N ) \ Prime ) )
213 211 212 syl
 |-  ( ph -> -. 2 e. ( ( 1 ... N ) \ Prime ) )
214 fveq2
 |-  ( i = 2 -> ( Lam ` i ) = ( Lam ` 2 ) )
215 vmaprm
 |-  ( 2 e. Prime -> ( Lam ` 2 ) = ( log ` 2 ) )
216 210 215 ax-mp
 |-  ( Lam ` 2 ) = ( log ` 2 )
217 214 216 eqtrdi
 |-  ( i = 2 -> ( Lam ` i ) = ( log ` 2 ) )
218 2cnd
 |-  ( ph -> 2 e. CC )
219 2ne0
 |-  2 =/= 0
220 219 a1i
 |-  ( ph -> 2 =/= 0 )
221 218 220 logcld
 |-  ( ph -> ( log ` 2 ) e. CC )
222 208 209 5 211 213 77 217 221 fsumsplitsn
 |-  ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) = ( sum_ i e. ( ( 1 ... N ) \ Prime ) ( Lam ` i ) + ( log ` 2 ) ) )
223 147 14 rpdp2cl
 |-  _ 6 2 e. RR+
224 159 223 rpdp2cl
 |-  _ 2 _ 6 2 e. RR+
225 3rp
 |-  3 e. RR+
226 147 225 rpdp2cl
 |-  _ 6 3 e. RR+
227 159 226 rpdp2cl
 |-  _ 2 _ 6 3 e. RR+
228 1p0e1
 |-  ( 1 + 0 ) = 1
229 4cn
 |-  4 e. CC
230 229 addid1i
 |-  ( 4 + 0 ) = 4
231 2cn
 |-  2 e. CC
232 231 addid1i
 |-  ( 2 + 0 ) = 2
233 3nn0
 |-  3 e. NN0
234 eqid
 |-  ; 6 2 = ; 6 2
235 eqid
 |-  ; 0 1 = ; 0 1
236 6cn
 |-  6 e. CC
237 236 addid1i
 |-  ( 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 ) ) x. ( sqrt ` N ) ) = ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) )
245 32 recnd
 |-  ( ph -> ( 1 . _ 4 _ 2 _ 6 2 ) e. CC )
246 52 recnd
 |-  ( ph -> ( 0 . _ 0 _ 0 _ 0 1 ) e. CC )
247 36 recnd
 |-  ( ph -> ( sqrt ` N ) e. CC )
248 245 246 247 adddird
 |-  ( ph -> ( ( ( 1 . _ 4 _ 2 _ 6 2 ) + ( 0 . _ 0 _ 0 _ 0 1 ) ) x. ( sqrt ` N ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) ) )
249 244 248 eqtr3id
 |-  ( ph -> ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) = ( ( ( 1 . _ 4 _ 2 _ 6 2 ) x. ( sqrt ` N ) ) + ( ( 0 . _ 0 _ 0 _ 0 1 ) x. ( sqrt ` N ) ) ) )
250 207 222 249 3brtr4d
 |-  ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) < ( ( 1 . _ 4 _ 2 _ 6 3 ) x. ( sqrt ` N ) ) )