Metamath Proof Explorer

Theorem hgt750lem

Description: Lemma for tgoldbachgtd . (Contributed by Thierry Arnoux, 17-Dec-2021)

Ref Expression
Assertion hgt750lem 
|- ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )

Proof

Step Hyp Ref Expression
1 7nn0 
 |-  7 e. NN0
2 3re 
 |-  3 e. RR
3 4re 
 |-  4 e. RR
4 8re 
 |-  8 e. RR
5 3 4 pm3.2i 
 |-  ( 4 e. RR /\ 8 e. RR )
6 dp2cl 
 |-  ( ( 4 e. RR /\ 8 e. RR ) -> _ 4 8 e. RR )
7 5 6 ax-mp 
 |-  _ 4 8 e. RR
8 2 7 pm3.2i 
 |-  ( 3 e. RR /\ _ 4 8 e. RR )
9 dp2cl 
 |-  ( ( 3 e. RR /\ _ 4 8 e. RR ) -> _ 3 _ 4 8 e. RR )
10 8 9 ax-mp 
 |-  _ 3 _ 4 8 e. RR
11 dpcl 
 |-  ( ( 7 e. NN0 /\ _ 3 _ 4 8 e. RR ) -> ( 7 . _ 3 _ 4 8 ) e. RR )
12 1 10 11 mp2an 
 |-  ( 7 . _ 3 _ 4 8 ) e. RR
13 12 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( 7 . _ 3 _ 4 8 ) e. RR )
14 nn0re 
 |-  ( N e. NN0 -> N e. RR )
15 14 adantr 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> N e. RR )
16 0re 
 |-  0 e. RR
17 16 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> 0 e. RR )
18 10re 
 |-  ; 1 0 e. RR
19 2nn0 
 |-  2 e. NN0
20 19 1 deccl 
 |-  ; 2 7 e. NN0
21 reexpcl 
 |-  ( ( ; 1 0 e. RR /\ ; 2 7 e. NN0 ) -> ( ; 1 0 ^ ; 2 7 ) e. RR )
22 18 20 21 mp2an 
 |-  ( ; 1 0 ^ ; 2 7 ) e. RR
23 22 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ; 1 0 ^ ; 2 7 ) e. RR )
24 0lt1 
 |-  0 < 1
25 1nn 
 |-  1 e. NN
26 0nn0 
 |-  0 e. NN0
27 1nn0 
 |-  1 e. NN0
28 1re 
 |-  1 e. RR
29 9re 
 |-  9 e. RR
30 1lt9 
 |-  1 < 9
31 28 29 30 ltleii 
 |-  1 <_ 9
32 25 26 27 31 declei 
 |-  1 <_ ; 1 0
33 expge1 
 |-  ( ( ; 1 0 e. RR /\ ; 2 7 e. NN0 /\ 1 <_ ; 1 0 ) -> 1 <_ ( ; 1 0 ^ ; 2 7 ) )
34 18 20 32 33 mp3an 
 |-  1 <_ ( ; 1 0 ^ ; 2 7 )
35 16 28 22 ltletri 
 |-  ( ( 0 < 1 /\ 1 <_ ( ; 1 0 ^ ; 2 7 ) ) -> 0 < ( ; 1 0 ^ ; 2 7 ) )
36 24 34 35 mp2an 
 |-  0 < ( ; 1 0 ^ ; 2 7 )
37 36 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> 0 < ( ; 1 0 ^ ; 2 7 ) )
38 simpr 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ; 1 0 ^ ; 2 7 ) <_ N )
39 17 23 15 37 38 ltletrd 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> 0 < N )
40 15 39 elrpd 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> N e. RR+ )
41 40 relogcld 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( log ` N ) e. RR )
42 40 rpge0d 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> 0 <_ N )
43 15 42 resqrtcld 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( sqrt ` N ) e. RR )
44 40 sqrtgt0d 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> 0 < ( sqrt ` N ) )
45 17 44 gtned 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( sqrt ` N ) =/= 0 )
46 41 43 45 redivcld 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( log ` N ) / ( sqrt ` N ) ) e. RR )
47 13 46 remulcld 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) e. RR )
48 elrp 
 |-  ( ( ; 1 0 ^ ; 2 7 ) e. RR+ <-> ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ 0 < ( ; 1 0 ^ ; 2 7 ) ) )
49 22 36 48 mpbir2an 
 |-  ( ; 1 0 ^ ; 2 7 ) e. RR+
50 relogcl 
 |-  ( ( ; 1 0 ^ ; 2 7 ) e. RR+ -> ( log ` ( ; 1 0 ^ ; 2 7 ) ) e. RR )
51 49 50 ax-mp 
 |-  ( log ` ( ; 1 0 ^ ; 2 7 ) ) e. RR
52 22 36 sqrtpclii 
 |-  ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) e. RR
53 22 36 sqrtgt0ii 
 |-  0 < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) )
54 16 53 gtneii 
 |-  ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) =/= 0
55 51 52 54 redivcli 
 |-  ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) e. RR
56 55 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) e. RR )
57 13 56 remulcld 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) e. RR )
58 qssre 
 |-  QQ C_ RR
59 4nn0 
 |-  4 e. NN0
60 nn0ssq 
 |-  NN0 C_ QQ
61 8nn0 
 |-  8 e. NN0
62 60 61 sselii 
 |-  8 e. QQ
63 59 62 dp2clq 
 |-  _ 4 8 e. QQ
64 19 63 dp2clq 
 |-  _ 2 _ 4 8 e. QQ
65 19 64 dp2clq 
 |-  _ 2 _ 2 _ 4 8 e. QQ
