Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  3lexlogpow5ineq1 Structured version   Visualization version   GIF version

Theorem 3lexlogpow5ineq1 40511
Description: First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.)
Assertion
Ref Expression
3lexlogpow5ineq1 9 < ((11 / 7)↑5)

Proof of Theorem 3lexlogpow5ineq1
StepHypRef Expression
1 eqid 2736 . . . . . . . . . 10 5 = 5
2 2p2e4 12288 . . . . . . . . . . . 12 (2 + 2) = 4
32oveq1i 7367 . . . . . . . . . . 11 ((2 + 2) + 1) = (4 + 1)
4 4p1e5 12299 . . . . . . . . . . 11 (4 + 1) = 5
53, 4eqtri 2764 . . . . . . . . . 10 ((2 + 2) + 1) = 5
61, 5eqtr4i 2767 . . . . . . . . 9 5 = ((2 + 2) + 1)
76oveq2i 7368 . . . . . . . 8 (7↑5) = (7↑((2 + 2) + 1))
8 7cn 12247 . . . . . . . . . 10 7 ∈ ℂ
9 2nn0 12430 . . . . . . . . . . 11 2 ∈ ℕ0
109, 9nn0addcli 12450 . . . . . . . . . 10 (2 + 2) ∈ ℕ0
118, 10pm3.2i 471 . . . . . . . . 9 (7 ∈ ℂ ∧ (2 + 2) ∈ ℕ0)
12 expp1 13974 . . . . . . . . 9 ((7 ∈ ℂ ∧ (2 + 2) ∈ ℕ0) → (7↑((2 + 2) + 1)) = ((7↑(2 + 2)) · 7))
1311, 12ax-mp 5 . . . . . . . 8 (7↑((2 + 2) + 1)) = ((7↑(2 + 2)) · 7)
148, 9, 93pm3.2i 1339 . . . . . . . . . . 11 (7 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
15 expadd 14010 . . . . . . . . . . 11 ((7 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (7↑(2 + 2)) = ((7↑2) · (7↑2)))
1614, 15ax-mp 5 . . . . . . . . . 10 (7↑(2 + 2)) = ((7↑2) · (7↑2))
178sqvali 14084 . . . . . . . . . . . . 13 (7↑2) = (7 · 7)
18 7t7e49 12732 . . . . . . . . . . . . 13 (7 · 7) = 49
1917, 18eqtri 2764 . . . . . . . . . . . 12 (7↑2) = 49
2019, 19oveq12i 7369 . . . . . . . . . . 11 ((7↑2) · (7↑2)) = (49 · 49)
21 4nn0 12432 . . . . . . . . . . . . 13 4 ∈ ℕ0
22 9nn0 12437 . . . . . . . . . . . . 13 9 ∈ ℕ0
2321, 22deccl 12633 . . . . . . . . . . . 12 49 ∈ ℕ0
24 eqid 2736 . . . . . . . . . . . 12 49 = 49
25 1nn0 12429 . . . . . . . . . . . 12 1 ∈ ℕ0
2621, 21deccl 12633 . . . . . . . . . . . 12 44 ∈ ℕ0
27 eqid 2736 . . . . . . . . . . . . 13 44 = 44
28 0nn0 12428 . . . . . . . . . . . . 13 0 ∈ ℕ0
29 6nn0 12434 . . . . . . . . . . . . . 14 6 ∈ ℕ0
3021, 21nn0addcli 12450 . . . . . . . . . . . . . 14 (4 + 4) ∈ ℕ0
31 4t4e16 12717 . . . . . . . . . . . . . 14 (4 · 4) = 16
32 1p1e2 12278 . . . . . . . . . . . . . 14 (1 + 1) = 2
33 4p4e8 12308 . . . . . . . . . . . . . . . 16 (4 + 4) = 8
3433oveq2i 7368 . . . . . . . . . . . . . . 15 (6 + (4 + 4)) = (6 + 8)
35 8cn 12250 . . . . . . . . . . . . . . . 16 8 ∈ ℂ
36 6cn 12244 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
37 8p6e14 12702 . . . . . . . . . . . . . . . 16 (8 + 6) = 14
3835, 36, 37addcomli 11347 . . . . . . . . . . . . . . 15 (6 + 8) = 14
3934, 38eqtri 2764 . . . . . . . . . . . . . 14 (6 + (4 + 4)) = 14
4025, 29, 30, 31, 32, 21, 39decaddci 12679 . . . . . . . . . . . . 13 ((4 · 4) + (4 + 4)) = 24
41 3nn0 12431 . . . . . . . . . . . . . 14 3 ∈ ℕ0
42 9t4e36 12742 . . . . . . . . . . . . . 14 (9 · 4) = 36
43 3p1e4 12298 . . . . . . . . . . . . . 14 (3 + 1) = 4
44 6p4e10 12690 . . . . . . . . . . . . . 14 (6 + 4) = 10
4541, 29, 21, 42, 43, 44decaddci2 12680 . . . . . . . . . . . . 13 ((9 · 4) + 4) = 40
4621, 22, 21, 21, 24, 27, 21, 28, 21, 40, 45decmac 12670 . . . . . . . . . . . 12 ((49 · 4) + 44) = 240
47 8nn0 12436 . . . . . . . . . . . . 13 8 ∈ ℕ0
48 9cn 12253 . . . . . . . . . . . . . . 15 9 ∈ ℂ
49 4cn 12238 . . . . . . . . . . . . . . 15 4 ∈ ℂ
5048, 49, 42mulcomli 11164 . . . . . . . . . . . . . 14 (4 · 9) = 36
5141, 29, 47, 50, 43, 21, 38decaddci 12679 . . . . . . . . . . . . 13 ((4 · 9) + 8) = 44
52 9t9e81 12747 . . . . . . . . . . . . 13 (9 · 9) = 81
5322, 21, 22, 24, 25, 47, 51, 52decmul1c 12683 . . . . . . . . . . . 12 (49 · 9) = 441
5423, 21, 22, 24, 25, 26, 46, 53decmul2c 12684 . . . . . . . . . . 11 (49 · 49) = 2401
5520, 54eqtri 2764 . . . . . . . . . 10 ((7↑2) · (7↑2)) = 2401
5616, 55eqtri 2764 . . . . . . . . 9 (7↑(2 + 2)) = 2401
5756oveq1i 7367 . . . . . . . 8 ((7↑(2 + 2)) · 7) = (2401 · 7)
587, 13, 573eqtri 2768 . . . . . . 7 (7↑5) = (2401 · 7)
59 7nn0 12435 . . . . . . . 8 7 ∈ ℕ0
609, 21deccl 12633 . . . . . . . . 9 24 ∈ ℕ0
6160, 28deccl 12633 . . . . . . . 8 240 ∈ ℕ0
62 eqid 2736 . . . . . . . 8 2401 = 2401
6325, 29deccl 12633 . . . . . . . . . 10 16 ∈ ℕ0
6463, 47deccl 12633 . . . . . . . . 9 168 ∈ ℕ0
65 eqid 2736 . . . . . . . . . 10 240 = 240
66 eqid 2736 . . . . . . . . . . . 12 24 = 24
67 2cn 12228 . . . . . . . . . . . . . 14 2 ∈ ℂ
68 7t2e14 12727 . . . . . . . . . . . . . 14 (7 · 2) = 14
698, 67, 68mulcomli 11164 . . . . . . . . . . . . 13 (2 · 7) = 14
70 4p2e6 12306 . . . . . . . . . . . . 13 (4 + 2) = 6
7125, 21, 9, 69, 70decaddi 12678 . . . . . . . . . . . 12 ((2 · 7) + 2) = 16
72 7t4e28 12729 . . . . . . . . . . . . 13 (7 · 4) = 28
738, 49, 72mulcomli 11164 . . . . . . . . . . . 12 (4 · 7) = 28
7459, 9, 21, 66, 47, 9, 71, 73decmul1c 12683 . . . . . . . . . . 11 (24 · 7) = 168
7535addid1i 11342 . . . . . . . . . . 11 (8 + 0) = 8
7663, 47, 28, 74, 75decaddi 12678 . . . . . . . . . 10 ((24 · 7) + 0) = 168
77 0cn 11147 . . . . . . . . . . 11 0 ∈ ℂ
788mul01i 11345 . . . . . . . . . . . 12 (7 · 0) = 0
7928dec0h 12640 . . . . . . . . . . . . 13 0 = 00
8079eqcomi 2745 . . . . . . . . . . . 12 00 = 0
8178, 80eqtr4i 2767 . . . . . . . . . . 11 (7 · 0) = 00
828, 77, 81mulcomli 11164 . . . . . . . . . 10 (0 · 7) = 00
8359, 60, 28, 65, 28, 28, 76, 82decmul1c 12683 . . . . . . . . 9 (240 · 7) = 1680
84 00id 11330 . . . . . . . . 9 (0 + 0) = 0
8564, 28, 28, 83, 84decaddi 12678 . . . . . . . 8 ((240 · 7) + 0) = 1680
86 ax-1cn 11109 . . . . . . . . 9 1 ∈ ℂ
878mulid1i 11159 . . . . . . . . . 10 (7 · 1) = 7
8859dec0h 12640 . . . . . . . . . . 11 7 = 07
8988eqcomi 2745 . . . . . . . . . 10 07 = 7
9087, 89eqtr4i 2767 . . . . . . . . 9 (7 · 1) = 07
918, 86, 90mulcomli 11164 . . . . . . . 8 (1 · 7) = 07
9259, 61, 25, 62, 59, 28, 85, 91decmul1c 12683 . . . . . . 7 (2401 · 7) = 16807
9358, 92eqtri 2764 . . . . . 6 (7↑5) = 16807
9493oveq2i 7368 . . . . 5 (9 · (7↑5)) = (9 · 16807)
9564, 28deccl 12633 . . . . . . . . 9 1680 ∈ ℕ0
9695, 59deccl 12633 . . . . . . . 8 16807 ∈ ℕ0
9796nn0cni 12425 . . . . . . 7 16807 ∈ ℂ
9848, 97mulcomi 11163 . . . . . 6 (9 · 16807) = (16807 · 9)
99 eqid 2736 . . . . . . . 8 16807 = 16807
100 eqid 2736 . . . . . . . . 9 1680 = 1680
10129dec0h 12640 . . . . . . . . 9 6 = 06
102 5nn0 12433 . . . . . . . . . . . 12 5 ∈ ℕ0
10325, 102deccl 12633 . . . . . . . . . . 11 15 ∈ ℕ0
104103, 25deccl 12633 . . . . . . . . . 10 151 ∈ ℕ0
105 eqid 2736 . . . . . . . . . . 11 168 = 168
106 eqid 2736 . . . . . . . . . . . 12 16 = 16
10748mulid2i 11160 . . . . . . . . . . . . . 14 (1 · 9) = 9
10836addid2i 11343 . . . . . . . . . . . . . 14 (0 + 6) = 6
109107, 108oveq12i 7369 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 6)) = (9 + 6)
110 9p6e15 12709 . . . . . . . . . . . . 13 (9 + 6) = 15
111109, 110eqtri 2764 . . . . . . . . . . . 12 ((1 · 9) + (0 + 6)) = 15
112 9t6e54 12744 . . . . . . . . . . . . . 14 (9 · 6) = 54
11348, 36, 112mulcomli 11164 . . . . . . . . . . . . 13 (6 · 9) = 54
114 5p1e6 12300 . . . . . . . . . . . . 13 (5 + 1) = 6
115 7p4e11 12694 . . . . . . . . . . . . . 14 (7 + 4) = 11
1168, 49, 115addcomli 11347 . . . . . . . . . . . . 13 (4 + 7) = 11
117102, 21, 59, 113, 114, 25, 116decaddci 12679 . . . . . . . . . . . 12 ((6 · 9) + 7) = 61
11825, 29, 28, 59, 106, 88, 22, 25, 29, 111, 117decmac 12670 . . . . . . . . . . 11 ((16 · 9) + 7) = 151
119 9t8e72 12746 . . . . . . . . . . . 12 (9 · 8) = 72
12048, 35, 119mulcomli 11164 . . . . . . . . . . 11 (8 · 9) = 72
12122, 63, 47, 105, 9, 59, 118, 120decmul1c 12683 . . . . . . . . . 10 (168 · 9) = 1512
12267addid1i 11342 . . . . . . . . . 10 (2 + 0) = 2
123104, 9, 28, 121, 122decaddi 12678 . . . . . . . . 9 ((168 · 9) + 0) = 1512
12448mul02i 11344 . . . . . . . . . . 11 (0 · 9) = 0
125124oveq1i 7367 . . . . . . . . . 10 ((0 · 9) + 6) = (0 + 6)
126125, 108eqtri 2764 . . . . . . . . 9 ((0 · 9) + 6) = 6
12764, 28, 28, 29, 100, 101, 22, 123, 126decma 12669 . . . . . . . 8 ((1680 · 9) + 6) = 15126
128 9t7e63 12745 . . . . . . . . 9 (9 · 7) = 63
12948, 8, 128mulcomli 11164 . . . . . . . 8 (7 · 9) = 63
13022, 95, 59, 99, 41, 29, 127, 129decmul1c 12683 . . . . . . 7 (16807 · 9) = 151263
131104, 9deccl 12633 . . . . . . . . 9 1512 ∈ ℕ0
132131, 29deccl 12633 . . . . . . . 8 15126 ∈ ℕ0
13363, 25deccl 12633 . . . . . . . . . 10 161 ∈ ℕ0
134133, 28deccl 12633 . . . . . . . . 9 1610 ∈ ℕ0
135134, 102deccl 12633 . . . . . . . 8 16105 ∈ ℕ0
136 3lt10 12755 . . . . . . . 8 3 < 10
137 6lt10 12752 . . . . . . . . 9 6 < 10
138 2lt10 12756 . . . . . . . . . 10 2 < 10
139 1lt10 12757 . . . . . . . . . . 11 1 < 10
140 6nn 12242 . . . . . . . . . . . 12 6 ∈ ℕ
141 5lt6 12334 . . . . . . . . . . . 12 5 < 6
14225, 102, 140, 141declt 12646 . . . . . . . . . . 11 15 < 16
143103, 63, 25, 25, 139, 142decltc 12647 . . . . . . . . . 10 151 < 161
144104, 133, 9, 28, 138, 143decltc 12647 . . . . . . . . 9 1512 < 1610
145131, 134, 29, 102, 137, 144decltc 12647 . . . . . . . 8 15126 < 16105
146132, 135, 41, 25, 136, 145decltc 12647 . . . . . . 7 151263 < 161051
147130, 146eqbrtri 5126 . . . . . 6 (16807 · 9) < 161051
14898, 147eqbrtri 5126 . . . . 5 (9 · 16807) < 161051
14994, 148eqbrtri 5126 . . . 4 (9 · (7↑5)) < 161051
1504eqcomi 2745 . . . . . . . 8 5 = (4 + 1)
151150oveq2i 7368 . . . . . . 7 (11↑5) = (11↑(4 + 1))
15225, 25deccl 12633 . . . . . . . . . . 11 11 ∈ ℕ0
153152nn0cni 12425 . . . . . . . . . 10 11 ∈ ℂ
154153, 21pm3.2i 471 . . . . . . . . 9 (11 ∈ ℂ ∧ 4 ∈ ℕ0)
155 expp1 13974 . . . . . . . . 9 ((11 ∈ ℂ ∧ 4 ∈ ℕ0) → (11↑(4 + 1)) = ((11↑4) · 11))
156154, 155ax-mp 5 . . . . . . . 8 (11↑(4 + 1)) = ((11↑4) · 11)
1572eqcomi 2745 . . . . . . . . . . 11 4 = (2 + 2)
158157oveq2i 7368 . . . . . . . . . 10 (11↑4) = (11↑(2 + 2))
159153, 9, 93pm3.2i 1339 . . . . . . . . . . . 12 (11 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
160 expadd 14010 . . . . . . . . . . . 12 ((11 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0) → (11↑(2 + 2)) = ((11↑2) · (11↑2)))
161159, 160ax-mp 5 . . . . . . . . . . 11 (11↑(2 + 2)) = ((11↑2) · (11↑2))
162153sqvali 14084 . . . . . . . . . . . . . 14 (11↑2) = (11 · 11)
163 eqid 2736 . . . . . . . . . . . . . . 15 11 = 11
164153mulid2i 11160 . . . . . . . . . . . . . . . 16 (1 · 11) = 11
16525, 25, 32, 164decsuc 12649 . . . . . . . . . . . . . . 15 ((1 · 11) + 1) = 12
166152, 25, 25, 163, 25, 25, 165, 164decmul1c 12683 . . . . . . . . . . . . . 14 (11 · 11) = 121
167162, 166eqtri 2764 . . . . . . . . . . . . 13 (11↑2) = 121
168167, 167oveq12i 7369 . . . . . . . . . . . 12 ((11↑2) · (11↑2)) = (121 · 121)
16925, 9deccl 12633 . . . . . . . . . . . . . 14 12 ∈ ℕ0
170169, 25deccl 12633 . . . . . . . . . . . . 13 121 ∈ ℕ0
171 eqid 2736 . . . . . . . . . . . . 13 121 = 121
172 eqid 2736 . . . . . . . . . . . . . 14 12 = 12
173170nn0cni 12425 . . . . . . . . . . . . . . . 16 121 ∈ ℂ
174173mulid2i 11160 . . . . . . . . . . . . . . 15 (1 · 121) = 121
17525dec0h 12640 . . . . . . . . . . . . . . . 16 1 = 01
17667addid2i 11343 . . . . . . . . . . . . . . . 16 (0 + 2) = 2
17749, 86, 4addcomli 11347 . . . . . . . . . . . . . . . 16 (1 + 4) = 5
17828, 25, 9, 21, 175, 66, 176, 177decadd 12672 . . . . . . . . . . . . . . 15 (1 + 24) = 25
17925, 9, 9, 172, 2decaddi 12678 . . . . . . . . . . . . . . 15 (12 + 2) = 14
180 5cn 12241 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
181180, 86, 114addcomli 11347 . . . . . . . . . . . . . . 15 (1 + 5) = 6
182169, 25, 9, 102, 174, 178, 179, 181decadd 12672 . . . . . . . . . . . . . 14 ((1 · 121) + (1 + 24)) = 146
1839dec0h 12640 . . . . . . . . . . . . . . 15 2 = 02
18428, 28nn0addcli 12450 . . . . . . . . . . . . . . . 16 (0 + 0) ∈ ℕ0
185 2t1e2 12316 . . . . . . . . . . . . . . . . . . 19 (2 · 1) = 2
186185oveq1i 7367 . . . . . . . . . . . . . . . . . 18 ((2 · 1) + 0) = (2 + 0)
187186, 122eqtri 2764 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 0) = 2
188 2t2e4 12317 . . . . . . . . . . . . . . . . . 18 (2 · 2) = 4
18921dec0h 12640 . . . . . . . . . . . . . . . . . . 19 4 = 04
190189eqcomi 2745 . . . . . . . . . . . . . . . . . 18 04 = 4
191188, 190eqtr4i 2767 . . . . . . . . . . . . . . . . 17 (2 · 2) = 04
1929, 25, 9, 172, 21, 28, 187, 191decmul2c 12684 . . . . . . . . . . . . . . . 16 (2 · 12) = 24
19384oveq2i 7368 . . . . . . . . . . . . . . . . 17 (4 + (0 + 0)) = (4 + 0)
19449addid1i 11342 . . . . . . . . . . . . . . . . 17 (4 + 0) = 4
195193, 194eqtri 2764 . . . . . . . . . . . . . . . 16 (4 + (0 + 0)) = 4
1969, 21, 184, 192, 195decaddi 12678 . . . . . . . . . . . . . . 15 ((2 · 12) + (0 + 0)) = 24
197185oveq1i 7367 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 2) = (2 + 2)
198197, 2eqtri 2764 . . . . . . . . . . . . . . . 16 ((2 · 1) + 2) = 4
199198, 190eqtr4i 2767 . . . . . . . . . . . . . . 15 ((2 · 1) + 2) = 04
200169, 25, 28, 9, 171, 183, 9, 21, 28, 196, 199decma2c 12671 . . . . . . . . . . . . . 14 ((2 · 121) + 2) = 244
20125, 9, 25, 9, 172, 172, 170, 21, 60, 182, 200decmac 12670 . . . . . . . . . . . . 13 ((12 · 121) + 12) = 1464
202170, 169, 25, 171, 25, 169, 201, 174decmul1c 12683 . . . . . . . . . . . 12 (121 · 121) = 14641
203168, 202eqtri 2764 . . . . . . . . . . 11 ((11↑2) · (11↑2)) = 14641
204161, 203eqtri 2764 . . . . . . . . . 10 (11↑(2 + 2)) = 14641
205158, 204eqtri 2764 . . . . . . . . 9 (11↑4) = 14641
206205oveq1i 7367 . . . . . . . 8 ((11↑4) · 11) = (14641 · 11)
207156, 206eqtri 2764 . . . . . . 7 (11↑(4 + 1)) = (14641 · 11)
208151, 207eqtri 2764 . . . . . 6 (11↑5) = (14641 · 11)
20925, 21deccl 12633 . . . . . . . . 9 14 ∈ ℕ0
210209, 29deccl 12633 . . . . . . . 8 146 ∈ ℕ0
211210, 21deccl 12633 . . . . . . 7 1464 ∈ ℕ0
212 eqid 2736 . . . . . . 7 14641 = 14641
213 eqid 2736 . . . . . . . 8 1464 = 1464
214 eqid 2736 . . . . . . . . 9 146 = 146
215194, 190eqtr4i 2767 . . . . . . . . . 10 (4 + 0) = 04
21649, 77, 215addcomli 11347 . . . . . . . . 9 (0 + 4) = 04
217 eqid 2736 . . . . . . . . . 10 14 = 14
2188addid1i 11342 . . . . . . . . . . . 12 (7 + 0) = 7
219218, 89eqtr4i 2767 . . . . . . . . . . 11 (7 + 0) = 07
2208, 77, 219addcomli 11347 . . . . . . . . . 10 (0 + 7) = 07
22128, 102nn0addcli 12450 . . . . . . . . . . 11 (0 + 5) ∈ ℕ0
222180addid2i 11343 . . . . . . . . . . . . 13 (0 + 5) = 5
223222oveq2i 7368 . . . . . . . . . . . 12 (1 + (0 + 5)) = (1 + 5)
224223, 181eqtri 2764 . . . . . . . . . . 11 (1 + (0 + 5)) = 6
22525, 25, 221, 164, 224decaddi 12678 . . . . . . . . . 10 ((1 · 11) + (0 + 5)) = 16
22649mulid1i 11159 . . . . . . . . . . . . 13 (4 · 1) = 4
227 0p1e1 12275 . . . . . . . . . . . . 13 (0 + 1) = 1
228226, 227oveq12i 7369 . . . . . . . . . . . 12 ((4 · 1) + (0 + 1)) = (4 + 1)
229228, 4eqtri 2764 . . . . . . . . . . 11 ((4 · 1) + (0 + 1)) = 5
230226oveq1i 7367 . . . . . . . . . . . 12 ((4 · 1) + 7) = (4 + 7)
231230, 116eqtri 2764 . . . . . . . . . . 11 ((4 · 1) + 7) = 11
23225, 25, 28, 59, 163, 88, 21, 25, 25, 229, 231decma2c 12671 . . . . . . . . . 10 ((4 · 11) + 7) = 51
23325, 21, 28, 59, 217, 220, 152, 25, 102, 225, 232decmac 12670 . . . . . . . . 9 ((14 · 11) + (0 + 7)) = 161
23436mulid1i 11159 . . . . . . . . . . . 12 (6 · 1) = 6
23586addid2i 11343 . . . . . . . . . . . 12 (0 + 1) = 1
236234, 235oveq12i 7369 . . . . . . . . . . 11 ((6 · 1) + (0 + 1)) = (6 + 1)
237 6p1e7 12301 . . . . . . . . . . 11 (6 + 1) = 7
238236, 237eqtri 2764 . . . . . . . . . 10 ((6 · 1) + (0 + 1)) = 7
239 eqid 2736 . . . . . . . . . . . 12 4 = 4
240234, 239oveq12i 7369 . . . . . . . . . . 11 ((6 · 1) + 4) = (6 + 4)
241240, 44eqtri 2764 . . . . . . . . . 10 ((6 · 1) + 4) = 10
24225, 25, 28, 21, 163, 189, 29, 28, 25, 238, 241decma2c 12671 . . . . . . . . 9 ((6 · 11) + 4) = 70
243209, 29, 28, 21, 214, 216, 152, 28, 59, 233, 242decmac 12670 . . . . . . . 8 ((146 · 11) + (0 + 4)) = 1610
244226, 84oveq12i 7369 . . . . . . . . . 10 ((4 · 1) + (0 + 0)) = (4 + 0)
245244, 194eqtri 2764 . . . . . . . . 9 ((4 · 1) + (0 + 0)) = 4
246226oveq1i 7367 . . . . . . . . . . 11 ((4 · 1) + 1) = (4 + 1)
247246, 4eqtri 2764 . . . . . . . . . 10 ((4 · 1) + 1) = 5
248102dec0h 12640 . . . . . . . . . . 11 5 = 05
249248eqcomi 2745 . . . . . . . . . 10 05 = 5
250247, 249eqtr4i 2767 . . . . . . . . 9 ((4 · 1) + 1) = 05
25125, 25, 28, 25, 163, 175, 21, 102, 28, 245, 250decma2c 12671 . . . . . . . 8 ((4 · 11) + 1) = 45
252210, 21, 28, 25, 213, 175, 152, 102, 21, 243, 251decmac 12670 . . . . . . 7 ((1464 · 11) + 1) = 16105
253152, 211, 25, 212, 25, 25, 252, 164decmul1c 12683 . . . . . 6 (14641 · 11) = 161051
254208, 253eqtri 2764 . . . . 5 (11↑5) = 161051
255254eqcomi 2745 . . . 4 161051 = (11↑5)
256149, 255breqtri 5130 . . 3 (9 · (7↑5)) < (11↑5)
257 7re 12246 . . . . . 6 7 ∈ ℝ
258 5nn 12239 . . . . . . 7 5 ∈ ℕ
259258nnzi 12527 . . . . . 6 5 ∈ ℤ
260 7pos 12264 . . . . . 6 0 < 7
261257, 259, 2603pm3.2i 1339 . . . . 5 (7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7)
262 expgt0 14001 . . . . 5 ((7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) → 0 < (7↑5))
263261, 262ax-mp 5 . . . 4 0 < (7↑5)
264 9re 12252 . . . . 5 9 ∈ ℝ
265 1nn 12164 . . . . . . . . 9 1 ∈ ℕ
26625, 265decnncl 12638 . . . . . . . 8 11 ∈ ℕ
267266nnrei 12162 . . . . . . 7 11 ∈ ℝ
268267, 102pm3.2i 471 . . . . . 6 (11 ∈ ℝ ∧ 5 ∈ ℕ0)
269 reexpcl 13984 . . . . . 6 ((11 ∈ ℝ ∧ 5 ∈ ℕ0) → (11↑5) ∈ ℝ)
270268, 269ax-mp 5 . . . . 5 (11↑5) ∈ ℝ
271257, 102pm3.2i 471 . . . . . 6 (7 ∈ ℝ ∧ 5 ∈ ℕ0)
272 reexpcl 13984 . . . . . 6 ((7 ∈ ℝ ∧ 5 ∈ ℕ0) → (7↑5) ∈ ℝ)
273271, 272ax-mp 5 . . . . 5 (7↑5) ∈ ℝ
274264, 270, 273ltmuldivi 12075 . . . 4 (0 < (7↑5) → ((9 · (7↑5)) < (11↑5) ↔ 9 < ((11↑5) / (7↑5))))
275263, 274ax-mp 5 . . 3 ((9 · (7↑5)) < (11↑5) ↔ 9 < ((11↑5) / (7↑5)))
276256, 275mpbi 229 . 2 9 < ((11↑5) / (7↑5))
277153a1i 11 . . . . 5 (⊤ → 11 ∈ ℂ)
2788a1i 11 . . . . 5 (⊤ → 7 ∈ ℂ)
279 0red 11158 . . . . . . 7 (⊤ → 0 ∈ ℝ)
280260a1i 11 . . . . . . 7 (⊤ → 0 < 7)
281279, 280ltned 11291 . . . . . 6 (⊤ → 0 ≠ 7)
282281necomd 2999 . . . . 5 (⊤ → 7 ≠ 0)
283102a1i 11 . . . . 5 (⊤ → 5 ∈ ℕ0)
284277, 278, 282, 283expdivd 14065 . . . 4 (⊤ → ((11 / 7)↑5) = ((11↑5) / (7↑5)))
285284eqcomd 2742 . . 3 (⊤ → ((11↑5) / (7↑5)) = ((11 / 7)↑5))
286285mptru 1548 . 2 ((11↑5) / (7↑5)) = ((11 / 7)↑5)
287276, 286breqtri 5130 1 9 < ((11 / 7)↑5)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  w3a 1087   = wceq 1541  wtru 1542  wcel 2106   class class class wbr 5105  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189   / cdiv 11812  2c2 12208  3c3 12209  4c4 12210  5c5 12211  6c6 12212  7c7 12213  8c8 12214  9c9 12215  0cn0 12413  cz 12499  cdc 12618  cexp 13967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-rp 12916  df-seq 13907  df-exp 13968
This theorem is referenced by:  3lexlogpow5ineq4  40513
  Copyright terms: Public domain W3C validator