Theorem hgt750lem

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

	Ref	Expression
Assertion	hgt750lem	$$⊢\left(N\in {\mathbb{N}}_0\wedge {10}^{27}\le N\right)\to \mathrm{7<mi\; href="df-dp.html">.</mi>348}\left(\frac{\log N}{\sqrt{N}}\right)<\mathrm{0<mi\; href="df-dp.html">.</mi>00042248}$$

Proof

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