66 59 65 dp2clq 
 |-  _ 4 _ 2 _ 2 _ 4 8 e. QQ
67 26 66 dp2clq 
 |-  _ 0 _ 4 _ 2 _ 2 _ 4 8 e. QQ
68 26 67 dp2clq 
 |-  _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. QQ
69 26 68 dp2clq 
 |-  _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. QQ
70 58 69 sselii 
 |-  _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. RR
71 dpcl 
 |-  ( ( 0 e. NN0 /\ _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. RR ) -> ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. RR )
72 26 70 71 mp2an 
 |-  ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. RR
73 72 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. RR )
74 3nn0 
 |-  3 e. NN0
75 8pos 
 |-  0 < 8
76 elrp 
 |-  ( 8 e. RR+ <-> ( 8 e. RR /\ 0 < 8 ) )
77 4 75 76 mpbir2an 
 |-  8 e. RR+
78 59 77 rpdp2cl 
 |-  _ 4 8 e. RR+
79 74 78 rpdp2cl 
 |-  _ 3 _ 4 8 e. RR+
80 1 79 rpdpcl 
 |-  ( 7 . _ 3 _ 4 8 ) e. RR+
81 elrp 
 |-  ( ( 7 . _ 3 _ 4 8 ) e. RR+ <-> ( ( 7 . _ 3 _ 4 8 ) e. RR /\ 0 < ( 7 . _ 3 _ 4 8 ) ) )
82 80 81 mpbi 
 |-  ( ( 7 . _ 3 _ 4 8 ) e. RR /\ 0 < ( 7 . _ 3 _ 4 8 ) )
83 82 simpri 
 |-  0 < ( 7 . _ 3 _ 4 8 )
84 16 12 83 ltleii 
 |-  0 <_ ( 7 . _ 3 _ 4 8 )
85 84 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> 0 <_ ( 7 . _ 3 _ 4 8 ) )
86 49 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ; 1 0 ^ ; 2 7 ) e. RR+ )
87 2cn 
 |-  2 e. CC
88 87 mullidi 
 |-  ( 1 x. 2 ) = 2
89 2nn 
 |-  2 e. NN
90 89 1 27 31 declei 
 |-  1 <_ ; 2 7
91 2pos 
 |-  0 < 2
92 20 nn0rei 
 |-  ; 2 7 e. RR
93 2re 
 |-  2 e. RR
94 28 92 93 lemul1i 
 |-  ( 0 < 2 -> ( 1 <_ ; 2 7 <-> ( 1 x. 2 ) <_ ( ; 2 7 x. 2 ) ) )
95 91 94 ax-mp 
 |-  ( 1 <_ ; 2 7 <-> ( 1 x. 2 ) <_ ( ; 2 7 x. 2 ) )
96 90 95 mpbi 
 |-  ( 1 x. 2 ) <_ ( ; 2 7 x. 2 )
97 88 96 eqbrtrri 
 |-  2 <_ ( ; 2 7 x. 2 )
98 1p1e2 
 |-  ( 1 + 1 ) = 2
99 loge 
 |-  ( log ` _e ) = 1
100 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
101 100 simpri 
 |-  _e < 3
102 epr 
 |-  _e e. RR+
103 3rp 
 |-  3 e. RR+
104 logltb 
 |-  ( ( _e e. RR+ /\ 3 e. RR+ ) -> ( _e < 3 <-> ( log ` _e ) < ( log ` 3 ) ) )
105 102 103 104 mp2an 
 |-  ( _e < 3 <-> ( log ` _e ) < ( log ` 3 ) )
106 101 105 mpbi 
 |-  ( log ` _e ) < ( log ` 3 )
107 99 106 eqbrtrri 
 |-  1 < ( log ` 3 )
108 relogcl 
 |-  ( 3 e. RR+ -> ( log ` 3 ) e. RR )
109 103 108 ax-mp 
 |-  ( log ` 3 ) e. RR
110 28 28 109 109 lt2addi 
 |-  ( ( 1 < ( log ` 3 ) /\ 1 < ( log ` 3 ) ) -> ( 1 + 1 ) < ( ( log ` 3 ) + ( log ` 3 ) ) )
111 107 107 110 mp2an 
 |-  ( 1 + 1 ) < ( ( log ` 3 ) + ( log ` 3 ) )
112 3cn 
 |-  3 e. CC
113 3ne0 
 |-  3 =/= 0
114 logmul2 
 |-  ( ( 3 e. CC /\ 3 =/= 0 /\ 3 e. RR+ ) -> ( log ` ( 3 x. 3 ) ) = ( ( log ` 3 ) + ( log ` 3 ) ) )
115 112 113 103 114 mp3an 
 |-  ( log ` ( 3 x. 3 ) ) = ( ( log ` 3 ) + ( log ` 3 ) )
116 3t3e9 
 |-  ( 3 x. 3 ) = 9
117 116 fveq2i 
 |-  ( log ` ( 3 x. 3 ) ) = ( log ` 9 )
118 9lt10 
 |-  9 < ; 1 0
119 29 18 118 ltleii 
 |-  9 <_ ; 1 0
120 9pos 
 |-  0 < 9
121 elrp 
 |-  ( 9 e. RR+ <-> ( 9 e. RR /\ 0 < 9 ) )
122 29 120 121 mpbir2an 
 |-  9 e. RR+
123 10pos 
 |-  0 < ; 1 0
124 elrp 
 |-  ( ; 1 0 e. RR+ <-> ( ; 1 0 e. RR /\ 0 < ; 1 0 ) )
125 18 123 124 mpbir2an 
 |-  ; 1 0 e. RR+
126 logleb 
 |-  ( ( 9 e. RR+ /\ ; 1 0 e. RR+ ) -> ( 9 <_ ; 1 0 <-> ( log ` 9 ) <_ ( log ` ; 1 0 ) ) )
127 122 125 126 mp2an 
 |-  ( 9 <_ ; 1 0 <-> ( log ` 9 ) <_ ( log ` ; 1 0 ) )
128 119 127 mpbi 
 |-  ( log ` 9 ) <_ ( log ` ; 1 0 )
129 117 128 eqbrtri 
 |-  ( log ` ( 3 x. 3 ) ) <_ ( log ` ; 1 0 )
130 115 129 eqbrtrri 
 |-  ( ( log ` 3 ) + ( log ` 3 ) ) <_ ( log ` ; 1 0 )
131 28 28 readdcli 
 |-  ( 1 + 1 ) e. RR
132 109 109 readdcli 
 |-  ( ( log ` 3 ) + ( log ` 3 ) ) e. RR
133 relogcl 
 |-  ( ; 1 0 e. RR+ -> ( log ` ; 1 0 ) e. RR )
134 125 133 ax-mp 
 |-  ( log ` ; 1 0 ) e. RR
135 131 132 134 ltletri 
 |-  ( ( ( 1 + 1 ) < ( ( log ` 3 ) + ( log ` 3 ) ) /\ ( ( log ` 3 ) + ( log ` 3 ) ) <_ ( log ` ; 1 0 ) ) -> ( 1 + 1 ) < ( log ` ; 1 0 ) )
136 111 130 135 mp2an 
 |-  ( 1 + 1 ) < ( log ` ; 1 0 )
