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 42055
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 2737 . . . . . . . . . 10 5 = 5
2 2p2e4 12401 . . . . . . . . . . . 12 (2 + 2) = 4
32oveq1i 7441 . . . . . . . . . . 11 ((2 + 2) + 1) = (4 + 1)
4 4p1e5 12412 . . . . . . . . . . 11 (4 + 1) = 5
53, 4eqtri 2765 . . . . . . . . . 10 ((2 + 2) + 1) = 5
61, 5eqtr4i 2768 . . . . . . . . 9 5 = ((2 + 2) + 1)
76oveq2i 7442 . . . . . . . 8 (7↑5) = (7↑((2 + 2) + 1))
8 7cn 12360 . . . . . . . . . 10 7 ∈ ℂ
9 2nn0 12543 . . . . . . . . . . 11 2 ∈ ℕ0
109, 9nn0addcli 12563 . . . . . . . . . 10 (2 + 2) ∈ ℕ0
118, 10pm3.2i 470 . . . . . . . . 9 (7 ∈ ℂ ∧ (2 + 2) ∈ ℕ0)
12 expp1 14109 . . . . . . . . 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 1340 . . . . . . . . . . 11 (7 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
15 expadd 14145 . . . . . . . . . . 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 14219 . . . . . . . . . . . . 13 (7↑2) = (7 · 7)
18 7t7e49 12847 . . . . . . . . . . . . 13 (7 · 7) = 49
1917, 18eqtri 2765 . . . . . . . . . . . 12 (7↑2) = 49
2019, 19oveq12i 7443 . . . . . . . . . . 11 ((7↑2) · (7↑2)) = (49 · 49)
21 4nn0 12545 . . . . . . . . . . . . 13 4 ∈ ℕ0
22 9nn0 12550 . . . . . . . . . . . . 13 9 ∈ ℕ0
2321, 22deccl 12748 . . . . . . . . . . . 12 49 ∈ ℕ0
24 eqid 2737 . . . . . . . . . . . 12 49 = 49
25 1nn0 12542 . . . . . . . . . . . 12 1 ∈ ℕ0
2621, 21deccl 12748 . . . . . . . . . . . 12 44 ∈ ℕ0
27 eqid 2737 . . . . . . . . . . . . 13 44 = 44
28 0nn0 12541 . . . . . . . . . . . . 13 0 ∈ ℕ0
29 6nn0 12547 . . . . . . . . . . . . . 14 6 ∈ ℕ0
3021, 21nn0addcli 12563 . . . . . . . . . . . . . 14 (4 + 4) ∈ ℕ0
31 4t4e16 12832 . . . . . . . . . . . . . 14 (4 · 4) = 16
32 1p1e2 12391 . . . . . . . . . . . . . 14 (1 + 1) = 2
33 4p4e8 12421 . . . . . . . . . . . . . . . 16 (4 + 4) = 8
3433oveq2i 7442 . . . . . . . . . . . . . . 15 (6 + (4 + 4)) = (6 + 8)
35 8cn 12363 . . . . . . . . . . . . . . . 16 8 ∈ ℂ
36 6cn 12357 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
37 8p6e14 12817 . . . . . . . . . . . . . . . 16 (8 + 6) = 14
3835, 36, 37addcomli 11453 . . . . . . . . . . . . . . 15 (6 + 8) = 14
3934, 38eqtri 2765 . . . . . . . . . . . . . 14 (6 + (4 + 4)) = 14
4025, 29, 30, 31, 32, 21, 39decaddci 12794 . . . . . . . . . . . . 13 ((4 · 4) + (4 + 4)) = 24
41 3nn0 12544 . . . . . . . . . . . . . 14 3 ∈ ℕ0
42 9t4e36 12857 . . . . . . . . . . . . . 14 (9 · 4) = 36
43 3p1e4 12411 . . . . . . . . . . . . . 14 (3 + 1) = 4
44 6p4e10 12805 . . . . . . . . . . . . . 14 (6 + 4) = 10
4541, 29, 21, 42, 43, 44decaddci2 12795 . . . . . . . . . . . . 13 ((9 · 4) + 4) = 40
4621, 22, 21, 21, 24, 27, 21, 28, 21, 40, 45decmac 12785 . . . . . . . . . . . 12 ((49 · 4) + 44) = 240
47 8nn0 12549 . . . . . . . . . . . . 13 8 ∈ ℕ0
48 9cn 12366 . . . . . . . . . . . . . . 15 9 ∈ ℂ
49 4cn 12351 . . . . . . . . . . . . . . 15 4 ∈ ℂ
5048, 49, 42mulcomli 11270 . . . . . . . . . . . . . 14 (4 · 9) = 36
5141, 29, 47, 50, 43, 21, 38decaddci 12794 . . . . . . . . . . . . 13 ((4 · 9) + 8) = 44
52 9t9e81 12862 . . . . . . . . . . . . 13 (9 · 9) = 81
5322, 21, 22, 24, 25, 47, 51, 52decmul1c 12798 . . . . . . . . . . . 12 (49 · 9) = 441
5423, 21, 22, 24, 25, 26, 46, 53decmul2c 12799 . . . . . . . . . . 11 (49 · 49) = 2401
5520, 54eqtri 2765 . . . . . . . . . 10 ((7↑2) · (7↑2)) = 2401
5616, 55eqtri 2765 . . . . . . . . 9 (7↑(2 + 2)) = 2401
5756oveq1i 7441 . . . . . . . 8 ((7↑(2 + 2)) · 7) = (2401 · 7)
587, 13, 573eqtri 2769 . . . . . . 7 (7↑5) = (2401 · 7)
59 7nn0 12548 . . . . . . . 8 7 ∈ ℕ0
609, 21deccl 12748 . . . . . . . . 9 24 ∈ ℕ0
6160, 28deccl 12748 . . . . . . . 8 240 ∈ ℕ0
62 eqid 2737 . . . . . . . 8 2401 = 2401
6325, 29deccl 12748 . . . . . . . . . 10 16 ∈ ℕ0
6463, 47deccl 12748 . . . . . . . . 9 168 ∈ ℕ0
65 eqid 2737 . . . . . . . . . 10 240 = 240
66 eqid 2737 . . . . . . . . . . . 12 24 = 24
67 2cn 12341 . . . . . . . . . . . . . 14 2 ∈ ℂ
68 7t2e14 12842 . . . . . . . . . . . . . 14 (7 · 2) = 14
698, 67, 68mulcomli 11270 . . . . . . . . . . . . 13 (2 · 7) = 14
70 4p2e6 12419 . . . . . . . . . . . . 13 (4 + 2) = 6
7125, 21, 9, 69, 70decaddi 12793 . . . . . . . . . . . 12 ((2 · 7) + 2) = 16
72 7t4e28 12844 . . . . . . . . . . . . 13 (7 · 4) = 28
738, 49, 72mulcomli 11270 . . . . . . . . . . . 12 (4 · 7) = 28
7459, 9, 21, 66, 47, 9, 71, 73decmul1c 12798 . . . . . . . . . . 11 (24 · 7) = 168
7535addridi 11448 . . . . . . . . . . 11 (8 + 0) = 8
7663, 47, 28, 74, 75decaddi 12793 . . . . . . . . . 10 ((24 · 7) + 0) = 168
77 0cn 11253 . . . . . . . . . . 11 0 ∈ ℂ
788mul01i 11451 . . . . . . . . . . . 12 (7 · 0) = 0
7928dec0h 12755 . . . . . . . . . . . . 13 0 = 00
8079eqcomi 2746 . . . . . . . . . . . 12 00 = 0
8178, 80eqtr4i 2768 . . . . . . . . . . 11 (7 · 0) = 00
828, 77, 81mulcomli 11270 . . . . . . . . . 10 (0 · 7) = 00
8359, 60, 28, 65, 28, 28, 76, 82decmul1c 12798 . . . . . . . . 9 (240 · 7) = 1680
84 00id 11436 . . . . . . . . 9 (0 + 0) = 0
8564, 28, 28, 83, 84decaddi 12793 . . . . . . . 8 ((240 · 7) + 0) = 1680
86 ax-1cn 11213 . . . . . . . . 9 1 ∈ ℂ
878mulridi 11265 . . . . . . . . . 10 (7 · 1) = 7
8859dec0h 12755 . . . . . . . . . . 11 7 = 07
8988eqcomi 2746 . . . . . . . . . 10 07 = 7
9087, 89eqtr4i 2768 . . . . . . . . 9 (7 · 1) = 07
918, 86, 90mulcomli 11270 . . . . . . . 8 (1 · 7) = 07
9259, 61, 25, 62, 59, 28, 85, 91decmul1c 12798 . . . . . . 7 (2401 · 7) = 16807
9358, 92eqtri 2765 . . . . . 6 (7↑5) = 16807
9493oveq2i 7442 . . . . 5 (9 · (7↑5)) = (9 · 16807)
9564, 28deccl 12748 . . . . . . . . 9 1680 ∈ ℕ0
9695, 59deccl 12748 . . . . . . . 8 16807 ∈ ℕ0
9796nn0cni 12538 . . . . . . 7 16807 ∈ ℂ
9848, 97mulcomi 11269 . . . . . 6 (9 · 16807) = (16807 · 9)
99 eqid 2737 . . . . . . . 8 16807 = 16807
100 eqid 2737 . . . . . . . . 9 1680 = 1680
10129dec0h 12755 . . . . . . . . 9 6 = 06
102 5nn0 12546 . . . . . . . . . . . 12 5 ∈ ℕ0
10325, 102deccl 12748 . . . . . . . . . . 11 15 ∈ ℕ0
104103, 25deccl 12748 . . . . . . . . . 10 151 ∈ ℕ0
105 eqid 2737 . . . . . . . . . . 11 168 = 168
106 eqid 2737 . . . . . . . . . . . 12 16 = 16
10748mullidi 11266 . . . . . . . . . . . . . 14 (1 · 9) = 9
10836addlidi 11449 . . . . . . . . . . . . . 14 (0 + 6) = 6
109107, 108oveq12i 7443 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 6)) = (9 + 6)
110 9p6e15 12824 . . . . . . . . . . . . 13 (9 + 6) = 15
111109, 110eqtri 2765 . . . . . . . . . . . 12 ((1 · 9) + (0 + 6)) = 15
112 9t6e54 12859 . . . . . . . . . . . . . 14 (9 · 6) = 54
11348, 36, 112mulcomli 11270 . . . . . . . . . . . . 13 (6 · 9) = 54
114 5p1e6 12413 . . . . . . . . . . . . 13 (5 + 1) = 6
115 7p4e11 12809 . . . . . . . . . . . . . 14 (7 + 4) = 11
1168, 49, 115addcomli 11453 . . . . . . . . . . . . 13 (4 + 7) = 11
117102, 21, 59, 113, 114, 25, 116decaddci 12794 . . . . . . . . . . . 12 ((6 · 9) + 7) = 61
11825, 29, 28, 59, 106, 88, 22, 25, 29, 111, 117decmac 12785 . . . . . . . . . . 11 ((16 · 9) + 7) = 151
119 9t8e72 12861 . . . . . . . . . . . 12 (9 · 8) = 72
12048, 35, 119mulcomli 11270 . . . . . . . . . . 11 (8 · 9) = 72
12122, 63, 47, 105, 9, 59, 118, 120decmul1c 12798 . . . . . . . . . 10 (168 · 9) = 1512
12267addridi 11448 . . . . . . . . . 10 (2 + 0) = 2
123104, 9, 28, 121, 122decaddi 12793 . . . . . . . . 9 ((168 · 9) + 0) = 1512
12448mul02i 11450 . . . . . . . . . . 11 (0 · 9) = 0
125124oveq1i 7441 . . . . . . . . . 10 ((0 · 9) + 6) = (0 + 6)
126125, 108eqtri 2765 . . . . . . . . 9 ((0 · 9) + 6) = 6
12764, 28, 28, 29, 100, 101, 22, 123, 126decma 12784 . . . . . . . 8 ((1680 · 9) + 6) = 15126
128 9t7e63 12860 . . . . . . . . 9 (9 · 7) = 63
12948, 8, 128mulcomli 11270 . . . . . . . 8 (7 · 9) = 63
13022, 95, 59, 99, 41, 29, 127, 129decmul1c 12798 . . . . . . 7 (16807 · 9) = 151263
131104, 9deccl 12748 . . . . . . . . 9 1512 ∈ ℕ0
132131, 29deccl 12748 . . . . . . . 8 15126 ∈ ℕ0
13363, 25deccl 12748 . . . . . . . . . 10 161 ∈ ℕ0
134133, 28deccl 12748 . . . . . . . . 9 1610 ∈ ℕ0
135134, 102deccl 12748 . . . . . . . 8 16105 ∈ ℕ0
136 3lt10 12870 . . . . . . . 8 3 < 10
137 6lt10 12867 . . . . . . . . 9 6 < 10
138 2lt10 12871 . . . . . . . . . 10 2 < 10
139 1lt10 12872 . . . . . . . . . . 11 1 < 10
140 6nn 12355 . . . . . . . . . . . 12 6 ∈ ℕ
141 5lt6 12447 . . . . . . . . . . . 12 5 < 6
14225, 102, 140, 141declt 12761 . . . . . . . . . . 11 15 < 16
143103, 63, 25, 25, 139, 142decltc 12762 . . . . . . . . . 10 151 < 161
144104, 133, 9, 28, 138, 143decltc 12762 . . . . . . . . 9 1512 < 1610
145131, 134, 29, 102, 137, 144decltc 12762 . . . . . . . 8 15126 < 16105
146132, 135, 41, 25, 136, 145decltc 12762 . . . . . . 7 151263 < 161051
147130, 146eqbrtri 5164 . . . . . 6 (16807 · 9) < 161051
14898, 147eqbrtri 5164 . . . . 5 (9 · 16807) < 161051
14994, 148eqbrtri 5164 . . . 4 (9 · (7↑5)) < 161051
1504eqcomi 2746 . . . . . . . 8 5 = (4 + 1)
151150oveq2i 7442 . . . . . . 7 (11↑5) = (11↑(4 + 1))
15225, 25deccl 12748 . . . . . . . . . . 11 11 ∈ ℕ0
153152nn0cni 12538 . . . . . . . . . 10 11 ∈ ℂ
154153, 21pm3.2i 470 . . . . . . . . 9 (11 ∈ ℂ ∧ 4 ∈ ℕ0)
155 expp1 14109 . . . . . . . . 9 ((11 ∈ ℂ ∧ 4 ∈ ℕ0) → (11↑(4 + 1)) = ((11↑4) · 11))
156154, 155ax-mp 5 . . . . . . . 8 (11↑(4 + 1)) = ((11↑4) · 11)
1572eqcomi 2746 . . . . . . . . . . 11 4 = (2 + 2)
158157oveq2i 7442 . . . . . . . . . 10 (11↑4) = (11↑(2 + 2))
159153, 9, 93pm3.2i 1340 . . . . . . . . . . . 12 (11 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
160 expadd 14145 . . . . . . . . . . . 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 14219 . . . . . . . . . . . . . 14 (11↑2) = (11 · 11)
163 eqid 2737 . . . . . . . . . . . . . . 15 11 = 11
164153mullidi 11266 . . . . . . . . . . . . . . . 16 (1 · 11) = 11
16525, 25, 32, 164decsuc 12764 . . . . . . . . . . . . . . 15 ((1 · 11) + 1) = 12
166152, 25, 25, 163, 25, 25, 165, 164decmul1c 12798 . . . . . . . . . . . . . 14 (11 · 11) = 121
167162, 166eqtri 2765 . . . . . . . . . . . . 13 (11↑2) = 121
168167, 167oveq12i 7443 . . . . . . . . . . . 12 ((11↑2) · (11↑2)) = (121 · 121)
16925, 9deccl 12748 . . . . . . . . . . . . . 14 12 ∈ ℕ0
170169, 25deccl 12748 . . . . . . . . . . . . 13 121 ∈ ℕ0
171 eqid 2737 . . . . . . . . . . . . 13 121 = 121
172 eqid 2737 . . . . . . . . . . . . . 14 12 = 12
173170nn0cni 12538 . . . . . . . . . . . . . . . 16 121 ∈ ℂ
174173mullidi 11266 . . . . . . . . . . . . . . 15 (1 · 121) = 121
17525dec0h 12755 . . . . . . . . . . . . . . . 16 1 = 01
17667addlidi 11449 . . . . . . . . . . . . . . . 16 (0 + 2) = 2
17749, 86, 4addcomli 11453 . . . . . . . . . . . . . . . 16 (1 + 4) = 5
17828, 25, 9, 21, 175, 66, 176, 177decadd 12787 . . . . . . . . . . . . . . 15 (1 + 24) = 25
17925, 9, 9, 172, 2decaddi 12793 . . . . . . . . . . . . . . 15 (12 + 2) = 14
180 5cn 12354 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
181180, 86, 114addcomli 11453 . . . . . . . . . . . . . . 15 (1 + 5) = 6
182169, 25, 9, 102, 174, 178, 179, 181decadd 12787 . . . . . . . . . . . . . 14 ((1 · 121) + (1 + 24)) = 146
1839dec0h 12755 . . . . . . . . . . . . . . 15 2 = 02
18428, 28nn0addcli 12563 . . . . . . . . . . . . . . . 16 (0 + 0) ∈ ℕ0
185 2t1e2 12429 . . . . . . . . . . . . . . . . . . 19 (2 · 1) = 2
186185oveq1i 7441 . . . . . . . . . . . . . . . . . 18 ((2 · 1) + 0) = (2 + 0)
187186, 122eqtri 2765 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 0) = 2
188 2t2e4 12430 . . . . . . . . . . . . . . . . . 18 (2 · 2) = 4
18921dec0h 12755 . . . . . . . . . . . . . . . . . . 19 4 = 04
190189eqcomi 2746 . . . . . . . . . . . . . . . . . 18 04 = 4
191188, 190eqtr4i 2768 . . . . . . . . . . . . . . . . 17 (2 · 2) = 04
1929, 25, 9, 172, 21, 28, 187, 191decmul2c 12799 . . . . . . . . . . . . . . . 16 (2 · 12) = 24
19384oveq2i 7442 . . . . . . . . . . . . . . . . 17 (4 + (0 + 0)) = (4 + 0)
19449addridi 11448 . . . . . . . . . . . . . . . . 17 (4 + 0) = 4
195193, 194eqtri 2765 . . . . . . . . . . . . . . . 16 (4 + (0 + 0)) = 4
1969, 21, 184, 192, 195decaddi 12793 . . . . . . . . . . . . . . 15 ((2 · 12) + (0 + 0)) = 24
197185oveq1i 7441 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 2) = (2 + 2)
198197, 2eqtri 2765 . . . . . . . . . . . . . . . 16 ((2 · 1) + 2) = 4
199198, 190eqtr4i 2768 . . . . . . . . . . . . . . 15 ((2 · 1) + 2) = 04
200169, 25, 28, 9, 171, 183, 9, 21, 28, 196, 199decma2c 12786 . . . . . . . . . . . . . 14 ((2 · 121) + 2) = 244
20125, 9, 25, 9, 172, 172, 170, 21, 60, 182, 200decmac 12785 . . . . . . . . . . . . 13 ((12 · 121) + 12) = 1464
202170, 169, 25, 171, 25, 169, 201, 174decmul1c 12798 . . . . . . . . . . . 12 (121 · 121) = 14641
203168, 202eqtri 2765 . . . . . . . . . . 11 ((11↑2) · (11↑2)) = 14641
204161, 203eqtri 2765 . . . . . . . . . 10 (11↑(2 + 2)) = 14641
205158, 204eqtri 2765 . . . . . . . . 9 (11↑4) = 14641
206205oveq1i 7441 . . . . . . . 8 ((11↑4) · 11) = (14641 · 11)
207156, 206eqtri 2765 . . . . . . 7 (11↑(4 + 1)) = (14641 · 11)
208151, 207eqtri 2765 . . . . . 6 (11↑5) = (14641 · 11)
20925, 21deccl 12748 . . . . . . . . 9 14 ∈ ℕ0
210209, 29deccl 12748 . . . . . . . 8 146 ∈ ℕ0
211210, 21deccl 12748 . . . . . . 7 1464 ∈ ℕ0
212 eqid 2737 . . . . . . 7 14641 = 14641
213 eqid 2737 . . . . . . . 8 1464 = 1464
214 eqid 2737 . . . . . . . . 9 146 = 146
215194, 190eqtr4i 2768 . . . . . . . . . 10 (4 + 0) = 04
21649, 77, 215addcomli 11453 . . . . . . . . 9 (0 + 4) = 04
217 eqid 2737 . . . . . . . . . 10 14 = 14
2188addridi 11448 . . . . . . . . . . . 12 (7 + 0) = 7
219218, 89eqtr4i 2768 . . . . . . . . . . 11 (7 + 0) = 07
2208, 77, 219addcomli 11453 . . . . . . . . . 10 (0 + 7) = 07
22128, 102nn0addcli 12563 . . . . . . . . . . 11 (0 + 5) ∈ ℕ0
222180addlidi 11449 . . . . . . . . . . . . 13 (0 + 5) = 5
223222oveq2i 7442 . . . . . . . . . . . 12 (1 + (0 + 5)) = (1 + 5)
224223, 181eqtri 2765 . . . . . . . . . . 11 (1 + (0 + 5)) = 6
22525, 25, 221, 164, 224decaddi 12793 . . . . . . . . . 10 ((1 · 11) + (0 + 5)) = 16
22649mulridi 11265 . . . . . . . . . . . . 13 (4 · 1) = 4
227 0p1e1 12388 . . . . . . . . . . . . 13 (0 + 1) = 1
228226, 227oveq12i 7443 . . . . . . . . . . . 12 ((4 · 1) + (0 + 1)) = (4 + 1)
229228, 4eqtri 2765 . . . . . . . . . . 11 ((4 · 1) + (0 + 1)) = 5
230226oveq1i 7441 . . . . . . . . . . . 12 ((4 · 1) + 7) = (4 + 7)
231230, 116eqtri 2765 . . . . . . . . . . 11 ((4 · 1) + 7) = 11
23225, 25, 28, 59, 163, 88, 21, 25, 25, 229, 231decma2c 12786 . . . . . . . . . 10 ((4 · 11) + 7) = 51
23325, 21, 28, 59, 217, 220, 152, 25, 102, 225, 232decmac 12785 . . . . . . . . 9 ((14 · 11) + (0 + 7)) = 161
23436mulridi 11265 . . . . . . . . . . . 12 (6 · 1) = 6
23586addlidi 11449 . . . . . . . . . . . 12 (0 + 1) = 1
236234, 235oveq12i 7443 . . . . . . . . . . 11 ((6 · 1) + (0 + 1)) = (6 + 1)
237 6p1e7 12414 . . . . . . . . . . 11 (6 + 1) = 7
238236, 237eqtri 2765 . . . . . . . . . 10 ((6 · 1) + (0 + 1)) = 7
239 eqid 2737 . . . . . . . . . . . 12 4 = 4
240234, 239oveq12i 7443 . . . . . . . . . . 11 ((6 · 1) + 4) = (6 + 4)
241240, 44eqtri 2765 . . . . . . . . . 10 ((6 · 1) + 4) = 10
24225, 25, 28, 21, 163, 189, 29, 28, 25, 238, 241decma2c 12786 . . . . . . . . 9 ((6 · 11) + 4) = 70
243209, 29, 28, 21, 214, 216, 152, 28, 59, 233, 242decmac 12785 . . . . . . . 8 ((146 · 11) + (0 + 4)) = 1610
244226, 84oveq12i 7443 . . . . . . . . . 10 ((4 · 1) + (0 + 0)) = (4 + 0)
245244, 194eqtri 2765 . . . . . . . . 9 ((4 · 1) + (0 + 0)) = 4
246226oveq1i 7441 . . . . . . . . . . 11 ((4 · 1) + 1) = (4 + 1)
247246, 4eqtri 2765 . . . . . . . . . 10 ((4 · 1) + 1) = 5
248102dec0h 12755 . . . . . . . . . . 11 5 = 05
249248eqcomi 2746 . . . . . . . . . 10 05 = 5
250247, 249eqtr4i 2768 . . . . . . . . 9 ((4 · 1) + 1) = 05
25125, 25, 28, 25, 163, 175, 21, 102, 28, 245, 250decma2c 12786 . . . . . . . 8 ((4 · 11) + 1) = 45
252210, 21, 28, 25, 213, 175, 152, 102, 21, 243, 251decmac 12785 . . . . . . 7 ((1464 · 11) + 1) = 16105
253152, 211, 25, 212, 25, 25, 252, 164decmul1c 12798 . . . . . 6 (14641 · 11) = 161051
254208, 253eqtri 2765 . . . . 5 (11↑5) = 161051
255254eqcomi 2746 . . . 4 161051 = (11↑5)
256149, 255breqtri 5168 . . 3 (9 · (7↑5)) < (11↑5)
257 7re 12359 . . . . . 6 7 ∈ ℝ
258 5nn 12352 . . . . . . 7 5 ∈ ℕ
259258nnzi 12641 . . . . . 6 5 ∈ ℤ
260 7pos 12377 . . . . . 6 0 < 7
261257, 259, 2603pm3.2i 1340 . . . . 5 (7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7)
262 expgt0 14136 . . . . 5 ((7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) → 0 < (7↑5))
263261, 262ax-mp 5 . . . 4 0 < (7↑5)
264 9re 12365 . . . . 5 9 ∈ ℝ
265 1nn 12277 . . . . . . . . 9 1 ∈ ℕ
26625, 265decnncl 12753 . . . . . . . 8 11 ∈ ℕ
267266nnrei 12275 . . . . . . 7 11 ∈ ℝ
268267, 102pm3.2i 470 . . . . . 6 (11 ∈ ℝ ∧ 5 ∈ ℕ0)
269 reexpcl 14119 . . . . . 6 ((11 ∈ ℝ ∧ 5 ∈ ℕ0) → (11↑5) ∈ ℝ)
270268, 269ax-mp 5 . . . . 5 (11↑5) ∈ ℝ
271257, 102pm3.2i 470 . . . . . 6 (7 ∈ ℝ ∧ 5 ∈ ℕ0)
272 reexpcl 14119 . . . . . 6 ((7 ∈ ℝ ∧ 5 ∈ ℕ0) → (7↑5) ∈ ℝ)
273271, 272ax-mp 5 . . . . 5 (7↑5) ∈ ℝ
274264, 270, 273ltmuldivi 12188 . . . 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 230 . 2 9 < ((11↑5) / (7↑5))
277153a1i 11 . . . . 5 (⊤ → 11 ∈ ℂ)
2788a1i 11 . . . . 5 (⊤ → 7 ∈ ℂ)
279 0red 11264 . . . . . . 7 (⊤ → 0 ∈ ℝ)
280260a1i 11 . . . . . . 7 (⊤ → 0 < 7)
281279, 280ltned 11397 . . . . . 6 (⊤ → 0 ≠ 7)
282281necomd 2996 . . . . 5 (⊤ → 7 ≠ 0)
283102a1i 11 . . . . 5 (⊤ → 5 ∈ ℕ0)
284277, 278, 282, 283expdivd 14200 . . . 4 (⊤ → ((11 / 7)↑5) = ((11↑5) / (7↑5)))
285284eqcomd 2743 . . 3 (⊤ → ((11↑5) / (7↑5)) = ((11 / 7)↑5))
286285mptru 1547 . 2 ((11↑5) / (7↑5)) = ((11 / 7)↑5)
287276, 286breqtri 5168 1 9 < ((11 / 7)↑5)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  w3a 1087   = wceq 1540  wtru 1541  wcel 2108   class class class wbr 5143  (class class class)co 7431  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295   / cdiv 11920  2c2 12321  3c3 12322  4c4 12323  5c5 12324  6c6 12325  7c7 12326  8c8 12327  9c9 12328  0cn0 12526  cz 12613  cdc 12733  cexp 14102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-seq 14043  df-exp 14103
This theorem is referenced by:  3lexlogpow5ineq4  42057
  Copyright terms: Public domain W3C validator