hgt750lem

		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 ) )

Metamath Proof Explorer

Theorem hgt750lem

Proof