137 98 136 eqbrtrri 
 |-  2 < ( log ` ; 1 0 )
138 93 134 ltlei 
 |-  ( 2 < ( log ` ; 1 0 ) -> 2 <_ ( log ` ; 1 0 ) )
139 137 138 ax-mp 
 |-  2 <_ ( log ` ; 1 0 )
140 16 29 120 ltleii 
 |-  0 <_ 9
141 89 1 26 140 decltdi 
 |-  0 < ; 2 7
142 93 134 92 lemul2i 
 |-  ( 0 < ; 2 7 -> ( 2 <_ ( log ` ; 1 0 ) <-> ( ; 2 7 x. 2 ) <_ ( ; 2 7 x. ( log ` ; 1 0 ) ) ) )
143 141 142 ax-mp 
 |-  ( 2 <_ ( log ` ; 1 0 ) <-> ( ; 2 7 x. 2 ) <_ ( ; 2 7 x. ( log ` ; 1 0 ) ) )
144 139 143 mpbi 
 |-  ( ; 2 7 x. 2 ) <_ ( ; 2 7 x. ( log ` ; 1 0 ) )
145 92 93 remulcli 
 |-  ( ; 2 7 x. 2 ) e. RR
146 20 nn0zi 
 |-  ; 2 7 e. ZZ
147 relogexp 
 |-  ( ( ; 1 0 e. RR+ /\ ; 2 7 e. ZZ ) -> ( log ` ( ; 1 0 ^ ; 2 7 ) ) = ( ; 2 7 x. ( log ` ; 1 0 ) ) )
148 125 146 147 mp2an 
 |-  ( log ` ( ; 1 0 ^ ; 2 7 ) ) = ( ; 2 7 x. ( log ` ; 1 0 ) )
149 148 51 eqeltrri 
 |-  ( ; 2 7 x. ( log ` ; 1 0 ) ) e. RR
150 93 145 149 letri 
 |-  ( ( 2 <_ ( ; 2 7 x. 2 ) /\ ( ; 2 7 x. 2 ) <_ ( ; 2 7 x. ( log ` ; 1 0 ) ) ) -> 2 <_ ( ; 2 7 x. ( log ` ; 1 0 ) ) )
151 97 144 150 mp2an 
 |-  2 <_ ( ; 2 7 x. ( log ` ; 1 0 ) )
152 relogef 
 |-  ( 2 e. RR -> ( log ` ( exp ` 2 ) ) = 2 )
153 93 152 ax-mp 
 |-  ( log ` ( exp ` 2 ) ) = 2
154 151 153 148 3brtr4i 
 |-  ( log ` ( exp ` 2 ) ) <_ ( log ` ( ; 1 0 ^ ; 2 7 ) )
155 rpefcl 
 |-  ( 2 e. RR -> ( exp ` 2 ) e. RR+ )
156 93 155 ax-mp 
 |-  ( exp ` 2 ) e. RR+
157 logleb 
 |-  ( ( ( exp ` 2 ) e. RR+ /\ ( ; 1 0 ^ ; 2 7 ) e. RR+ ) -> ( ( exp ` 2 ) <_ ( ; 1 0 ^ ; 2 7 ) <-> ( log ` ( exp ` 2 ) ) <_ ( log ` ( ; 1 0 ^ ; 2 7 ) ) ) )
158 156 49 157 mp2an 
 |-  ( ( exp ` 2 ) <_ ( ; 1 0 ^ ; 2 7 ) <-> ( log ` ( exp ` 2 ) ) <_ ( log ` ( ; 1 0 ^ ; 2 7 ) ) )
159 154 158 mpbir 
 |-  ( exp ` 2 ) <_ ( ; 1 0 ^ ; 2 7 )
160 159 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( exp ` 2 ) <_ ( ; 1 0 ^ ; 2 7 ) )
161 86 40 160 38 logdivsqrle 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( log ` N ) / ( sqrt ` N ) ) <_ ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) )
162 46 56 13 85 161 lemul2ad 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) <_ ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) )
163 3lt10 
 |-  3 < ; 1 0
164 4lt10 
 |-  4 < ; 1 0
165 8lt10 
 |-  8 < ; 1 0
166 59 77 164 165 dp2lt10 
 |-  _ 4 8 < ; 1 0
167 74 78 163 166 dp2lt10 
 |-  _ 3 _ 4 8 < ; 1 0
168 7p1e8 
 |-  ( 7 + 1 ) = 8
169 1 79 61 167 168 dplti 
 |-  ( 7 . _ 3 _ 4 8 ) < 8
170 58 62 sselii 
 |-  8 e. RR
171 12 170 18 lttri 
 |-  ( ( ( 7 . _ 3 _ 4 8 ) < 8 /\ 8 < ; 1 0 ) -> ( 7 . _ 3 _ 4 8 ) < ; 1 0 )
172 169 165 171 mp2an 
 |-  ( 7 . _ 3 _ 4 8 ) < ; 1 0
173 27 26 deccl 
 |-  ; 1 0 e. NN0
174 173 numexp0 
 |-  ( ; 1 0 ^ 0 ) = 1
175 0z 
 |-  0 e. ZZ
176 18 175 146 3pm3.2i 
 |-  ( ; 1 0 e. RR /\ 0 e. ZZ /\ ; 2 7 e. ZZ )
177 1lt10 
 |-  1 < ; 1 0
178 177 141 pm3.2i 
 |-  ( 1 < ; 1 0 /\ 0 < ; 2 7 )
179 ltexp2a 
 |-  ( ( ( ; 1 0 e. RR /\ 0 e. ZZ /\ ; 2 7 e. ZZ ) /\ ( 1 < ; 1 0 /\ 0 < ; 2 7 ) ) -> ( ; 1 0 ^ 0 ) < ( ; 1 0 ^ ; 2 7 ) )
180 176 178 179 mp2an 
 |-  ( ; 1 0 ^ 0 ) < ( ; 1 0 ^ ; 2 7 )
181 174 180 eqbrtrri 
 |-  1 < ( ; 1 0 ^ ; 2 7 )
182 loggt0b 
 |-  ( ( ; 1 0 ^ ; 2 7 ) e. RR+ -> ( 0 < ( log ` ( ; 1 0 ^ ; 2 7 ) ) <-> 1 < ( ; 1 0 ^ ; 2 7 ) ) )
183 49 182 ax-mp 
 |-  ( 0 < ( log ` ( ; 1 0 ^ ; 2 7 ) ) <-> 1 < ( ; 1 0 ^ ; 2 7 ) )
184 181 183 mpbir 
 |-  0 < ( log ` ( ; 1 0 ^ ; 2 7 ) )
185 51 52 divgt0i 
 |-  ( ( 0 < ( log ` ( ; 1 0 ^ ; 2 7 ) ) /\ 0 < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) -> 0 < ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) )
186 184 53 185 mp2an 
 |-  0 < ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) )
187 12 18 55 ltmul1i 
 |-  ( 0 < ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) -> ( ( 7 . _ 3 _ 4 8 ) < ; 1 0 <-> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( ; 1 0 x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) ) )
188 186 187 ax-mp 
 |-  ( ( 7 . _ 3 _ 4 8 ) < ; 1 0 <-> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( ; 1 0 x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) )
189 172 188 mpbi 
 |-  ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( ; 1 0 x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) )
190 18 recni 
 |-  ; 1 0 e. CC
191 expmul 
 |-  ( ( ; 1 0 e. CC /\ 7 e. NN0 /\ 2 e. NN0 ) -> ( ; 1 0 ^ ( 7 x. 2 ) ) = ( ( ; 1 0 ^ 7 ) ^ 2 ) )
192 190 1 19 191 mp3an 
 |-  ( ; 1 0 ^ ( 7 x. 2 ) ) = ( ( ; 1 0 ^ 7 ) ^ 2 )
193 7t2e14 
 |-  ( 7 x. 2 ) = ; 1 4
194 193 oveq2i 
 |-  ( ; 1 0 ^ ( 7 x. 2 ) ) = ( ; 1 0 ^ ; 1 4 )
195 192 194 eqtr3i 
 |-  ( ( ; 1 0 ^ 7 ) ^ 2 ) = ( ; 1 0 ^ ; 1 4 )
196 195 fveq2i 
 |-  ( sqrt ` ( ( ; 1 0 ^ 7 ) ^ 2 ) ) = ( sqrt ` ( ; 1 0 ^ ; 1 4 ) )
197 reexpcl 
 |-  ( ( ; 1 0 e. RR /\ 7 e. NN0 ) -> ( ; 1 0 ^ 7 ) e. RR )
198 18 1 197 mp2an 
 |-  ( ; 1 0 ^ 7 ) e. RR
199 1 nn0zi 
 |-  7 e. ZZ
200 expgt0 
 |-  ( ( ; 1 0 e. RR /\ 7 e. ZZ /\ 0 < ; 1 0 ) -> 0 < ( ; 1 0 ^ 7 ) )
201 18 199 123 200 mp3an 
 |-  0 < ( ; 1 0 ^ 7 )
202 16 198 201 ltleii 
 |-  0 <_ ( ; 1 0 ^ 7 )
203 sqrtsq 
 |-  ( ( ( ; 1 0 ^ 7 ) e. RR /\ 0 <_ ( ; 1 0 ^ 7 ) ) -> ( sqrt ` ( ( ; 1 0 ^ 7 ) ^ 2 ) ) = ( ; 1 0 ^ 7 ) )
204 198 202 203 mp2an 
 |-  ( sqrt ` ( ( ; 1 0 ^ 7 ) ^ 2 ) ) = ( ; 1 0 ^ 7 )
205 196 204 eqtr3i 
 |-  ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) = ( ; 1 0 ^ 7 )
206 27 59 deccl 
 |-  ; 1 4 e. NN0
207 206 nn0zi 
 |-  ; 1 4 e. ZZ
208 18 207 146 3pm3.2i 
 |-  ( ; 1 0 e. RR /\ ; 1 4 e. ZZ /\ ; 2 7 e. ZZ )
209 1lt2 
 |-  1 < 2
210 27 19 59 1 164 209 decltc 
 |-  ; 1 4 < ; 2 7
211 177 210 pm3.2i 
 |-  ( 1 < ; 1 0 /\ ; 1 4 < ; 2 7 )
212 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 ) )
213 208 211 212 mp2an 
 |-  ( ; 1 0 ^ ; 1 4 ) < ( ; 1 0 ^ ; 2 7 )
214 reexpcl 
 |-  ( ( ; 1 0 e. RR /\ ; 1 4 e. NN0 ) -> ( ; 1 0 ^ ; 1 4 ) e. RR )
215 18 206 214 mp2an 
 |-  ( ; 1 0 ^ ; 1 4 ) e. RR
216 expgt0 
 |-  ( ( ; 1 0 e. RR /\ ; 1 4 e. ZZ /\ 0 < ; 1 0 ) -> 0 < ( ; 1 0 ^ ; 1 4 ) )
217 18 207 123 216 mp3an 
 |-  0 < ( ; 1 0 ^ ; 1 4 )
218 16 215 217 ltleii 
 |-  0 <_ ( ; 1 0 ^ ; 1 4 )
219 215 218 pm3.2i 
 |-  ( ( ; 1 0 ^ ; 1 4 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 1 4 ) )
220 16 22 36 ltleii 
 |-  0 <_ ( ; 1 0 ^ ; 2 7 )
221 22 220 pm3.2i 
 |-  ( ( ; 1 0 ^ ; 2 7 ) e. RR /\ 0 <_ ( ; 1 0 ^ ; 2 7 ) )
222 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 ) ) ) )
223 219 221 222 mp2an 
 |-  ( ( ; 1 0 ^ ; 1 4 ) < ( ; 1 0 ^ ; 2 7 ) <-> ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) )
224 213 223 mpbi 
 |-  ( sqrt ` ( ; 1 0 ^ ; 1 4 ) ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) )
225 205 224 eqbrtrri 
 |-  ( ; 1 0 ^ 7 ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) )
226 198 201 pm3.2i 
 |-  ( ( ; 1 0 ^ 7 ) e. RR /\ 0 < ( ; 1 0 ^ 7 ) )
227 52 53 pm3.2i 
 |-  ( ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) e. RR /\ 0 < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) )
228 51 184 pm3.2i 
 |-  ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) e. RR /\ 0 < ( log ` ( ; 1 0 ^ ; 2 7 ) ) )
229 ltdiv2 
 |-  ( ( ( ( ; 1 0 ^ 7 ) e. RR /\ 0 < ( ; 1 0 ^ 7 ) ) /\ ( ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) e. RR /\ 0 < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) /\ ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) e. RR /\ 0 < ( log ` ( ; 1 0 ^ ; 2 7 ) ) ) ) -> ( ( ; 1 0 ^ 7 ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) <-> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( ; 1 0 ^ 7 ) ) ) )
