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