hgt750lem

		Ref	Expression
	Assertion	hgt750lem	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )

Proof

Step	Hyp	Ref	Expression
1		7nn0	⊢ 7 ∈ ℕ₀
2		3re	⊢ 3 ∈ ℝ
3		4re	⊢ 4 ∈ ℝ
4		8re	⊢ 8 ∈ ℝ
5	3 4	pm3.2i	⊢ ( 4 ∈ ℝ ∧ 8 ∈ ℝ )
6		dp2cl	⊢ ( ( 4 ∈ ℝ ∧ 8 ∈ ℝ ) → _ 4 8 ∈ ℝ )
7	5 6	ax-mp	⊢ _ 4 8 ∈ ℝ
8	2 7	pm3.2i	⊢ ( 3 ∈ ℝ ∧ _ 4 8 ∈ ℝ )
9		dp2cl	⊢ ( ( 3 ∈ ℝ ∧ _ 4 8 ∈ ℝ ) → _ 3 _ 4 8 ∈ ℝ )
10	8 9	ax-mp	⊢ _ 3 _ 4 8 ∈ ℝ
11		dpcl	⊢ ( ( 7 ∈ ℕ₀ ∧ _ 3 _ 4 8 ∈ ℝ ) → ( 7 . _ 3 _ 4 8 ) ∈ ℝ )
12	1 10 11	mp2an	⊢ ( 7 . _ 3 _ 4 8 ) ∈ ℝ
13	12	a1i	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( 7 . _ 3 _ 4 8 ) ∈ ℝ )
14		nn0re	⊢ ( 𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ )
15	14	adantr	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → 𝑁 ∈ ℝ )
16		0re	⊢ 0 ∈ ℝ
17	16	a1i	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → 0 ∈ ℝ )
18		10re	⊢ ; 1 0 ∈ ℝ
19		2nn0	⊢ 2 ∈ ℕ₀
20	19 1	deccl	⊢ ; 2 7 ∈ ℕ₀
21		reexpcl	⊢ ( ( ; 1 0 ∈ ℝ ∧ ; 2 7 ∈ ℕ₀ ) → ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ )
22	18 20 21	mp2an	⊢ ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ
23	22	a1i	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ )
24		0lt1	⊢ 0 < 1
25		1nn	⊢ 1 ∈ ℕ
26		0nn0	⊢ 0 ∈ ℕ₀
27		1nn0	⊢ 1 ∈ ℕ₀
28		1re	⊢ 1 ∈ ℝ
29		9re	⊢ 9 ∈ ℝ
30		1lt9	⊢ 1 < 9
31	28 29 30	ltleii	⊢ 1 ≤ 9
32	25 26 27 31	declei	⊢ 1 ≤ ; 1 0
33		expge1	⊢ ( ( ; 1 0 ∈ ℝ ∧ ; 2 7 ∈ ℕ₀ ∧ 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	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → 0 < ( ; 1 0 ↑ ; 2 7 ) )
38		simpr	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 )
39	17 23 15 37 38	ltletrd	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → 0 < 𝑁 )
40	15 39	elrpd	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → 𝑁 ∈ ℝ⁺ )
41	40	relogcld	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( log ‘ 𝑁 ) ∈ ℝ )
42	40	rpge0d	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → 0 ≤ 𝑁 )
43	15 42	resqrtcld	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( √ ‘ 𝑁 ) ∈ ℝ )
44	40	sqrtgt0d	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → 0 < ( √ ‘ 𝑁 ) )
45	17 44	gtned	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( √ ‘ 𝑁 ) ≠ 0 )
46	41 43 45	redivcld	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ∈ ℝ )
47	13 46	remulcld	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
48		elrp	⊢ ( ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ⁺ ↔ ( ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ ∧ 0 < ( ; 1 0 ↑ ; 2 7 ) ) )
49	22 36 48	mpbir2an	⊢ ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ⁺
50		relogcl	⊢ ( ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ⁺ → ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) ∈ ℝ )
51	49 50	ax-mp	⊢ ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) ∈ ℝ
52	22 36	sqrtpclii	⊢ ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ∈ ℝ
53	22 36	sqrtgt0ii	⊢ 0 < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) )
54	16 53	gtneii	⊢ ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ≠ 0
55	51 52 54	redivcli	⊢ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ∈ ℝ
56	55	a1i	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ∈ ℝ )
57	13 56	remulcld	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) ∈ ℝ )
58		qssre	⊢ ℚ ⊆ ℝ
59		4nn0	⊢ 4 ∈ ℕ₀
60		nn0ssq	⊢ ℕ₀ ⊆ ℚ
61		8nn0	⊢ 8 ∈ ℕ₀
62	60 61	sselii	⊢ 8 ∈ ℚ
63	59 62	dp2clq	⊢ _ 4 8 ∈ ℚ
64	19 63	dp2clq	⊢ _ 2 _ 4 8 ∈ ℚ
65	19 64	dp2clq	⊢ _ 2 _ 2 _ 4 8 ∈ ℚ
66	59 65	dp2clq	⊢ _ 4 _ 2 _ 2 _ 4 8 ∈ ℚ
67	26 66	dp2clq	⊢ _ 0 _ 4 _ 2 _ 2 _ 4 8 ∈ ℚ
68	26 67	dp2clq	⊢ _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ∈ ℚ
69	26 68	dp2clq	⊢ _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ∈ ℚ
70	58 69	sselii	⊢ _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ∈ ℝ
71		dpcl	⊢ ( ( 0 ∈ ℕ₀ ∧ _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ∈ ℝ ) → ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) ∈ ℝ )
72	26 70 71	mp2an	⊢ ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) ∈ ℝ
73	72	a1i	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) ∈ ℝ )
74		3nn0	⊢ 3 ∈ ℕ₀
75		8pos	⊢ 0 < 8
76		elrp	⊢ ( 8 ∈ ℝ⁺ ↔ ( 8 ∈ ℝ ∧ 0 < 8 ) )
77	4 75 76	mpbir2an	⊢ 8 ∈ ℝ⁺
78	59 77	rpdp2cl	⊢ _ 4 8 ∈ ℝ⁺
79	74 78	rpdp2cl	⊢ _ 3 _ 4 8 ∈ ℝ⁺
80	1 79	rpdpcl	⊢ ( 7 . _ 3 _ 4 8 ) ∈ ℝ⁺
81		elrp	⊢ ( ( 7 . _ 3 _ 4 8 ) ∈ ℝ⁺ ↔ ( ( 7 . _ 3 _ 4 8 ) ∈ ℝ ∧ 0 < ( 7 . _ 3 _ 4 8 ) ) )
82	80 81	mpbi	⊢ ( ( 7 . _ 3 _ 4 8 ) ∈ ℝ ∧ 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	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → 0 ≤ ( 7 . _ 3 _ 4 8 ) )
86	49	a1i	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ⁺ )
87		2cn	⊢ 2 ∈ ℂ
88	87	mullidi	⊢ ( 1 · 2 ) = 2
89		2nn	⊢ 2 ∈ ℕ
90	89 1 27 31	declei	⊢ 1 ≤ ; 2 7
91		2pos	⊢ 0 < 2
92	20	nn0rei	⊢ ; 2 7 ∈ ℝ
93		2re	⊢ 2 ∈ ℝ
94	28 92 93	lemul1i	⊢ ( 0 < 2 → ( 1 ≤ ; 2 7 ↔ ( 1 · 2 ) ≤ ( ; 2 7 · 2 ) ) )
95	91 94	ax-mp	⊢ ( 1 ≤ ; 2 7 ↔ ( 1 · 2 ) ≤ ( ; 2 7 · 2 ) )
96	90 95	mpbi	⊢ ( 1 · 2 ) ≤ ( ; 2 7 · 2 )
97	88 96	eqbrtrri	⊢ 2 ≤ ( ; 2 7 · 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 ∈ ℝ⁺
103		3rp	⊢ 3 ∈ ℝ⁺
104		logltb	⊢ ( ( e ∈ ℝ⁺ ∧ 3 ∈ ℝ⁺ ) → ( 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 ∈ ℝ⁺ → ( log ‘ 3 ) ∈ ℝ )
109	103 108	ax-mp	⊢ ( log ‘ 3 ) ∈ ℝ
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 ∈ ℂ
113		3ne0	⊢ 3 ≠ 0
114		logmul2	⊢ ( ( 3 ∈ ℂ ∧ 3 ≠ 0 ∧ 3 ∈ ℝ⁺ ) → ( log ‘ ( 3 · 3 ) ) = ( ( log ‘ 3 ) + ( log ‘ 3 ) ) )
115	112 113 103 114	mp3an	⊢ ( log ‘ ( 3 · 3 ) ) = ( ( log ‘ 3 ) + ( log ‘ 3 ) )
116		3t3e9	⊢ ( 3 · 3 ) = 9
117	116	fveq2i	⊢ ( log ‘ ( 3 · 3 ) ) = ( log ‘ 9 )
118		9lt10	⊢ 9 < ; 1 0
119	29 18 118	ltleii	⊢ 9 ≤ ; 1 0
120		9pos	⊢ 0 < 9
121		elrp	⊢ ( 9 ∈ ℝ⁺ ↔ ( 9 ∈ ℝ ∧ 0 < 9 ) )
122	29 120 121	mpbir2an	⊢ 9 ∈ ℝ⁺
123		10pos	⊢ 0 < ; 1 0
124		elrp	⊢ ( ; 1 0 ∈ ℝ⁺ ↔ ( ; 1 0 ∈ ℝ ∧ 0 < ; 1 0 ) )
125	18 123 124	mpbir2an	⊢ ; 1 0 ∈ ℝ⁺
126		logleb	⊢ ( ( 9 ∈ ℝ⁺ ∧ ; 1 0 ∈ ℝ⁺ ) → ( 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 · 3 ) ) ≤ ( log ‘ ; 1 0 )
130	115 129	eqbrtrri	⊢ ( ( log ‘ 3 ) + ( log ‘ 3 ) ) ≤ ( log ‘ ; 1 0 )
131	28 28	readdcli	⊢ ( 1 + 1 ) ∈ ℝ
132	109 109	readdcli	⊢ ( ( log ‘ 3 ) + ( log ‘ 3 ) ) ∈ ℝ
133		relogcl	⊢ ( ; 1 0 ∈ ℝ⁺ → ( log ‘ ; 1 0 ) ∈ ℝ )
134	125 133	ax-mp	⊢ ( log ‘ ; 1 0 ) ∈ ℝ
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 · 2 ) ≤ ( ; 2 7 · ( log ‘ ; 1 0 ) ) ) )
143	141 142	ax-mp	⊢ ( 2 ≤ ( log ‘ ; 1 0 ) ↔ ( ; 2 7 · 2 ) ≤ ( ; 2 7 · ( log ‘ ; 1 0 ) ) )
144	139 143	mpbi	⊢ ( ; 2 7 · 2 ) ≤ ( ; 2 7 · ( log ‘ ; 1 0 ) )
145	92 93	remulcli	⊢ ( ; 2 7 · 2 ) ∈ ℝ
146	20	nn0zi	⊢ ; 2 7 ∈ ℤ
147		relogexp	⊢ ( ( ; 1 0 ∈ ℝ⁺ ∧ ; 2 7 ∈ ℤ ) → ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) = ( ; 2 7 · ( log ‘ ; 1 0 ) ) )
148	125 146 147	mp2an	⊢ ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) = ( ; 2 7 · ( log ‘ ; 1 0 ) )
149	148 51	eqeltrri	⊢ ( ; 2 7 · ( log ‘ ; 1 0 ) ) ∈ ℝ
150	93 145 149	letri	⊢ ( ( 2 ≤ ( ; 2 7 · 2 ) ∧ ( ; 2 7 · 2 ) ≤ ( ; 2 7 · ( log ‘ ; 1 0 ) ) ) → 2 ≤ ( ; 2 7 · ( log ‘ ; 1 0 ) ) )
151	97 144 150	mp2an	⊢ 2 ≤ ( ; 2 7 · ( log ‘ ; 1 0 ) )
152		relogef	⊢ ( 2 ∈ ℝ → ( 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 ∈ ℝ → ( exp ‘ 2 ) ∈ ℝ⁺ )
156	93 155	ax-mp	⊢ ( exp ‘ 2 ) ∈ ℝ⁺
157		logleb	⊢ ( ( ( exp ‘ 2 ) ∈ ℝ⁺ ∧ ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ⁺ ) → ( ( 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	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( exp ‘ 2 ) ≤ ( ; 1 0 ↑ ; 2 7 ) )
161	86 40 160 38	logdivsqrle	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ≤ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) )
162	46 56 13 85 161	lemul2ad	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) ≤ ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 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 ∈ ℝ
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 ∈ ℕ₀
174	173	numexp0	⊢ ( ; 1 0 ↑ 0 ) = 1
175		0z	⊢ 0 ∈ ℤ
176	18 175 146	3pm3.2i	⊢ ( ; 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ ; 2 7 ∈ ℤ )
177		1lt10	⊢ 1 < ; 1 0
178	177 141	pm3.2i	⊢ ( 1 < ; 1 0 ∧ 0 < ; 2 7 )
179		ltexp2a	⊢ ( ( ( ; 1 0 ∈ ℝ ∧ 0 ∈ ℤ ∧ ; 2 7 ∈ ℤ ) ∧ ( 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 ) ∈ ℝ⁺ → ( 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 < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) → 0 < ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) )
186	184 53 185	mp2an	⊢ 0 < ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) )
187	12 18 55	ltmul1i	⊢ ( 0 < ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) → ( ( 7 . _ 3 _ 4 8 ) < ; 1 0 ↔ ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( ; 1 0 · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) ) )
188	186 187	ax-mp	⊢ ( ( 7 . _ 3 _ 4 8 ) < ; 1 0 ↔ ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( ; 1 0 · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) )
189	172 188	mpbi	⊢ ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( ; 1 0 · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) )
190	18	recni	⊢ ; 1 0 ∈ ℂ
191		expmul	⊢ ( ( ; 1 0 ∈ ℂ ∧ 7 ∈ ℕ₀ ∧ 2 ∈ ℕ₀ ) → ( ; 1 0 ↑ ( 7 · 2 ) ) = ( ( ; 1 0 ↑ 7 ) ↑ 2 ) )
192	190 1 19 191	mp3an	⊢ ( ; 1 0 ↑ ( 7 · 2 ) ) = ( ( ; 1 0 ↑ 7 ) ↑ 2 )
193		7t2e14	⊢ ( 7 · 2 ) = ; 1 4
194	193	oveq2i	⊢ ( ; 1 0 ↑ ( 7 · 2 ) ) = ( ; 1 0 ↑ ; 1 4 )
195	192 194	eqtr3i	⊢ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) = ( ; 1 0 ↑ ; 1 4 )
196	195	fveq2i	⊢ ( √ ‘ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) = ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) )
197		reexpcl	⊢ ( ( ; 1 0 ∈ ℝ ∧ 7 ∈ ℕ₀ ) → ( ; 1 0 ↑ 7 ) ∈ ℝ )
198	18 1 197	mp2an	⊢ ( ; 1 0 ↑ 7 ) ∈ ℝ
199	1	nn0zi	⊢ 7 ∈ ℤ
200		expgt0	⊢ ( ( ; 1 0 ∈ ℝ ∧ 7 ∈ ℤ ∧ 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 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ 7 ) ) → ( √ ‘ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) = ( ; 1 0 ↑ 7 ) )
204	198 202 203	mp2an	⊢ ( √ ‘ ( ( ; 1 0 ↑ 7 ) ↑ 2 ) ) = ( ; 1 0 ↑ 7 )
205	196 204	eqtr3i	⊢ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) = ( ; 1 0 ↑ 7 )
206	27 59	deccl	⊢ ; 1 4 ∈ ℕ₀
207	206	nn0zi	⊢ ; 1 4 ∈ ℤ
208	18 207 146	3pm3.2i	⊢ ( ; 1 0 ∈ ℝ ∧ ; 1 4 ∈ ℤ ∧ ; 2 7 ∈ ℤ )
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 ∈ ℝ ∧ ; 1 4 ∈ ℤ ∧ ; 2 7 ∈ ℤ ) ∧ ( 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 ∈ ℝ ∧ ; 1 4 ∈ ℕ₀ ) → ( ; 1 0 ↑ ; 1 4 ) ∈ ℝ )
215	18 206 214	mp2an	⊢ ( ; 1 0 ↑ ; 1 4 ) ∈ ℝ
216		expgt0	⊢ ( ( ; 1 0 ∈ ℝ ∧ ; 1 4 ∈ ℤ ∧ 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 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 1 4 ) )
220	16 22 36	ltleii	⊢ 0 ≤ ( ; 1 0 ↑ ; 2 7 )
221	22 220	pm3.2i	⊢ ( ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 2 7 ) )
222		sqrtlt	⊢ ( ( ( ( ; 1 0 ↑ ; 1 4 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 1 4 ) ) ∧ ( ( ; 1 0 ↑ ; 2 7 ) ∈ ℝ ∧ 0 ≤ ( ; 1 0 ↑ ; 2 7 ) ) ) → ( ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 ) ↔ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) )
223	219 221 222	mp2an	⊢ ( ( ; 1 0 ↑ ; 1 4 ) < ( ; 1 0 ↑ ; 2 7 ) ↔ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) )
224	213 223	mpbi	⊢ ( √ ‘ ( ; 1 0 ↑ ; 1 4 ) ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) )
225	205 224	eqbrtrri	⊢ ( ; 1 0 ↑ 7 ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) )
226	198 201	pm3.2i	⊢ ( ( ; 1 0 ↑ 7 ) ∈ ℝ ∧ 0 < ( ; 1 0 ↑ 7 ) )
227	52 53	pm3.2i	⊢ ( ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ∈ ℝ ∧ 0 < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) )
228	51 184	pm3.2i	⊢ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) ∈ ℝ ∧ 0 < ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) )
229		ltdiv2	⊢ ( ( ( ( ; 1 0 ↑ 7 ) ∈ ℝ ∧ 0 < ( ; 1 0 ↑ 7 ) ) ∧ ( ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ∈ ℝ ∧ 0 < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ∧ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) ∈ ℝ ∧ 0 < ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) → ( ( ; 1 0 ↑ 7 ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ↔ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( ; 1 0 ↑ 7 ) ) ) )
230	226 227 228 229	mp3an	⊢ ( ( ; 1 0 ↑ 7 ) < ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ↔ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( ; 1 0 ↑ 7 ) ) )
231	225 230	mpbi	⊢ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( ; 1 0 ↑ 7 ) )
232		6nn	⊢ 6 ∈ ℕ
233	232	nngt0i	⊢ 0 < 6
234	27 26 232 233	declt	⊢ ; 1 0 < ; 1 6
235		6nn0	⊢ 6 ∈ ℕ₀
236	27 235	deccl	⊢ ; 1 6 ∈ ℕ₀
237	236	nn0rei	⊢ ; 1 6 ∈ ℝ
238	25 235 26 123	declti	⊢ 0 < ; 1 6
239		elrp	⊢ ( ; 1 6 ∈ ℝ⁺ ↔ ( ; 1 6 ∈ ℝ ∧ 0 < ; 1 6 ) )
240	237 238 239	mpbir2an	⊢ ; 1 6 ∈ ℝ⁺
241		logltb	⊢ ( ( ; 1 0 ∈ ℝ⁺ ∧ ; 1 6 ∈ ℝ⁺ ) → ( ; 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 ∈ ℝ⁺
247	59	nn0zi	⊢ 4 ∈ ℤ
248		relogexp	⊢ ( ( 2 ∈ ℝ⁺ ∧ 4 ∈ ℤ ) → ( log ‘ ( 2 ↑ 4 ) ) = ( 4 · ( log ‘ 2 ) ) )
249	246 247 248	mp2an	⊢ ( log ‘ ( 2 ↑ 4 ) ) = ( 4 · ( log ‘ 2 ) )
250	245 249	eqtr3i	⊢ ( log ‘ ; 1 6 ) = ( 4 · ( log ‘ 2 ) )
251	243 250	breqtri	⊢ ( log ‘ ; 1 0 ) < ( 4 · ( log ‘ 2 ) )
252	100	simpli	⊢ 2 < e
253		logltb	⊢ ( ( 2 ∈ ℝ⁺ ∧ e ∈ ℝ⁺ ) → ( 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 ∈ ℝ⁺ → ( log ‘ 2 ) ∈ ℝ )
259	246 258	ax-mp	⊢ ( log ‘ 2 ) ∈ ℝ
260	259 28 3	ltmul2i	⊢ ( 0 < 4 → ( ( log ‘ 2 ) < 1 ↔ ( 4 · ( log ‘ 2 ) ) < ( 4 · 1 ) ) )
261	257 260	ax-mp	⊢ ( ( log ‘ 2 ) < 1 ↔ ( 4 · ( log ‘ 2 ) ) < ( 4 · 1 ) )
262	256 261	mpbi	⊢ ( 4 · ( log ‘ 2 ) ) < ( 4 · 1 )
263		4cn	⊢ 4 ∈ ℂ
264	263	mulridi	⊢ ( 4 · 1 ) = 4
265	262 264	breqtri	⊢ ( 4 · ( log ‘ 2 ) ) < 4
266	3 259	remulcli	⊢ ( 4 · ( log ‘ 2 ) ) ∈ ℝ
267	134 266 3	lttri	⊢ ( ( ( log ‘ ; 1 0 ) < ( 4 · ( log ‘ 2 ) ) ∧ ( 4 · ( 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 · ( log ‘ ; 1 0 ) ) < ( ; 2 7 · 4 ) ) )
270	141 269	ax-mp	⊢ ( ( log ‘ ; 1 0 ) < 4 ↔ ( ; 2 7 · ( log ‘ ; 1 0 ) ) < ( ; 2 7 · 4 ) )
271	268 270	mpbi	⊢ ( ; 2 7 · ( log ‘ ; 1 0 ) ) < ( ; 2 7 · 4 )
272	148 271	eqbrtri	⊢ ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) < ( ; 2 7 · 4 )
273	92 3	remulcli	⊢ ( ; 2 7 · 4 ) ∈ ℝ
274	51 273 198	ltdiv1i	⊢ ( 0 < ( ; 1 0 ↑ 7 ) → ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) < ( ; 2 7 · 4 ) ↔ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( ; 1 0 ↑ 7 ) ) < ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) ) )
275	201 274	ax-mp	⊢ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) < ( ; 2 7 · 4 ) ↔ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( ; 1 0 ↑ 7 ) ) < ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) )
276	272 275	mpbi	⊢ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( ; 1 0 ↑ 7 ) ) < ( ( ; 2 7 · 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 ) ) ∈ ℝ
279	273 198 277	redivcli	⊢ ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) ∈ ℝ
280	55 278 279	lttri	⊢ ( ( ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( ; 1 0 ↑ 7 ) ) ∧ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( ; 1 0 ↑ 7 ) ) < ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) ) → ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) )
281	231 276 280	mp2an	⊢ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( ; 2 7 · 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 ∈ ℕ
286	285	decnncl2	⊢ ; ; 1 0 0 ∈ ℕ
287	286	nnrei	⊢ ; ; 1 0 0 ∈ ℝ
288	92 287 3	ltmul1i	⊢ ( 0 < 4 → ( ; 2 7 < ; ; 1 0 0 ↔ ( ; 2 7 · 4 ) < ( ; ; 1 0 0 · 4 ) ) )
289	257 288	ax-mp	⊢ ( ; 2 7 < ; ; 1 0 0 ↔ ( ; 2 7 · 4 ) < ( ; ; 1 0 0 · 4 ) )
290	284 289	mpbi	⊢ ( ; 2 7 · 4 ) < ( ; ; 1 0 0 · 4 )
291	287 3	remulcli	⊢ ( ; ; 1 0 0 · 4 ) ∈ ℝ
292	273 291 198	ltdiv1i	⊢ ( 0 < ( ; 1 0 ↑ 7 ) → ( ( ; 2 7 · 4 ) < ( ; ; 1 0 0 · 4 ) ↔ ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( ; ; 1 0 0 · 4 ) / ( ; 1 0 ↑ 7 ) ) ) )
293	201 292	ax-mp	⊢ ( ( ; 2 7 · 4 ) < ( ; ; 1 0 0 · 4 ) ↔ ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( ; ; 1 0 0 · 4 ) / ( ; 1 0 ↑ 7 ) ) )
294	290 293	mpbi	⊢ ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( ; ; 1 0 0 · 4 ) / ( ; 1 0 ↑ 7 ) )
295		8nn	⊢ 8 ∈ ℕ
296		nnrp	⊢ ( 8 ∈ ℕ → 8 ∈ ℝ⁺ )
297	295 296	ax-mp	⊢ 8 ∈ ℝ⁺
298	59 297	rpdp2cl	⊢ _ 4 8 ∈ ℝ⁺
299	19 298	rpdp2cl	⊢ _ 2 _ 4 8 ∈ ℝ⁺
300	19 299	rpdp2cl	⊢ _ 2 _ 2 _ 4 8 ∈ ℝ⁺
301	59 300	dpgti	⊢ 4 < ( 4 . _ 2 _ 2 _ 4 8 )
302	72	recni	⊢ ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) ∈ ℂ
303	198	recni	⊢ ( ; 1 0 ↑ 7 ) ∈ ℂ
304	302 303	mulcli	⊢ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) ∈ ℂ
305	16 123	gtneii	⊢ ; 1 0 ≠ 0
306	190 305	pm3.2i	⊢ ( ; 1 0 ∈ ℂ ∧ ; 1 0 ≠ 0 )
307	287	recni	⊢ ; ; 1 0 0 ∈ ℂ
308	286	nnne0i	⊢ ; ; 1 0 0 ≠ 0
309	307 308	pm3.2i	⊢ ( ; ; 1 0 0 ∈ ℂ ∧ ; ; 1 0 0 ≠ 0 )
310		divdiv1	⊢ ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) ∈ ℂ ∧ ( ; 1 0 ∈ ℂ ∧ ; 1 0 ≠ 0 ) ∧ ( ; ; 1 0 0 ∈ ℂ ∧ ; ; 1 0 0 ≠ 0 ) ) → ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) / ; 1 0 ) / ; ; 1 0 0 ) = ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) / ( ; 1 0 · ; ; 1 0 0 ) ) )
311	304 306 309 310	mp3an	⊢ ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) / ; 1 0 ) / ; ; 1 0 0 ) = ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) / ( ; 1 0 · ; ; 1 0 0 ) )
312	302 303 190 305	div23i	⊢ ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) / ; 1 0 ) = ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) )
313	312	oveq1i	⊢ ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) / ; 1 0 ) / ; ; 1 0 0 ) = ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) ) / ; ; 1 0 0 )
314	190 307	mulcli	⊢ ( ; 1 0 · ; ; 1 0 0 ) ∈ ℂ
315	190 307 305 308	mulne0i	⊢ ( ; 1 0 · ; ; 1 0 0 ) ≠ 0
316	302 303 314 315	divassi	⊢ ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) / ( ; 1 0 · ; ; 1 0 0 ) ) = ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ( ; 1 0 ↑ 7 ) / ( ; 1 0 · ; ; 1 0 0 ) ) )
317		expp1	⊢ ( ( ; 1 0 ∈ ℂ ∧ 2 ∈ ℕ₀ ) → ( ; 1 0 ↑ ( 2 + 1 ) ) = ( ( ; 1 0 ↑ 2 ) · ; 1 0 ) )
318	190 19 317	mp2an	⊢ ( ; 1 0 ↑ ( 2 + 1 ) ) = ( ( ; 1 0 ↑ 2 ) · ; 1 0 )
319		sq10	⊢ ( ; 1 0 ↑ 2 ) = ; ; 1 0 0
320	319	oveq1i	⊢ ( ( ; 1 0 ↑ 2 ) · ; 1 0 ) = ( ; ; 1 0 0 · ; 1 0 )
321	307 190	mulcomi	⊢ ( ; ; 1 0 0 · ; 1 0 ) = ( ; 1 0 · ; ; 1 0 0 )
322	318 320 321	3eqtrri	⊢ ( ; 1 0 · ; ; 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 · ; ; 1 0 0 ) = ( ; 1 0 ↑ 3 )
326	325	oveq2i	⊢ ( ( ; 1 0 ↑ 7 ) / ( ; 1 0 · ; ; 1 0 0 ) ) = ( ( ; 1 0 ↑ 7 ) / ( ; 1 0 ↑ 3 ) )
327	74	nn0zi	⊢ 3 ∈ ℤ
328	199 327	pm3.2i	⊢ ( 7 ∈ ℤ ∧ 3 ∈ ℤ )
329		expsub	⊢ ( ( ( ; 1 0 ∈ ℂ ∧ ; 1 0 ≠ 0 ) ∧ ( 7 ∈ ℤ ∧ 3 ∈ ℤ ) ) → ( ; 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 ∈ ℂ
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 · ; ; 1 0 0 ) ) = ( ; 1 0 ↑ 4 )
337	336	oveq2i	⊢ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ( ; 1 0 ↑ 7 ) / ( ; 1 0 · ; ; 1 0 0 ) ) ) = ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 4 ) )
338	173	numexp1	⊢ ( ; 1 0 ↑ 1 ) = ; 1 0
339	338	oveq2i	⊢ ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 1 ) ) = ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) · ; 1 0 )
340	59 300	rpdp2cl	⊢ _ 4 _ 2 _ 2 _ 4 8 ∈ ℝ⁺
341	25	nnzi	⊢ 1 ∈ ℤ
342	89	nnzi	⊢ 2 ∈ ℤ
343	26 340 98 341 342	dpexpp1	⊢ ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 1 ) ) = ( ( 0 . _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 2 ) )
344	26 340	rpdp2cl	⊢ _ 0 _ 4 _ 2 _ 2 _ 4 8 ∈ ℝ⁺
345	26 344 323 342 327	dpexpp1	⊢ ( ( 0 . _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 2 ) ) = ( ( 0 . _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 3 ) )
346	26 344	rpdp2cl	⊢ _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ∈ ℝ⁺
347		3p1e4	⊢ ( 3 + 1 ) = 4
348	26 346 347 327 247	dpexpp1	⊢ ( ( 0 . _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 3 ) ) = ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 4 ) )
349	343 345 348	3eqtri	⊢ ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 1 ) ) = ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 4 ) )
350	59 300	0dp2dp	⊢ ( ( 0 . _ 4 _ 2 _ 2 _ 4 8 ) · ; 1 0 ) = ( 4 . _ 2 _ 2 _ 4 8 )
351	339 349 350	3eqtr3i	⊢ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 4 ) ) = ( 4 . _ 2 _ 2 _ 4 8 )
352	316 337 351	3eqtri	⊢ ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) · ( ; 1 0 ↑ 7 ) ) / ( ; 1 0 · ; ; 1 0 0 ) ) = ( 4 . _ 2 _ 2 _ 4 8 )
353	311 313 352	3eqtr3i	⊢ ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 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 ) · ( ; 1 0 ↑ 7 ) ) / ; ; 1 0 0 )
355	72 18 305	redivcli	⊢ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ∈ ℝ
356	355 198	remulcli	⊢ ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) ) ∈ ℝ
357	286	nngt0i	⊢ 0 < ; ; 1 0 0
358	287 357	pm3.2i	⊢ ( ; ; 1 0 0 ∈ ℝ ∧ 0 < ; ; 1 0 0 )
359		ltmuldiv2	⊢ ( ( 4 ∈ ℝ ∧ ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) ) ∈ ℝ ∧ ( ; ; 1 0 0 ∈ ℝ ∧ 0 < ; ; 1 0 0 ) ) → ( ( ; ; 1 0 0 · 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) ) ↔ 4 < ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) ) / ; ; 1 0 0 ) ) )
360	3 356 358 359	mp3an	⊢ ( ( ; ; 1 0 0 · 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) ) ↔ 4 < ( ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) ) / ; ; 1 0 0 ) )
361	354 360	mpbir	⊢ ( ; ; 1 0 0 · 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) )
362		ltdivmul2	⊢ ( ( ( ; ; 1 0 0 · 4 ) ∈ ℝ ∧ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ∈ ℝ ∧ ( ( ; 1 0 ↑ 7 ) ∈ ℝ ∧ 0 < ( ; 1 0 ↑ 7 ) ) ) → ( ( ( ; ; 1 0 0 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ↔ ( ; ; 1 0 0 · 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) ) ) )
363	291 355 226 362	mp3an	⊢ ( ( ( ; ; 1 0 0 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ↔ ( ; ; 1 0 0 · 4 ) < ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) · ( ; 1 0 ↑ 7 ) ) )
364	361 363	mpbir	⊢ ( ( ; ; 1 0 0 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 )
365	291 198 277	redivcli	⊢ ( ( ; ; 1 0 0 · 4 ) / ( ; 1 0 ↑ 7 ) ) ∈ ℝ
366	279 365 355	lttri	⊢ ( ( ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( ; ; 1 0 0 · 4 ) / ( ; 1 0 ↑ 7 ) ) ∧ ( ( ; ; 1 0 0 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ) → ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) )
367	294 364 366	mp2an	⊢ ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 )
368	226	simpli	⊢ ( ; 1 0 ↑ 7 ) ∈ ℝ
369	273 368 277	redivcli	⊢ ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) ∈ ℝ
370	55 369 355	lttri	⊢ ( ( ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) ∧ ( ( ; 2 7 · 4 ) / ( ; 1 0 ↑ 7 ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ) → ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 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 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 )
372	125 124	mpbi	⊢ ( ; 1 0 ∈ ℝ ∧ 0 < ; 1 0 )
373		ltmuldiv2	⊢ ( ( ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ∈ ℝ ∧ ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) ∈ ℝ ∧ ( ; 1 0 ∈ ℝ ∧ 0 < ; 1 0 ) ) → ( ( ; 1 0 · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) ↔ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) ) )
374	55 72 372 373	mp3an	⊢ ( ( ; 1 0 · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) ↔ ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) < ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) / ; 1 0 ) )
375	371 374	mpbir	⊢ ( ; 1 0 · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 )
376	12 55	remulcli	⊢ ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) ∈ ℝ
377	18 55	remulcli	⊢ ( ; 1 0 · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) ∈ ℝ
378	376 377 72	lttri	⊢ ( ( ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( ; 1 0 · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) ∧ ( ; 1 0 · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) ) → ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )
379	189 375 378	mp2an	⊢ ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 )
380	379	a1i	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ ( ; 1 0 ↑ ; 2 7 ) ) / ( √ ‘ ( ; 1 0 ↑ ; 2 7 ) ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )
381	47 57 73 162 380	lelttrd	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( ; 1 0 ↑ ; 2 7 ) ≤ 𝑁 ) → ( ( 7 . _ 3 _ 4 8 ) · ( ( log ‘ 𝑁 ) / ( √ ‘ 𝑁 ) ) ) < ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) )

Metamath Proof Explorer

Theorem hgt750lem

Proof