230 226 227 228 229 mp3an 
 |-  ( ( ; 1 0 ^ 7 ) < ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) <-> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( ; 1 0 ^ 7 ) ) )
231 225 230 mpbi 
 |-  ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( ; 1 0 ^ 7 ) )
232 6nn 
 |-  6 e. NN
233 232 nngt0i 
 |-  0 < 6
234 27 26 232 233 declt 
 |-  ; 1 0 < ; 1 6
235 6nn0 
 |-  6 e. NN0
236 27 235 deccl 
 |-  ; 1 6 e. NN0
237 236 nn0rei 
 |-  ; 1 6 e. RR
238 25 235 26 123 declti 
 |-  0 < ; 1 6
239 elrp 
 |-  ( ; 1 6 e. RR+ <-> ( ; 1 6 e. RR /\ 0 < ; 1 6 ) )
240 237 238 239 mpbir2an 
 |-  ; 1 6 e. RR+
241 logltb 
 |-  ( ( ; 1 0 e. RR+ /\ ; 1 6 e. RR+ ) -> ( ; 1 0 < ; 1 6 <-> ( log ` ; 1 0 ) < ( log ` ; 1 6 ) ) )
242 125 240 241 mp2an 
 |-  ( ; 1 0 < ; 1 6 <-> ( log ` ; 1 0 ) < ( log ` ; 1 6 ) )
