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 42035
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 2734 . . . . . . . . . 10 5 = 5
2 2p2e4 12398 . . . . . . . . . . . 12 (2 + 2) = 4
32oveq1i 7440 . . . . . . . . . . 11 ((2 + 2) + 1) = (4 + 1)
4 4p1e5 12409 . . . . . . . . . . 11 (4 + 1) = 5
53, 4eqtri 2762 . . . . . . . . . 10 ((2 + 2) + 1) = 5
61, 5eqtr4i 2765 . . . . . . . . 9 5 = ((2 + 2) + 1)
76oveq2i 7441 . . . . . . . 8 (7↑5) = (7↑((2 + 2) + 1))
8 7cn 12357 . . . . . . . . . 10 7 ∈ ℂ
9 2nn0 12540 . . . . . . . . . . 11 2 ∈ ℕ0
109, 9nn0addcli 12560 . . . . . . . . . 10 (2 + 2) ∈ ℕ0
118, 10pm3.2i 470 . . . . . . . . 9 (7 ∈ ℂ ∧ (2 + 2) ∈ ℕ0)
12 expp1 14105 . . . . . . . . 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 1338 . . . . . . . . . . 11 (7 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
15 expadd 14141 . . . . . . . . . . 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 14215 . . . . . . . . . . . . 13 (7↑2) = (7 · 7)
18 7t7e49 12844 . . . . . . . . . . . . 13 (7 · 7) = 49
1917, 18eqtri 2762 . . . . . . . . . . . 12 (7↑2) = 49
2019, 19oveq12i 7442 . . . . . . . . . . 11 ((7↑2) · (7↑2)) = (49 · 49)
21 4nn0 12542 . . . . . . . . . . . . 13 4 ∈ ℕ0
22 9nn0 12547 . . . . . . . . . . . . 13 9 ∈ ℕ0
2321, 22deccl 12745 . . . . . . . . . . . 12 49 ∈ ℕ0
24 eqid 2734 . . . . . . . . . . . 12 49 = 49
25 1nn0 12539 . . . . . . . . . . . 12 1 ∈ ℕ0
2621, 21deccl 12745 . . . . . . . . . . . 12 44 ∈ ℕ0
27 eqid 2734 . . . . . . . . . . . . 13 44 = 44
28 0nn0 12538 . . . . . . . . . . . . 13 0 ∈ ℕ0
29 6nn0 12544 . . . . . . . . . . . . . 14 6 ∈ ℕ0
3021, 21nn0addcli 12560 . . . . . . . . . . . . . 14 (4 + 4) ∈ ℕ0
31 4t4e16 12829 . . . . . . . . . . . . . 14 (4 · 4) = 16
32 1p1e2 12388 . . . . . . . . . . . . . 14 (1 + 1) = 2
33 4p4e8 12418 . . . . . . . . . . . . . . . 16 (4 + 4) = 8
3433oveq2i 7441 . . . . . . . . . . . . . . 15 (6 + (4 + 4)) = (6 + 8)
35 8cn 12360 . . . . . . . . . . . . . . . 16 8 ∈ ℂ
36 6cn 12354 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
37 8p6e14 12814 . . . . . . . . . . . . . . . 16 (8 + 6) = 14
3835, 36, 37addcomli 11450 . . . . . . . . . . . . . . 15 (6 + 8) = 14
3934, 38eqtri 2762 . . . . . . . . . . . . . 14 (6 + (4 + 4)) = 14
4025, 29, 30, 31, 32, 21, 39decaddci 12791 . . . . . . . . . . . . 13 ((4 · 4) + (4 + 4)) = 24
41 3nn0 12541 . . . . . . . . . . . . . 14 3 ∈ ℕ0
42 9t4e36 12854 . . . . . . . . . . . . . 14 (9 · 4) = 36
43 3p1e4 12408 . . . . . . . . . . . . . 14 (3 + 1) = 4
44 6p4e10 12802 . . . . . . . . . . . . . 14 (6 + 4) = 10
4541, 29, 21, 42, 43, 44decaddci2 12792 . . . . . . . . . . . . 13 ((9 · 4) + 4) = 40
4621, 22, 21, 21, 24, 27, 21, 28, 21, 40, 45decmac 12782 . . . . . . . . . . . 12 ((49 · 4) + 44) = 240
47 8nn0 12546 . . . . . . . . . . . . 13 8 ∈ ℕ0
48 9cn 12363 . . . . . . . . . . . . . . 15 9 ∈ ℂ
49 4cn 12348 . . . . . . . . . . . . . . 15 4 ∈ ℂ
5048, 49, 42mulcomli 11267 . . . . . . . . . . . . . 14 (4 · 9) = 36
5141, 29, 47, 50, 43, 21, 38decaddci 12791 . . . . . . . . . . . . 13 ((4 · 9) + 8) = 44
52 9t9e81 12859 . . . . . . . . . . . . 13 (9 · 9) = 81
5322, 21, 22, 24, 25, 47, 51, 52decmul1c 12795 . . . . . . . . . . . 12 (49 · 9) = 441
5423, 21, 22, 24, 25, 26, 46, 53decmul2c 12796 . . . . . . . . . . 11 (49 · 49) = 2401
5520, 54eqtri 2762 . . . . . . . . . 10 ((7↑2) · (7↑2)) = 2401
5616, 55eqtri 2762 . . . . . . . . 9 (7↑(2 + 2)) = 2401
5756oveq1i 7440 . . . . . . . 8 ((7↑(2 + 2)) · 7) = (2401 · 7)
587, 13, 573eqtri 2766 . . . . . . 7 (7↑5) = (2401 · 7)
59 7nn0 12545 . . . . . . . 8 7 ∈ ℕ0
609, 21deccl 12745 . . . . . . . . 9 24 ∈ ℕ0
6160, 28deccl 12745 . . . . . . . 8 240 ∈ ℕ0
62 eqid 2734 . . . . . . . 8 2401 = 2401
6325, 29deccl 12745 . . . . . . . . . 10 16 ∈ ℕ0
6463, 47deccl 12745 . . . . . . . . 9 168 ∈ ℕ0
65 eqid 2734 . . . . . . . . . 10 240 = 240
66 eqid 2734 . . . . . . . . . . . 12 24 = 24
67 2cn 12338 . . . . . . . . . . . . . 14 2 ∈ ℂ
68 7t2e14 12839 . . . . . . . . . . . . . 14 (7 · 2) = 14
698, 67, 68mulcomli 11267 . . . . . . . . . . . . 13 (2 · 7) = 14
70 4p2e6 12416 . . . . . . . . . . . . 13 (4 + 2) = 6
7125, 21, 9, 69, 70decaddi 12790 . . . . . . . . . . . 12 ((2 · 7) + 2) = 16
72 7t4e28 12841 . . . . . . . . . . . . 13 (7 · 4) = 28
738, 49, 72mulcomli 11267 . . . . . . . . . . . 12 (4 · 7) = 28
7459, 9, 21, 66, 47, 9, 71, 73decmul1c 12795 . . . . . . . . . . 11 (24 · 7) = 168
7535addridi 11445 . . . . . . . . . . 11 (8 + 0) = 8
7663, 47, 28, 74, 75decaddi 12790 . . . . . . . . . 10 ((24 · 7) + 0) = 168
77 0cn 11250 . . . . . . . . . . 11 0 ∈ ℂ
788mul01i 11448 . . . . . . . . . . . 12 (7 · 0) = 0
7928dec0h 12752 . . . . . . . . . . . . 13 0 = 00
8079eqcomi 2743 . . . . . . . . . . . 12 00 = 0
8178, 80eqtr4i 2765 . . . . . . . . . . 11 (7 · 0) = 00
828, 77, 81mulcomli 11267 . . . . . . . . . 10 (0 · 7) = 00
8359, 60, 28, 65, 28, 28, 76, 82decmul1c 12795 . . . . . . . . 9 (240 · 7) = 1680
84 00id 11433 . . . . . . . . 9 (0 + 0) = 0
8564, 28, 28, 83, 84decaddi 12790 . . . . . . . 8 ((240 · 7) + 0) = 1680
86 ax-1cn 11210 . . . . . . . . 9 1 ∈ ℂ
878mulridi 11262 . . . . . . . . . 10 (7 · 1) = 7
8859dec0h 12752 . . . . . . . . . . 11 7 = 07
8988eqcomi 2743 . . . . . . . . . 10 07 = 7
9087, 89eqtr4i 2765 . . . . . . . . 9 (7 · 1) = 07
918, 86, 90mulcomli 11267 . . . . . . . 8 (1 · 7) = 07
9259, 61, 25, 62, 59, 28, 85, 91decmul1c 12795 . . . . . . 7 (2401 · 7) = 16807
9358, 92eqtri 2762 . . . . . 6 (7↑5) = 16807
9493oveq2i 7441 . . . . 5 (9 · (7↑5)) = (9 · 16807)
9564, 28deccl 12745 . . . . . . . . 9 1680 ∈ ℕ0
9695, 59deccl 12745 . . . . . . . 8 16807 ∈ ℕ0
9796nn0cni 12535 . . . . . . 7 16807 ∈ ℂ
9848, 97mulcomi 11266 . . . . . 6 (9 · 16807) = (16807 · 9)
99 eqid 2734 . . . . . . . 8 16807 = 16807
100 eqid 2734 . . . . . . . . 9 1680 = 1680
10129dec0h 12752 . . . . . . . . 9 6 = 06
102 5nn0 12543 . . . . . . . . . . . 12 5 ∈ ℕ0
10325, 102deccl 12745 . . . . . . . . . . 11 15 ∈ ℕ0
104103, 25deccl 12745 . . . . . . . . . 10 151 ∈ ℕ0
105 eqid 2734 . . . . . . . . . . 11 168 = 168
106 eqid 2734 . . . . . . . . . . . 12 16 = 16
10748mullidi 11263 . . . . . . . . . . . . . 14 (1 · 9) = 9
10836addlidi 11446 . . . . . . . . . . . . . 14 (0 + 6) = 6
109107, 108oveq12i 7442 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 6)) = (9 + 6)
110 9p6e15 12821 . . . . . . . . . . . . 13 (9 + 6) = 15
111109, 110eqtri 2762 . . . . . . . . . . . 12 ((1 · 9) + (0 + 6)) = 15
112 9t6e54 12856 . . . . . . . . . . . . . 14 (9 · 6) = 54
11348, 36, 112mulcomli 11267 . . . . . . . . . . . . 13 (6 · 9) = 54
114 5p1e6 12410 . . . . . . . . . . . . 13 (5 + 1) = 6
115 7p4e11 12806 . . . . . . . . . . . . . 14 (7 + 4) = 11
1168, 49, 115addcomli 11450 . . . . . . . . . . . . 13 (4 + 7) = 11
117102, 21, 59, 113, 114, 25, 116decaddci 12791 . . . . . . . . . . . 12 ((6 · 9) + 7) = 61
11825, 29, 28, 59, 106, 88, 22, 25, 29, 111, 117decmac 12782 . . . . . . . . . . 11 ((16 · 9) + 7) = 151
119 9t8e72 12858 . . . . . . . . . . . 12 (9 · 8) = 72
12048, 35, 119mulcomli 11267 . . . . . . . . . . 11 (8 · 9) = 72
12122, 63, 47, 105, 9, 59, 118, 120decmul1c 12795 . . . . . . . . . 10 (168 · 9) = 1512
12267addridi 11445 . . . . . . . . . 10 (2 + 0) = 2
123104, 9, 28, 121, 122decaddi 12790 . . . . . . . . 9 ((168 · 9) + 0) = 1512
12448mul02i 11447 . . . . . . . . . . 11 (0 · 9) = 0
125124oveq1i 7440 . . . . . . . . . 10 ((0 · 9) + 6) = (0 + 6)
126125, 108eqtri 2762 . . . . . . . . 9 ((0 · 9) + 6) = 6
12764, 28, 28, 29, 100, 101, 22, 123, 126decma 12781 . . . . . . . 8 ((1680 · 9) + 6) = 15126
128 9t7e63 12857 . . . . . . . . 9 (9 · 7) = 63
12948, 8, 128mulcomli 11267 . . . . . . . 8 (7 · 9) = 63
13022, 95, 59, 99, 41, 29, 127, 129decmul1c 12795 . . . . . . 7 (16807 · 9) = 151263
131104, 9deccl 12745 . . . . . . . . 9 1512 ∈ ℕ0
132131, 29deccl 12745 . . . . . . . 8 15126 ∈ ℕ0
13363, 25deccl 12745 . . . . . . . . . 10 161 ∈ ℕ0
134133, 28deccl 12745 . . . . . . . . 9 1610 ∈ ℕ0
135134, 102deccl 12745 . . . . . . . 8 16105 ∈ ℕ0
136 3lt10 12867 . . . . . . . 8 3 < 10
137 6lt10 12864 . . . . . . . . 9 6 < 10
138 2lt10 12868 . . . . . . . . . 10 2 < 10
139 1lt10 12869 . . . . . . . . . . 11 1 < 10
140 6nn 12352 . . . . . . . . . . . 12 6 ∈ ℕ
141 5lt6 12444 . . . . . . . . . . . 12 5 < 6
14225, 102, 140, 141declt 12758 . . . . . . . . . . 11 15 < 16
143103, 63, 25, 25, 139, 142decltc 12759 . . . . . . . . . 10 151 < 161
144104, 133, 9, 28, 138, 143decltc 12759 . . . . . . . . 9 1512 < 1610
145131, 134, 29, 102, 137, 144decltc 12759 . . . . . . . 8 15126 < 16105
146132, 135, 41, 25, 136, 145decltc 12759 . . . . . . 7 151263 < 161051
147130, 146eqbrtri 5168 . . . . . 6 (16807 · 9) < 161051
14898, 147eqbrtri 5168 . . . . 5 (9 · 16807) < 161051
14994, 148eqbrtri 5168 . . . 4 (9 · (7↑5)) < 161051
1504eqcomi 2743 . . . . . . . 8 5 = (4 + 1)
151150oveq2i 7441 . . . . . . 7 (11↑5) = (11↑(4 + 1))
15225, 25deccl 12745 . . . . . . . . . . 11 11 ∈ ℕ0
153152nn0cni 12535 . . . . . . . . . 10 11 ∈ ℂ
154153, 21pm3.2i 470 . . . . . . . . 9 (11 ∈ ℂ ∧ 4 ∈ ℕ0)
155 expp1 14105 . . . . . . . . 9 ((11 ∈ ℂ ∧ 4 ∈ ℕ0) → (11↑(4 + 1)) = ((11↑4) · 11))
156154, 155ax-mp 5 . . . . . . . 8 (11↑(4 + 1)) = ((11↑4) · 11)
1572eqcomi 2743 . . . . . . . . . . 11 4 = (2 + 2)
158157oveq2i 7441 . . . . . . . . . 10 (11↑4) = (11↑(2 + 2))
159153, 9, 93pm3.2i 1338 . . . . . . . . . . . 12 (11 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
160 expadd 14141 . . . . . . . . . . . 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 14215 . . . . . . . . . . . . . 14 (11↑2) = (11 · 11)
163 eqid 2734 . . . . . . . . . . . . . . 15 11 = 11
164153mullidi 11263 . . . . . . . . . . . . . . . 16 (1 · 11) = 11
16525, 25, 32, 164decsuc 12761 . . . . . . . . . . . . . . 15 ((1 · 11) + 1) = 12
166152, 25, 25, 163, 25, 25, 165, 164decmul1c 12795 . . . . . . . . . . . . . 14 (11 · 11) = 121
167162, 166eqtri 2762 . . . . . . . . . . . . 13 (11↑2) = 121
168167, 167oveq12i 7442 . . . . . . . . . . . 12 ((11↑2) · (11↑2)) = (121 · 121)
16925, 9deccl 12745 . . . . . . . . . . . . . 14 12 ∈ ℕ0
170169, 25deccl 12745 . . . . . . . . . . . . 13 121 ∈ ℕ0
171 eqid 2734 . . . . . . . . . . . . 13 121 = 121
172 eqid 2734 . . . . . . . . . . . . . 14 12 = 12
173170nn0cni 12535 . . . . . . . . . . . . . . . 16 121 ∈ ℂ
174173mullidi 11263 . . . . . . . . . . . . . . 15 (1 · 121) = 121
17525dec0h 12752 . . . . . . . . . . . . . . . 16 1 = 01
17667addlidi 11446 . . . . . . . . . . . . . . . 16 (0 + 2) = 2
17749, 86, 4addcomli 11450 . . . . . . . . . . . . . . . 16 (1 + 4) = 5
17828, 25, 9, 21, 175, 66, 176, 177decadd 12784 . . . . . . . . . . . . . . 15 (1 + 24) = 25
17925, 9, 9, 172, 2decaddi 12790 . . . . . . . . . . . . . . 15 (12 + 2) = 14
180 5cn 12351 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
181180, 86, 114addcomli 11450 . . . . . . . . . . . . . . 15 (1 + 5) = 6
182169, 25, 9, 102, 174, 178, 179, 181decadd 12784 . . . . . . . . . . . . . 14 ((1 · 121) + (1 + 24)) = 146
1839dec0h 12752 . . . . . . . . . . . . . . 15 2 = 02
18428, 28nn0addcli 12560 . . . . . . . . . . . . . . . 16 (0 + 0) ∈ ℕ0
185 2t1e2 12426 . . . . . . . . . . . . . . . . . . 19 (2 · 1) = 2
186185oveq1i 7440 . . . . . . . . . . . . . . . . . 18 ((2 · 1) + 0) = (2 + 0)
187186, 122eqtri 2762 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 0) = 2
188 2t2e4 12427 . . . . . . . . . . . . . . . . . 18 (2 · 2) = 4
18921dec0h 12752 . . . . . . . . . . . . . . . . . . 19 4 = 04
190189eqcomi 2743 . . . . . . . . . . . . . . . . . 18 04 = 4
191188, 190eqtr4i 2765 . . . . . . . . . . . . . . . . 17 (2 · 2) = 04
1929, 25, 9, 172, 21, 28, 187, 191decmul2c 12796 . . . . . . . . . . . . . . . 16 (2 · 12) = 24
19384oveq2i 7441 . . . . . . . . . . . . . . . . 17 (4 + (0 + 0)) = (4 + 0)
19449addridi 11445 . . . . . . . . . . . . . . . . 17 (4 + 0) = 4
195193, 194eqtri 2762 . . . . . . . . . . . . . . . 16 (4 + (0 + 0)) = 4
1969, 21, 184, 192, 195decaddi 12790 . . . . . . . . . . . . . . 15 ((2 · 12) + (0 + 0)) = 24
197185oveq1i 7440 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 2) = (2 + 2)
198197, 2eqtri 2762 . . . . . . . . . . . . . . . 16 ((2 · 1) + 2) = 4
199198, 190eqtr4i 2765 . . . . . . . . . . . . . . 15 ((2 · 1) + 2) = 04
200169, 25, 28, 9, 171, 183, 9, 21, 28, 196, 199decma2c 12783 . . . . . . . . . . . . . 14 ((2 · 121) + 2) = 244
20125, 9, 25, 9, 172, 172, 170, 21, 60, 182, 200decmac 12782 . . . . . . . . . . . . 13 ((12 · 121) + 12) = 1464
202170, 169, 25, 171, 25, 169, 201, 174decmul1c 12795 . . . . . . . . . . . 12 (121 · 121) = 14641
203168, 202eqtri 2762 . . . . . . . . . . 11 ((11↑2) · (11↑2)) = 14641
204161, 203eqtri 2762 . . . . . . . . . 10 (11↑(2 + 2)) = 14641
205158, 204eqtri 2762 . . . . . . . . 9 (11↑4) = 14641
206205oveq1i 7440 . . . . . . . 8 ((11↑4) · 11) = (14641 · 11)
207156, 206eqtri 2762 . . . . . . 7 (11↑(4 + 1)) = (14641 · 11)
208151, 207eqtri 2762 . . . . . 6 (11↑5) = (14641 · 11)
20925, 21deccl 12745 . . . . . . . . 9 14 ∈ ℕ0
210209, 29deccl 12745 . . . . . . . 8 146 ∈ ℕ0
211210, 21deccl 12745 . . . . . . 7 1464 ∈ ℕ0
212 eqid 2734 . . . . . . 7 14641 = 14641
213 eqid 2734 . . . . . . . 8 1464 = 1464
214 eqid 2734 . . . . . . . . 9 146 = 146
215194, 190eqtr4i 2765 . . . . . . . . . 10 (4 + 0) = 04
21649, 77, 215addcomli 11450 . . . . . . . . 9 (0 + 4) = 04
217 eqid 2734 . . . . . . . . . 10 14 = 14
2188addridi 11445 . . . . . . . . . . . 12 (7 + 0) = 7
219218, 89eqtr4i 2765 . . . . . . . . . . 11 (7 + 0) = 07
2208, 77, 219addcomli 11450 . . . . . . . . . 10 (0 + 7) = 07
22128, 102nn0addcli 12560 . . . . . . . . . . 11 (0 + 5) ∈ ℕ0
222180addlidi 11446 . . . . . . . . . . . . 13 (0 + 5) = 5
223222oveq2i 7441 . . . . . . . . . . . 12 (1 + (0 + 5)) = (1 + 5)
224223, 181eqtri 2762 . . . . . . . . . . 11 (1 + (0 + 5)) = 6
22525, 25, 221, 164, 224decaddi 12790 . . . . . . . . . 10 ((1 · 11) + (0 + 5)) = 16
22649mulridi 11262 . . . . . . . . . . . . 13 (4 · 1) = 4
227 0p1e1 12385 . . . . . . . . . . . . 13 (0 + 1) = 1
228226, 227oveq12i 7442 . . . . . . . . . . . 12 ((4 · 1) + (0 + 1)) = (4 + 1)
229228, 4eqtri 2762 . . . . . . . . . . 11 ((4 · 1) + (0 + 1)) = 5
230226oveq1i 7440 . . . . . . . . . . . 12 ((4 · 1) + 7) = (4 + 7)
231230, 116eqtri 2762 . . . . . . . . . . 11 ((4 · 1) + 7) = 11
23225, 25, 28, 59, 163, 88, 21, 25, 25, 229, 231decma2c 12783 . . . . . . . . . 10 ((4 · 11) + 7) = 51
23325, 21, 28, 59, 217, 220, 152, 25, 102, 225, 232decmac 12782 . . . . . . . . 9 ((14 · 11) + (0 + 7)) = 161
23436mulridi 11262 . . . . . . . . . . . 12 (6 · 1) = 6
23586addlidi 11446 . . . . . . . . . . . 12 (0 + 1) = 1
236234, 235oveq12i 7442 . . . . . . . . . . 11 ((6 · 1) + (0 + 1)) = (6 + 1)
237 6p1e7 12411 . . . . . . . . . . 11 (6 + 1) = 7
238236, 237eqtri 2762 . . . . . . . . . 10 ((6 · 1) + (0 + 1)) = 7
239 eqid 2734 . . . . . . . . . . . 12 4 = 4
240234, 239oveq12i 7442 . . . . . . . . . . 11 ((6 · 1) + 4) = (6 + 4)
241240, 44eqtri 2762 . . . . . . . . . 10 ((6 · 1) + 4) = 10
24225, 25, 28, 21, 163, 189, 29, 28, 25, 238, 241decma2c 12783 . . . . . . . . 9 ((6 · 11) + 4) = 70
243209, 29, 28, 21, 214, 216, 152, 28, 59, 233, 242decmac 12782 . . . . . . . 8 ((146 · 11) + (0 + 4)) = 1610
244226, 84oveq12i 7442 . . . . . . . . . 10 ((4 · 1) + (0 + 0)) = (4 + 0)
245244, 194eqtri 2762 . . . . . . . . 9 ((4 · 1) + (0 + 0)) = 4
246226oveq1i 7440 . . . . . . . . . . 11 ((4 · 1) + 1) = (4 + 1)
247246, 4eqtri 2762 . . . . . . . . . 10 ((4 · 1) + 1) = 5
248102dec0h 12752 . . . . . . . . . . 11 5 = 05
249248eqcomi 2743 . . . . . . . . . 10 05 = 5
250247, 249eqtr4i 2765 . . . . . . . . 9 ((4 · 1) + 1) = 05
25125, 25, 28, 25, 163, 175, 21, 102, 28, 245, 250decma2c 12783 . . . . . . . 8 ((4 · 11) + 1) = 45
252210, 21, 28, 25, 213, 175, 152, 102, 21, 243, 251decmac 12782 . . . . . . 7 ((1464 · 11) + 1) = 16105
253152, 211, 25, 212, 25, 25, 252, 164decmul1c 12795 . . . . . 6 (14641 · 11) = 161051
254208, 253eqtri 2762 . . . . 5 (11↑5) = 161051
255254eqcomi 2743 . . . 4 161051 = (11↑5)
256149, 255breqtri 5172 . . 3 (9 · (7↑5)) < (11↑5)
257 7re 12356 . . . . . 6 7 ∈ ℝ
258 5nn 12349 . . . . . . 7 5 ∈ ℕ
259258nnzi 12638 . . . . . 6 5 ∈ ℤ
260 7pos 12374 . . . . . 6 0 < 7
261257, 259, 2603pm3.2i 1338 . . . . 5 (7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7)
262 expgt0 14132 . . . . 5 ((7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) → 0 < (7↑5))
263261, 262ax-mp 5 . . . 4 0 < (7↑5)
264 9re 12362 . . . . 5 9 ∈ ℝ
265 1nn 12274 . . . . . . . . 9 1 ∈ ℕ
26625, 265decnncl 12750 . . . . . . . 8 11 ∈ ℕ
267266nnrei 12272 . . . . . . 7 11 ∈ ℝ
268267, 102pm3.2i 470 . . . . . 6 (11 ∈ ℝ ∧ 5 ∈ ℕ0)
269 reexpcl 14115 . . . . . 6 ((11 ∈ ℝ ∧ 5 ∈ ℕ0) → (11↑5) ∈ ℝ)
270268, 269ax-mp 5 . . . . 5 (11↑5) ∈ ℝ
271257, 102pm3.2i 470 . . . . . 6 (7 ∈ ℝ ∧ 5 ∈ ℕ0)
272 reexpcl 14115 . . . . . 6 ((7 ∈ ℝ ∧ 5 ∈ ℕ0) → (7↑5) ∈ ℝ)
273271, 272ax-mp 5 . . . . 5 (7↑5) ∈ ℝ
274264, 270, 273ltmuldivi 12185 . . . 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 11261 . . . . . . 7 (⊤ → 0 ∈ ℝ)
280260a1i 11 . . . . . . 7 (⊤ → 0 < 7)
281279, 280ltned 11394 . . . . . 6 (⊤ → 0 ≠ 7)
282281necomd 2993 . . . . 5 (⊤ → 7 ≠ 0)
283102a1i 11 . . . . 5 (⊤ → 5 ∈ ℕ0)
284277, 278, 282, 283expdivd 14196 . . . 4 (⊤ → ((11 / 7)↑5) = ((11↑5) / (7↑5)))
285284eqcomd 2740 . . 3 (⊤ → ((11↑5) / (7↑5)) = ((11 / 7)↑5))
286285mptru 1543 . 2 ((11↑5) / (7↑5)) = ((11 / 7)↑5)
287276, 286breqtri 5172 1 9 < ((11 / 7)↑5)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  w3a 1086   = wceq 1536  wtru 1537  wcel 2105   class class class wbr 5147  (class class class)co 7430  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292   / cdiv 11917  2c2 12318  3c3 12319  4c4 12320  5c5 12321  6c6 12322  7c7 12323  8c8 12324  9c9 12325  0cn0 12523  cz 12610  cdc 12730  cexp 14098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-rp 13032  df-seq 14039  df-exp 14099
This theorem is referenced by:  3lexlogpow5ineq4  42037
  Copyright terms: Public domain W3C validator