Theorem 3lexlogpow5ineq1

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

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