243 234 242 mpbi 
 |-  ( log ` ; 1 0 ) < ( log ` ; 1 6 )
244 2exp4 
 |-  ( 2 ^ 4 ) = ; 1 6
245 244 fveq2i 
 |-  ( log ` ( 2 ^ 4 ) ) = ( log ` ; 1 6 )
246 2rp 
 |-  2 e. RR+
247 59 nn0zi 
 |-  4 e. ZZ
248 relogexp 
 |-  ( ( 2 e. RR+ /\ 4 e. ZZ ) -> ( log ` ( 2 ^ 4 ) ) = ( 4 x. ( log ` 2 ) ) )
249 246 247 248 mp2an 
 |-  ( log ` ( 2 ^ 4 ) ) = ( 4 x. ( log ` 2 ) )
250 245 249 eqtr3i 
 |-  ( log ` ; 1 6 ) = ( 4 x. ( log ` 2 ) )
251 243 250 breqtri 
 |-  ( log ` ; 1 0 ) < ( 4 x. ( log ` 2 ) )
252 100 simpli 
 |-  2 < _e
253 logltb 
 |-  ( ( 2 e. RR+ /\ _e e. RR+ ) -> ( 2 < _e <-> ( log ` 2 ) < ( log ` _e ) ) )
254 246 102 253 mp2an 
 |-  ( 2 < _e <-> ( log ` 2 ) < ( log ` _e ) )
