Metamath Proof Explorer

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 addridi 
 |-  ( 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 mulridi 
 |-  ( 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 mullidi 
 |-  ( 1 x. 9 ) = 9
108 36 addlidi 
 |-  ( 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 addridi 
 |-  ( 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 mullidi 
 |-  ( 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 mullidi 
 |-  ( 1 x. ; ; 1 2 1 ) = ; ; 1 2 1
175 25 dec0h 
 |-  1 = ; 0 1
176 67 addlidi 
 |-  ( 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 addridi 
 |-  ( 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 addridi 
 |-  ( 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 addlidi 
 |-  ( 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 mulridi 
 |-  ( 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 mulridi 
 |-  ( 6 x. 1 ) = 6
235 86 addlidi 
 |-  ( 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 )