This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 addridi 
 |-  ( 4 + 0 ) = 4
231 2cn 
 |-  2 e. CC
232 231 addridi 
 |-  ( 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 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 ) ) 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 ) ) )