255 252 254 mpbi 
 |-  ( log ` 2 ) < ( log ` _e )
256 255 99 breqtri 
 |-  ( log ` 2 ) < 1
257 4pos 
 |-  0 < 4
258 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
259 246 258 ax-mp 
 |-  ( log ` 2 ) e. RR
260 259 28 3 ltmul2i 
 |-  ( 0 < 4 -> ( ( log ` 2 ) < 1 <-> ( 4 x. ( log ` 2 ) ) < ( 4 x. 1 ) ) )
261 257 260 ax-mp 
 |-  ( ( log ` 2 ) < 1 <-> ( 4 x. ( log ` 2 ) ) < ( 4 x. 1 ) )
262 256 261 mpbi 
 |-  ( 4 x. ( log ` 2 ) ) < ( 4 x. 1 )
263 4cn 
 |-  4 e. CC
264 263 mulridi 
 |-  ( 4 x. 1 ) = 4
265 262 264 breqtri 
 |-  ( 4 x. ( log ` 2 ) ) < 4
266 3 259 remulcli 
 |-  ( 4 x. ( log ` 2 ) ) e. RR
267 134 266 3 lttri 
 |-  ( ( ( log ` ; 1 0 ) < ( 4 x. ( log ` 2 ) ) /\ ( 4 x. ( log ` 2 ) ) < 4 ) -> ( log ` ; 1 0 ) < 4 )
268 251 265 267 mp2an 
 |-  ( log ` ; 1 0 ) < 4
269 134 3 92 ltmul2i 
 |-  ( 0 < ; 2 7 -> ( ( log ` ; 1 0 ) < 4 <-> ( ; 2 7 x. ( log ` ; 1 0 ) ) < ( ; 2 7 x. 4 ) ) )
270 141 269 ax-mp 
 |-  ( ( log ` ; 1 0 ) < 4 <-> ( ; 2 7 x. ( log ` ; 1 0 ) ) < ( ; 2 7 x. 4 ) )
271 268 270 mpbi 
 |-  ( ; 2 7 x. ( log ` ; 1 0 ) ) < ( ; 2 7 x. 4 )
272 148 271 eqbrtri 
 |-  ( log ` ( ; 1 0 ^ ; 2 7 ) ) < ( ; 2 7 x. 4 )
273 92 3 remulcli 
 |-  ( ; 2 7 x. 4 ) e. RR
274 51 273 198 ltdiv1i 
 |-  ( 0 < ( ; 1 0 ^ 7 ) -> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) < ( ; 2 7 x. 4 ) <-> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( ; 1 0 ^ 7 ) ) < ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) ) )
275 201 274 ax-mp 
 |-  ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) < ( ; 2 7 x. 4 ) <-> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( ; 1 0 ^ 7 ) ) < ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) )
276 272 275 mpbi 
 |-  ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( ; 1 0 ^ 7 ) ) < ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) )
277 16 201 gtneii 
 |-  ( ; 1 0 ^ 7 ) =/= 0
278 51 198 277 redivcli 
 |-  ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( ; 1 0 ^ 7 ) ) e. RR
279 273 198 277 redivcli 
 |-  ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) e. RR
280 55 278 279 lttri 
 |-  ( ( ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( ; 1 0 ^ 7 ) ) /\ ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( ; 1 0 ^ 7 ) ) < ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) ) -> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) )
281 231 276 280 mp2an 
 |-  ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) )
282 7lt10 
 |-  7 < ; 1 0
283 2lt10 
 |-  2 < ; 1 0
284 19 173 1 26 282 283 decltc 
 |-  ; 2 7 < ; ; 1 0 0
285 10nn 
 |-  ; 1 0 e. NN
286 285 decnncl2 
 |-  ; ; 1 0 0 e. NN
287 286 nnrei 
 |-  ; ; 1 0 0 e. RR
288 92 287 3 ltmul1i 
 |-  ( 0 < 4 -> ( ; 2 7 < ; ; 1 0 0 <-> ( ; 2 7 x. 4 ) < ( ; ; 1 0 0 x. 4 ) ) )
289 257 288 ax-mp 
 |-  ( ; 2 7 < ; ; 1 0 0 <-> ( ; 2 7 x. 4 ) < ( ; ; 1 0 0 x. 4 ) )
290 284 289 mpbi 
 |-  ( ; 2 7 x. 4 ) < ( ; ; 1 0 0 x. 4 )
291 287 3 remulcli 
 |-  ( ; ; 1 0 0 x. 4 ) e. RR
292 273 291 198 ltdiv1i 
 |-  ( 0 < ( ; 1 0 ^ 7 ) -> ( ( ; 2 7 x. 4 ) < ( ; ; 1 0 0 x. 4 ) <-> ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( ; ; 1 0 0 x. 4 ) / ( ; 1 0 ^ 7 ) ) ) )
293 201 292 ax-mp 
 |-  ( ( ; 2 7 x. 4 ) < ( ; ; 1 0 0 x. 4 ) <-> ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( ; ; 1 0 0 x. 4 ) / ( ; 1 0 ^ 7 ) ) )
294 290 293 mpbi 
 |-  ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( ; ; 1 0 0 x. 4 ) / ( ; 1 0 ^ 7 ) )
295 8nn 
 |-  8 e. NN
