Theorem 3lexlogpow5ineq1

Description: First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024)

	Ref	Expression
Assertion	3lexlogpow5ineq1	$$⊢9<{\left(\frac{11}{7}\right)}^5$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢5=5$$
2		2p2e4	$$⊢2+2=4$$
3	2	oveq1i	$$⊢2+2+1=4+1$$
4		4p1e5	$$⊢4+1=5$$
5	3 4	eqtri	$$⊢2+2+1=5$$
6	1 5	eqtr4i	$$⊢5=2+2+1$$
7	6	oveq2i	$$⊢7^5=7^{2+2+1}$$
8		7cn	$$⊢7\in ℂ$$
9		2nn0	$$⊢2\in {\mathbb{N}}_0$$
10	9 9	nn0addcli	$$⊢2+2\in {\mathbb{N}}_0$$
11	8 10	pm3.2i	$$⊢\left(7\in ℂ\wedge 2+2\in {\mathbb{N}}_0\right)$$
12		expp1	$$⊢\left(7\in ℂ\wedge 2+2\in {\mathbb{N}}_0\right)\to 7^{2+2+1}=7^{2+2}\cdot 7$$
13	11 12	ax-mp	$$⊢7^{2+2+1}=7^{2+2}\cdot 7$$
14	8 9 9	3pm3.2i	$$⊢\left(7\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)$$
15		expadd	$$⊢\left(7\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\to 7^{2+2}=7^2{7}^2$$
16	14 15	ax-mp	$$⊢7^{2+2}=7^2{7}^2$$
17	8	sqvali	$$⊢7^2=7\cdot 7$$
18		7t7e49	$$⊢7\cdot 7=49$$
19	17 18	eqtri	$$⊢7^2=49$$
20	19 19	oveq12i	$$⊢7^2{7}^2=49\cdot 49$$
21		4nn0	$$⊢4\in {\mathbb{N}}_0$$
22		9nn0	$$⊢9\in {\mathbb{N}}_0$$
23	21 22	deccl	$$⊢49\in {\mathbb{N}}_0$$
24		eqid	$$⊢49=49$$
25		1nn0	$$⊢1\in {\mathbb{N}}_0$$
26	21 21	deccl	$$⊢44\in {\mathbb{N}}_0$$
27		eqid	$$⊢44=44$$
28		0nn0	$$⊢0\in {\mathbb{N}}_0$$
29		6nn0	$$⊢6\in {\mathbb{N}}_0$$
30	21 21	nn0addcli	$$⊢4+4\in {\mathbb{N}}_0$$
31		4t4e16	$$⊢4\cdot 4=16$$
32		1p1e2	$$⊢1+1=2$$
33		4p4e8	$$⊢4+4=8$$
34	33	oveq2i	$$⊢6+4+4=6+8$$
35		8cn	$$⊢8\in ℂ$$
36		6cn	$$⊢6\in ℂ$$
37		8p6e14	$$⊢8+6=14$$
38	35 36 37	addcomli	$$⊢6+8=14$$
39	34 38	eqtri	$$⊢6+4+4=14$$
40	25 29 30 31 32 21 39	decaddci	$$⊢4\cdot 4+4+4=24$$
41		3nn0	$$⊢3\in {\mathbb{N}}_0$$
42		9t4e36	$$⊢9\cdot 4=36$$
43		3p1e4	$$⊢3+1=4$$
44		6p4e10	$$⊢6+4=10$$
45	41 29 21 42 43 44	decaddci2	$$⊢9\cdot 4+4=40$$
46	21 22 21 21 24 27 21 28 21 40 45	decmac	$$⊢49\cdot 4+44=240$$
47		8nn0	$$⊢8\in {\mathbb{N}}_0$$
48		9cn	$$⊢9\in ℂ$$
49		4cn	$$⊢4\in ℂ$$
50	48 49 42	mulcomli	$$⊢4\cdot 9=36$$
51	41 29 47 50 43 21 38	decaddci	$$⊢4\cdot 9+8=44$$
52		9t9e81	$$⊢9\cdot 9=81$$
53	22 21 22 24 25 47 51 52	decmul1c	$$⊢49\cdot 9=441$$
54	23 21 22 24 25 26 46 53	decmul2c	$$⊢49\cdot 49=2401$$
55	20 54	eqtri	$$⊢7^2{7}^2=2401$$
56	16 55	eqtri	$$⊢7^{2+2}=2401$$
57	56	oveq1i	$$⊢7^{2+2}\cdot 7=2401\cdot 7$$
58	7 13 57	3eqtri	$$⊢7^5=2401\cdot 7$$
59		7nn0	$$⊢7\in {\mathbb{N}}_0$$
60	9 21	deccl	$$⊢24\in {\mathbb{N}}_0$$
61	60 28	deccl	$$⊢240\in {\mathbb{N}}_0$$
62		eqid	$$⊢2401=2401$$
63	25 29	deccl	$$⊢16\in {\mathbb{N}}_0$$
64	63 47	deccl	$$⊢168\in {\mathbb{N}}_0$$
65		eqid	$$⊢240=240$$
66		eqid	$$⊢24=24$$
67		2cn	$$⊢2\in ℂ$$
68		7t2e14	$$⊢7\cdot 2=14$$
69	8 67 68	mulcomli	$$⊢2\cdot 7=14$$
70		4p2e6	$$⊢4+2=6$$
71	25 21 9 69 70	decaddi	$$⊢2\cdot 7+2=16$$
72		7t4e28	$$⊢7\cdot 4=28$$
73	8 49 72	mulcomli	$$⊢4\cdot 7=28$$
74	59 9 21 66 47 9 71 73	decmul1c	$$⊢24\cdot 7=168$$
75	35	addid1i	$$⊢8+0=8$$
76	63 47 28 74 75	decaddi	$$⊢24\cdot 7+0=168$$
77		0cn	$$⊢0\in ℂ$$
78	8	mul01i	$$⊢7\cdot 0=0$$
79	28	dec0h	$$⊢0=00$$
80	79	eqcomi	$$⊢00=0$$
81	78 80	eqtr4i	$$⊢7\cdot 0=00$$
82	8 77 81	mulcomli	$$⊢0\cdot 7=00$$
83	59 60 28 65 28 28 76 82	decmul1c	$$⊢240\cdot 7=1680$$
84		00id	$$⊢0+0=0$$
85	64 28 28 83 84	decaddi	$$⊢240\cdot 7+0=1680$$
86		ax-1cn	$$⊢1\in ℂ$$
87	8	mulid1i	$$⊢7\cdot 1=7$$
88	59	dec0h	$$⊢7=07$$
89	88	eqcomi	$$⊢07=7$$
90	87 89	eqtr4i	$$⊢7\cdot 1=07$$
91	8 86 90	mulcomli	$$⊢1\cdot 7=07$$
92	59 61 25 62 59 28 85 91	decmul1c	$$⊢2401\cdot 7=16807$$
93	58 92	eqtri	$$⊢7^5=16807$$
94	93	oveq2i	$$⊢97^5=9\cdot 16807$$
95	64 28	deccl	$$⊢1680\in {\mathbb{N}}_0$$
96	95 59	deccl	$$⊢16807\in {\mathbb{N}}_0$$
97	96	nn0cni	$$⊢16807\in ℂ$$
98	48 97	mulcomi	$$⊢9\cdot 16807=16807\cdot 9$$
99		eqid	$$⊢16807=16807$$
100		eqid	$$⊢1680=1680$$
101	29	dec0h	$$⊢6=06$$
102		5nn0	$$⊢5\in {\mathbb{N}}_0$$
103	25 102	deccl	$$⊢15\in {\mathbb{N}}_0$$
104	103 25	deccl	$$⊢151\in {\mathbb{N}}_0$$
105		eqid	$$⊢168=168$$
106		eqid	$$⊢16=16$$
107	48	mulid2i	$$⊢1\cdot 9=9$$
108	36	addid2i	$$⊢0+6=6$$
109	107 108	oveq12i	$$⊢1\cdot 9+0+6=9+6$$
110		9p6e15	$$⊢9+6=15$$
111	109 110	eqtri	$$⊢1\cdot 9+0+6=15$$
112		9t6e54	$$⊢9\cdot 6=54$$
113	48 36 112	mulcomli	$$⊢6\cdot 9=54$$
114		5p1e6	$$⊢5+1=6$$
115		7p4e11	$$⊢7+4=11$$
116	8 49 115	addcomli	$$⊢4+7=11$$
117	102 21 59 113 114 25 116	decaddci	$$⊢6\cdot 9+7=61$$
118	25 29 28 59 106 88 22 25 29 111 117	decmac	$$⊢16\cdot 9+7=151$$
119		9t8e72	$$⊢9\cdot 8=72$$
120	48 35 119	mulcomli	$$⊢8\cdot 9=72$$
121	22 63 47 105 9 59 118 120	decmul1c	$$⊢168\cdot 9=1512$$
122	67	addid1i	$$⊢2+0=2$$
123	104 9 28 121 122	decaddi	$$⊢168\cdot 9+0=1512$$
124	48	mul02i	$$⊢0\cdot 9=0$$
125	124	oveq1i	$$⊢0\cdot 9+6=0+6$$
126	125 108	eqtri	$$⊢0\cdot 9+6=6$$
127	64 28 28 29 100 101 22 123 126	decma	$$⊢1680\cdot 9+6=15126$$
128		9t7e63	$$⊢9\cdot 7=63$$
129	48 8 128	mulcomli	$$⊢7\cdot 9=63$$
130	22 95 59 99 41 29 127 129	decmul1c	$$⊢16807\cdot 9=151263$$
131	104 9	deccl	$$⊢1512\in {\mathbb{N}}_0$$
132	131 29	deccl	$$⊢15126\in {\mathbb{N}}_0$$
133	63 25	deccl	$$⊢161\in {\mathbb{N}}_0$$
134	133 28	deccl	$$⊢1610\in {\mathbb{N}}_0$$
135	134 102	deccl	$$⊢16105\in {\mathbb{N}}_0$$
136		3lt10	$$⊢3<10$$
137		6lt10	$$⊢6<10$$
138		2lt10	$$⊢2<10$$
139		1lt10	$$⊢1<10$$
140		6nn	$$⊢6\in \mathbb{N}$$
141		5lt6	$$⊢5<6$$
142	25 102 140 141	declt	$$⊢15<16$$
143	103 63 25 25 139 142	decltc	$$⊢151<161$$
144	104 133 9 28 138 143	decltc	$$⊢1512<1610$$
145	131 134 29 102 137 144	decltc	$$⊢15126<16105$$
146	132 135 41 25 136 145	decltc	$$⊢151263<161051$$
147	130 146	eqbrtri	$$⊢16807\cdot 9<161051$$
148	98 147	eqbrtri	$$⊢9\cdot 16807<161051$$
149	94 148	eqbrtri	$$⊢97^5<161051$$
150	4	eqcomi	$$⊢5=4+1$$
151	150	oveq2i	$$⊢{11}^5={11}^{4+1}$$
152	25 25	deccl	$$⊢11\in {\mathbb{N}}_0$$
153	152	nn0cni	$$⊢11\in ℂ$$
154	153 21	pm3.2i	$$⊢\left(11\in ℂ\wedge 4\in {\mathbb{N}}_0\right)$$
155		expp1	$$⊢\left(11\in ℂ\wedge 4\in {\mathbb{N}}_0\right)\to {11}^{4+1}={11}^4\cdot 11$$
156	154 155	ax-mp	$$⊢{11}^{4+1}={11}^4\cdot 11$$
157	2	eqcomi	$$⊢4=2+2$$
158	157	oveq2i	$$⊢{11}^4={11}^{2+2}$$
159	153 9 9	3pm3.2i	$$⊢\left(11\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)$$
160		expadd	$$⊢\left(11\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\to {11}^{2+2}={11}^2{11}^2$$
161	159 160	ax-mp	$$⊢{11}^{2+2}={11}^2{11}^2$$
162	153	sqvali	$$⊢{11}^2=11\cdot 11$$
163		eqid	$$⊢11=11$$
164	153	mulid2i	$$⊢1\cdot 11=11$$
165	25 25 32 164	decsuc	$$⊢1\cdot 11+1=12$$
166	152 25 25 163 25 25 165 164	decmul1c	$$⊢11\cdot 11=121$$
167	162 166	eqtri	$$⊢{11}^2=121$$
168	167 167	oveq12i	$$⊢{11}^2{11}^2=121\cdot 121$$
169	25 9	deccl	$$⊢12\in {\mathbb{N}}_0$$
170	169 25	deccl	$$⊢121\in {\mathbb{N}}_0$$
171		eqid	$$⊢121=121$$
172		eqid	$$⊢12=12$$
173	170	nn0cni	$$⊢121\in ℂ$$
174	173	mulid2i	$$⊢1\cdot 121=121$$
175	25	dec0h	$$⊢1=01$$
176	67	addid2i	$$⊢0+2=2$$
177	49 86 4	addcomli	$$⊢1+4=5$$
178	28 25 9 21 175 66 176 177	decadd	$$⊢1+24=25$$
179	25 9 9 172 2	decaddi	$$⊢12+2=14$$
180		5cn	$$⊢5\in ℂ$$
181	180 86 114	addcomli	$$⊢1+5=6$$
182	169 25 9 102 174 178 179 181	decadd	$$⊢1\cdot 121+1+24=146$$
183	9	dec0h	$$⊢2=02$$
184	28 28	nn0addcli	$$⊢0+0\in {\mathbb{N}}_0$$
185		2t1e2	$$⊢2\cdot 1=2$$
186	185	oveq1i	$$⊢2\cdot 1+0=2+0$$
187	186 122	eqtri	$$⊢2\cdot 1+0=2$$
188		2t2e4	$$⊢2\cdot 2=4$$
189	21	dec0h	$$⊢4=04$$
190	189	eqcomi	$$⊢04=4$$
191	188 190	eqtr4i	$$⊢2\cdot 2=04$$
192	9 25 9 172 21 28 187 191	decmul2c	$$⊢2\cdot 12=24$$
193	84	oveq2i	$$⊢4+0+0=4+0$$
194	49	addid1i	$$⊢4+0=4$$
195	193 194	eqtri	$$⊢4+0+0=4$$
196	9 21 184 192 195	decaddi	$$⊢2\cdot 12+0+0=24$$
197	185	oveq1i	$$⊢2\cdot 1+2=2+2$$
198	197 2	eqtri	$$⊢2\cdot 1+2=4$$
199	198 190	eqtr4i	$$⊢2\cdot 1+2=04$$
200	169 25 28 9 171 183 9 21 28 196 199	decma2c	$$⊢2\cdot 121+2=244$$
201	25 9 25 9 172 172 170 21 60 182 200	decmac	$$⊢12\cdot 121+12=1464$$
202	170 169 25 171 25 169 201 174	decmul1c	$$⊢121\cdot 121=14641$$
203	168 202	eqtri	$$⊢{11}^2{11}^2=14641$$
204	161 203	eqtri	$$⊢{11}^{2+2}=14641$$
205	158 204	eqtri	$$⊢{11}^4=14641$$
206	205	oveq1i	$$⊢{11}^4\cdot 11=14641\cdot 11$$
207	156 206	eqtri	$$⊢{11}^{4+1}=14641\cdot 11$$
208	151 207	eqtri	$$⊢{11}^5=14641\cdot 11$$
209	25 21	deccl	$$⊢14\in {\mathbb{N}}_0$$
210	209 29	deccl	$$⊢146\in {\mathbb{N}}_0$$
211	210 21	deccl	$$⊢1464\in {\mathbb{N}}_0$$
212		eqid	$$⊢14641=14641$$
213		eqid	$$⊢1464=1464$$
214		eqid	$$⊢146=146$$
215	194 190	eqtr4i	$$⊢4+0=04$$
216	49 77 215	addcomli	$$⊢0+4=04$$
217		eqid	$$⊢14=14$$
218	8	addid1i	$$⊢7+0=7$$
219	218 89	eqtr4i	$$⊢7+0=07$$
220	8 77 219	addcomli	$$⊢0+7=07$$
221	28 102	nn0addcli	$$⊢0+5\in {\mathbb{N}}_0$$
222	180	addid2i	$$⊢0+5=5$$
223	222	oveq2i	$$⊢1+0+5=1+5$$
224	223 181	eqtri	$$⊢1+0+5=6$$
225	25 25 221 164 224	decaddi	$$⊢1\cdot 11+0+5=16$$
226	49	mulid1i	$$⊢4\cdot 1=4$$
227		0p1e1	$$⊢0+1=1$$
228	226 227	oveq12i	$$⊢4\cdot 1+0+1=4+1$$
229	228 4	eqtri	$$⊢4\cdot 1+0+1=5$$
230	226	oveq1i	$$⊢4\cdot 1+7=4+7$$
231	230 116	eqtri	$$⊢4\cdot 1+7=11$$
232	25 25 28 59 163 88 21 25 25 229 231	decma2c	$$⊢4\cdot 11+7=51$$
233	25 21 28 59 217 220 152 25 102 225 232	decmac	$$⊢14\cdot 11+0+7=161$$
234	36	mulid1i	$$⊢6\cdot 1=6$$
235	86	addid2i	$$⊢0+1=1$$
236	234 235	oveq12i	$$⊢6\cdot 1+0+1=6+1$$
237		6p1e7	$$⊢6+1=7$$
238	236 237	eqtri	$$⊢6\cdot 1+0+1=7$$
239		eqid	$$⊢4=4$$
240	234 239	oveq12i	$$⊢6\cdot 1+4=6+4$$
241	240 44	eqtri	$$⊢6\cdot 1+4=10$$
242	25 25 28 21 163 189 29 28 25 238 241	decma2c	$$⊢6\cdot 11+4=70$$
243	209 29 28 21 214 216 152 28 59 233 242	decmac	$$⊢146\cdot 11+0+4=1610$$
244	226 84	oveq12i	$$⊢4\cdot 1+0+0=4+0$$
245	244 194	eqtri	$$⊢4\cdot 1+0+0=4$$
246	226	oveq1i	$$⊢4\cdot 1+1=4+1$$
247	246 4	eqtri	$$⊢4\cdot 1+1=5$$
248	102	dec0h	$$⊢5=05$$
249	248	eqcomi	$$⊢05=5$$
250	247 249	eqtr4i	$$⊢4\cdot 1+1=05$$
251	25 25 28 25 163 175 21 102 28 245 250	decma2c	$$⊢4\cdot 11+1=45$$
252	210 21 28 25 213 175 152 102 21 243 251	decmac	$$⊢1464\cdot 11+1=16105$$
253	152 211 25 212 25 25 252 164	decmul1c	$$⊢14641\cdot 11=161051$$
254	208 253	eqtri	$$⊢{11}^5=161051$$
255	254	eqcomi	$$⊢161051={11}^5$$
256	149 255	breqtri	$$⊢97^5<{11}^5$$
257		7re	$$⊢7\in ℝ$$
258		5nn	$$⊢5\in \mathbb{N}$$
259	258	nnzi	$$⊢5\in \mathbb{Z}$$
260		7pos	$$⊢0<7$$
261	257 259 260	3pm3.2i	$$⊢\left(7\in ℝ\wedge 5\in \mathbb{Z}\wedge 0<7\right)$$
262		expgt0	$$⊢\left(7\in ℝ\wedge 5\in \mathbb{Z}\wedge 0<7\right)\to 0<7^5$$
263	261 262	ax-mp	$$⊢0<7^5$$
264		9re	$$⊢9\in ℝ$$
265		1nn	$$⊢1\in \mathbb{N}$$
266	25 265	decnncl	$$⊢11\in \mathbb{N}$$
267	266	nnrei	$$⊢11\in ℝ$$
268	267 102	pm3.2i	$$⊢\left(11\in ℝ\wedge 5\in {\mathbb{N}}_0\right)$$
269		reexpcl	$$⊢\left(11\in ℝ\wedge 5\in {\mathbb{N}}_0\right)\to {11}^5\in ℝ$$
270	268 269	ax-mp	$$⊢{11}^5\in ℝ$$
271	257 102	pm3.2i	$$⊢\left(7\in ℝ\wedge 5\in {\mathbb{N}}_0\right)$$
272		reexpcl	$$⊢\left(7\in ℝ\wedge 5\in {\mathbb{N}}_0\right)\to 7^5\in ℝ$$
273	271 272	ax-mp	$$⊢7^5\in ℝ$$
274	264 270 273	ltmuldivi	$$⊢0<7^5\to \left(97^5<{11}^5\leftrightarrow 9<\frac{{11}^5}{7^5}\right)$$
275	263 274	ax-mp	$$⊢97^5<{11}^5\leftrightarrow 9<\frac{{11}^5}{7^5}$$
276	256 275	mpbi	$$⊢9<\frac{{11}^5}{7^5}$$
277	153	a1i	$$⊢\top \to 11\in ℂ$$
278	8	a1i	$$⊢\top \to 7\in ℂ$$
279		0red	$$⊢\top \to 0\in ℝ$$
280	260	a1i	$$⊢\top \to 0<7$$
281	279 280	ltned	$$⊢\top \to 0\ne 7$$
282	281	necomd	$$⊢\top \to 7\ne 0$$
283	102	a1i	$$⊢\top \to 5\in {\mathbb{N}}_0$$
284	277 278 282 283	expdivd	$$⊢\top \to {\left(\frac{11}{7}\right)}^5=\frac{{11}^5}{7^5}$$
285	284	eqcomd	$$⊢\top \to \frac{{11}^5}{7^5}={\left(\frac{11}{7}\right)}^5$$
286	285	mptru	$$⊢\frac{{11}^5}{7^5}={\left(\frac{11}{7}\right)}^5$$
287	276 286	breqtri	$$⊢9<{\left(\frac{11}{7}\right)}^5$$