296 nnrp 
 |-  ( 8 e. NN -> 8 e. RR+ )
297 295 296 ax-mp 
 |-  8 e. RR+
298 59 297 rpdp2cl 
 |-  _ 4 8 e. RR+
299 19 298 rpdp2cl 
 |-  _ 2 _ 4 8 e. RR+
300 19 299 rpdp2cl 
 |-  _ 2 _ 2 _ 4 8 e. RR+
301 59 300 dpgti 
 |-  4 < ( 4 . _ 2 _ 2 _ 4 8 )
302 72 recni 
 |-  ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. CC
303 198 recni 
 |-  ( ; 1 0 ^ 7 ) e. CC
304 302 303 mulcli 
 |-  ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) e. CC
305 16 123 gtneii 
 |-  ; 1 0 =/= 0
306 190 305 pm3.2i 
 |-  ( ; 1 0 e. CC /\ ; 1 0 =/= 0 )
307 287 recni 
 |-  ; ; 1 0 0 e. CC
308 286 nnne0i 
 |-  ; ; 1 0 0 =/= 0
309 307 308 pm3.2i 
 |-  ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 )
310 divdiv1 
 |-  ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) e. CC /\ ( ; 1 0 e. CC /\ ; 1 0 =/= 0 ) /\ ( ; ; 1 0 0 e. CC /\ ; ; 1 0 0 =/= 0 ) ) -> ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) / ; 1 0 ) / ; ; 1 0 0 ) = ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) / ( ; 1 0 x. ; ; 1 0 0 ) ) )
311 304 306 309 310 mp3an 
 |-  ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) / ; 1 0 ) / ; ; 1 0 0 ) = ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) / ( ; 1 0 x. ; ; 1 0 0 ) )
312 302 303 190 305 div23i 
 |-  ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) / ; 1 0 ) = ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) )
313 312 oveq1i 
 |-  ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) / ; 1 0 ) / ; ; 1 0 0 ) = ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) / ; ; 1 0 0 )
314 190 307 mulcli 
 |-  ( ; 1 0 x. ; ; 1 0 0 ) e. CC
315 190 307 305 308 mulne0i 
 |-  ( ; 1 0 x. ; ; 1 0 0 ) =/= 0
316 302 303 314 315 divassi 
 |-  ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) / ( ; 1 0 x. ; ; 1 0 0 ) ) = ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ( ; 1 0 ^ 7 ) / ( ; 1 0 x. ; ; 1 0 0 ) ) )
317 expp1 
 |-  ( ( ; 1 0 e. CC /\ 2 e. NN0 ) -> ( ; 1 0 ^ ( 2 + 1 ) ) = ( ( ; 1 0 ^ 2 ) x. ; 1 0 ) )
318 190 19 317 mp2an 
 |-  ( ; 1 0 ^ ( 2 + 1 ) ) = ( ( ; 1 0 ^ 2 ) x. ; 1 0 )
319 sq10 
 |-  ( ; 1 0 ^ 2 ) = ; ; 1 0 0
320 319 oveq1i 
 |-  ( ( ; 1 0 ^ 2 ) x. ; 1 0 ) = ( ; ; 1 0 0 x. ; 1 0 )
321 307 190 mulcomi 
 |-  ( ; ; 1 0 0 x. ; 1 0 ) = ( ; 1 0 x. ; ; 1 0 0 )
322 318 320 321 3eqtrri 
 |-  ( ; 1 0 x. ; ; 1 0 0 ) = ( ; 1 0 ^ ( 2 + 1 ) )
323 2p1e3 
 |-  ( 2 + 1 ) = 3
324 323 oveq2i 
 |-  ( ; 1 0 ^ ( 2 + 1 ) ) = ( ; 1 0 ^ 3 )
325 322 324 eqtri 
 |-  ( ; 1 0 x. ; ; 1 0 0 ) = ( ; 1 0 ^ 3 )
326 325 oveq2i 
 |-  ( ( ; 1 0 ^ 7 ) / ( ; 1 0 x. ; ; 1 0 0 ) ) = ( ( ; 1 0 ^ 7 ) / ( ; 1 0 ^ 3 ) )
327 74 nn0zi 
 |-  3 e. ZZ
328 199 327 pm3.2i 
 |-  ( 7 e. ZZ /\ 3 e. ZZ )
329 expsub 
 |-  ( ( ( ; 1 0 e. CC /\ ; 1 0 =/= 0 ) /\ ( 7 e. ZZ /\ 3 e. ZZ ) ) -> ( ; 1 0 ^ ( 7 - 3 ) ) = ( ( ; 1 0 ^ 7 ) / ( ; 1 0 ^ 3 ) ) )
330 306 328 329 mp2an 
 |-  ( ; 1 0 ^ ( 7 - 3 ) ) = ( ( ; 1 0 ^ 7 ) / ( ; 1 0 ^ 3 ) )
331 7cn 
 |-  7 e. CC
332 4p3e7 
 |-  ( 4 + 3 ) = 7
333 263 112 332 addcomli 
 |-  ( 3 + 4 ) = 7
334 331 112 263 333 subaddrii 
 |-  ( 7 - 3 ) = 4
335 334 oveq2i 
 |-  ( ; 1 0 ^ ( 7 - 3 ) ) = ( ; 1 0 ^ 4 )
336 326 330 335 3eqtr2i 
 |-  ( ( ; 1 0 ^ 7 ) / ( ; 1 0 x. ; ; 1 0 0 ) ) = ( ; 1 0 ^ 4 )
337 336 oveq2i 
 |-  ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ( ; 1 0 ^ 7 ) / ( ; 1 0 x. ; ; 1 0 0 ) ) ) = ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 4 ) )
338 173 numexp1 
 |-  ( ; 1 0 ^ 1 ) = ; 1 0
339 338 oveq2i 
 |-  ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 1 ) ) = ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) x. ; 1 0 )
340 59 300 rpdp2cl 
 |-  _ 4 _ 2 _ 2 _ 4 8 e. RR+
341 25 nnzi 
 |-  1 e. ZZ
342 89 nnzi 
 |-  2 e. ZZ
343 26 340 98 341 342 dpexpp1 
 |-  ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 1 ) ) = ( ( 0 . _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 2 ) )
344 26 340 rpdp2cl 
 |-  _ 0 _ 4 _ 2 _ 2 _ 4 8 e. RR+
345 26 344 323 342 327 dpexpp1 
 |-  ( ( 0 . _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 2 ) ) = ( ( 0 . _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 3 ) )
346 26 344 rpdp2cl 
 |-  _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 e. RR+
347 3p1e4 
 |-  ( 3 + 1 ) = 4
348 26 346 347 327 247 dpexpp1 
 |-  ( ( 0 . _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 3 ) ) = ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 4 ) )
349 343 345 348 3eqtri 
 |-  ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 1 ) ) = ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 4 ) )
350 59 300 0dp2dp 
 |-  ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) x. ; 1 0 ) = ( 4 . _ 2 _ 2 _ 4 8 )
351 339 349 350 3eqtr3i 
 |-  ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 4 ) ) = ( 4 . _ 2 _ 2 _ 4 8 )
352 316 337 351 3eqtri 
 |-  ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( ; 1 0 ^ 7 ) ) / ( ; 1 0 x. ; ; 1 0 0 ) ) = ( 4 . _ 2 _ 2 _ 4 8 )
353 311 313 352 3eqtr3i 
 |-  ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) / ; ; 1 0 0 ) = ( 4 . _ 2 _ 2 _ 4 8 )
354 301 353 breqtrri 
 |-  4 < ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) / ; ; 1 0 0 )
355 72 18 305 redivcli 
 |-  ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) e. RR
356 355 198 remulcli 
 |-  ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) e. RR
357 286 nngt0i 
 |-  0 < ; ; 1 0 0
358 287 357 pm3.2i 
 |-  ( ; ; 1 0 0 e. RR /\ 0 < ; ; 1 0 0 )
359 ltmuldiv2 
 |-  ( ( 4 e. RR /\ ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) e. RR /\ ( ; ; 1 0 0 e. RR /\ 0 < ; ; 1 0 0 ) ) -> ( ( ; ; 1 0 0 x. 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) <-> 4 < ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) / ; ; 1 0 0 ) ) )
360 3 356 358 359 mp3an 
 |-  ( ( ; ; 1 0 0 x. 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) <-> 4 < ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) / ; ; 1 0 0 ) )
361 354 360 mpbir 
 |-  ( ; ; 1 0 0 x. 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) )
362 ltdivmul2 
 |-  ( ( ( ; ; 1 0 0 x. 4 ) e. RR /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) e. RR /\ ( ( ; 1 0 ^ 7 ) e. RR /\ 0 < ( ; 1 0 ^ 7 ) ) ) -> ( ( ( ; ; 1 0 0 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) <-> ( ; ; 1 0 0 x. 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) ) )
363 291 355 226 362 mp3an 
 |-  ( ( ( ; ; 1 0 0 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) <-> ( ; ; 1 0 0 x. 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) x. ( ; 1 0 ^ 7 ) ) )
364 361 363 mpbir 
 |-  ( ( ; ; 1 0 0 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 )
365 291 198 277 redivcli 
 |-  ( ( ; ; 1 0 0 x. 4 ) / ( ; 1 0 ^ 7 ) ) e. RR
366 279 365 355 lttri 
 |-  ( ( ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( ; ; 1 0 0 x. 4 ) / ( ; 1 0 ^ 7 ) ) /\ ( ( ; ; 1 0 0 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ) -> ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) )
367 294 364 366 mp2an 
 |-  ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 )
368 226 simpli 
 |-  ( ; 1 0 ^ 7 ) e. RR
369 273 368 277 redivcli 
 |-  ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) e. RR
370 55 369 355 lttri 
 |-  ( ( ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) /\ ( ( ; 2 7 x. 4 ) / ( ; 1 0 ^ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ) -> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) )
371 281 367 370 mp2an 
 |-  ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 )
372 125 124 mpbi 
 |-  ( ; 1 0 e. RR /\ 0 < ; 1 0 )
373 ltmuldiv2 
 |-  ( ( ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) e. RR /\ ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) e. RR /\ ( ; 1 0 e. RR /\ 0 < ; 1 0 ) ) -> ( ( ; 1 0 x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) <-> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ) )
374 55 72 372 373 mp3an 
 |-  ( ( ; 1 0 x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) <-> ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) )
375 371 374 mpbir 
 |-  ( ; 1 0 x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 )
376 12 55 remulcli 
 |-  ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) e. RR
377 18 55 remulcli 
 |-  ( ; 1 0 x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) e. RR
378 376 377 72 lttri 
 |-  ( ( ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( ; 1 0 x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) /\ ( ; 1 0 x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) ) -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )
379 189 375 378 mp2an 
 |-  ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 )
380 379 a1i 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` ( ; 1 0 ^ ; 2 7 ) ) / ( sqrt ` ( ; 1 0 ^ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )
381 47 57 73 162 380 lelttrd 
 |-  ( ( N e. NN0 /\ ( ; 1 0 ^ ; 2 7 ) <_ N ) -> ( ( 7 . _ 3 _ 4 8 ) x. ( ( log ` N ) / ( sqrt ` N ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )