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 40048
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 2738 . . . . . . . . . 10 5 = 5
2 2p2e4 12096 . . . . . . . . . . . 12 (2 + 2) = 4
32oveq1i 7278 . . . . . . . . . . 11 ((2 + 2) + 1) = (4 + 1)
4 4p1e5 12107 . . . . . . . . . . 11 (4 + 1) = 5
53, 4eqtri 2766 . . . . . . . . . 10 ((2 + 2) + 1) = 5
61, 5eqtr4i 2769 . . . . . . . . 9 5 = ((2 + 2) + 1)
76oveq2i 7279 . . . . . . . 8 (7↑5) = (7↑((2 + 2) + 1))
8 7cn 12055 . . . . . . . . . 10 7 ∈ ℂ
9 2nn0 12238 . . . . . . . . . . 11 2 ∈ ℕ0
109, 9nn0addcli 12258 . . . . . . . . . 10 (2 + 2) ∈ ℕ0
118, 10pm3.2i 471 . . . . . . . . 9 (7 ∈ ℂ ∧ (2 + 2) ∈ ℕ0)
12 expp1 13777 . . . . . . . . 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 13813 . . . . . . . . . . 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 13885 . . . . . . . . . . . . 13 (7↑2) = (7 · 7)
18 7t7e49 12539 . . . . . . . . . . . . 13 (7 · 7) = 49
1917, 18eqtri 2766 . . . . . . . . . . . 12 (7↑2) = 49
2019, 19oveq12i 7280 . . . . . . . . . . 11 ((7↑2) · (7↑2)) = (49 · 49)
21 4nn0 12240 . . . . . . . . . . . . 13 4 ∈ ℕ0
22 9nn0 12245 . . . . . . . . . . . . 13 9 ∈ ℕ0
2321, 22deccl 12440 . . . . . . . . . . . 12 49 ∈ ℕ0
24 eqid 2738 . . . . . . . . . . . 12 49 = 49
25 1nn0 12237 . . . . . . . . . . . 12 1 ∈ ℕ0
2621, 21deccl 12440 . . . . . . . . . . . 12 44 ∈ ℕ0
27 eqid 2738 . . . . . . . . . . . . 13 44 = 44
28 0nn0 12236 . . . . . . . . . . . . 13 0 ∈ ℕ0
29 6nn0 12242 . . . . . . . . . . . . . 14 6 ∈ ℕ0
3021, 21nn0addcli 12258 . . . . . . . . . . . . . 14 (4 + 4) ∈ ℕ0
31 4t4e16 12524 . . . . . . . . . . . . . 14 (4 · 4) = 16
32 1p1e2 12086 . . . . . . . . . . . . . 14 (1 + 1) = 2
33 4p4e8 12116 . . . . . . . . . . . . . . . 16 (4 + 4) = 8
3433oveq2i 7279 . . . . . . . . . . . . . . 15 (6 + (4 + 4)) = (6 + 8)
35 8cn 12058 . . . . . . . . . . . . . . . 16 8 ∈ ℂ
36 6cn 12052 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
37 8p6e14 12509 . . . . . . . . . . . . . . . 16 (8 + 6) = 14
3835, 36, 37addcomli 11155 . . . . . . . . . . . . . . 15 (6 + 8) = 14
3934, 38eqtri 2766 . . . . . . . . . . . . . 14 (6 + (4 + 4)) = 14
4025, 29, 30, 31, 32, 21, 39decaddci 12486 . . . . . . . . . . . . 13 ((4 · 4) + (4 + 4)) = 24
41 3nn0 12239 . . . . . . . . . . . . . 14 3 ∈ ℕ0
42 9t4e36 12549 . . . . . . . . . . . . . 14 (9 · 4) = 36
43 3p1e4 12106 . . . . . . . . . . . . . 14 (3 + 1) = 4
44 6p4e10 12497 . . . . . . . . . . . . . 14 (6 + 4) = 10
4541, 29, 21, 42, 43, 44decaddci2 12487 . . . . . . . . . . . . 13 ((9 · 4) + 4) = 40
4621, 22, 21, 21, 24, 27, 21, 28, 21, 40, 45decmac 12477 . . . . . . . . . . . 12 ((49 · 4) + 44) = 240
47 8nn0 12244 . . . . . . . . . . . . 13 8 ∈ ℕ0
48 9cn 12061 . . . . . . . . . . . . . . 15 9 ∈ ℂ
49 4cn 12046 . . . . . . . . . . . . . . 15 4 ∈ ℂ
5048, 49, 42mulcomli 10972 . . . . . . . . . . . . . 14 (4 · 9) = 36
5141, 29, 47, 50, 43, 21, 38decaddci 12486 . . . . . . . . . . . . 13 ((4 · 9) + 8) = 44
52 9t9e81 12554 . . . . . . . . . . . . 13 (9 · 9) = 81
5322, 21, 22, 24, 25, 47, 51, 52decmul1c 12490 . . . . . . . . . . . 12 (49 · 9) = 441
5423, 21, 22, 24, 25, 26, 46, 53decmul2c 12491 . . . . . . . . . . 11 (49 · 49) = 2401
5520, 54eqtri 2766 . . . . . . . . . 10 ((7↑2) · (7↑2)) = 2401
5616, 55eqtri 2766 . . . . . . . . 9 (7↑(2 + 2)) = 2401
5756oveq1i 7278 . . . . . . . 8 ((7↑(2 + 2)) · 7) = (2401 · 7)
587, 13, 573eqtri 2770 . . . . . . 7 (7↑5) = (2401 · 7)
59 7nn0 12243 . . . . . . . 8 7 ∈ ℕ0
609, 21deccl 12440 . . . . . . . . 9 24 ∈ ℕ0
6160, 28deccl 12440 . . . . . . . 8 240 ∈ ℕ0
62 eqid 2738 . . . . . . . 8 2401 = 2401
6325, 29deccl 12440 . . . . . . . . . 10 16 ∈ ℕ0
6463, 47deccl 12440 . . . . . . . . 9 168 ∈ ℕ0
65 eqid 2738 . . . . . . . . . 10 240 = 240
66 eqid 2738 . . . . . . . . . . . 12 24 = 24
67 2cn 12036 . . . . . . . . . . . . . 14 2 ∈ ℂ
68 7t2e14 12534 . . . . . . . . . . . . . 14 (7 · 2) = 14
698, 67, 68mulcomli 10972 . . . . . . . . . . . . 13 (2 · 7) = 14
70 4p2e6 12114 . . . . . . . . . . . . 13 (4 + 2) = 6
7125, 21, 9, 69, 70decaddi 12485 . . . . . . . . . . . 12 ((2 · 7) + 2) = 16
72 7t4e28 12536 . . . . . . . . . . . . 13 (7 · 4) = 28
738, 49, 72mulcomli 10972 . . . . . . . . . . . 12 (4 · 7) = 28
7459, 9, 21, 66, 47, 9, 71, 73decmul1c 12490 . . . . . . . . . . 11 (24 · 7) = 168
7535addid1i 11150 . . . . . . . . . . 11 (8 + 0) = 8
7663, 47, 28, 74, 75decaddi 12485 . . . . . . . . . 10 ((24 · 7) + 0) = 168
77 0cn 10955 . . . . . . . . . . 11 0 ∈ ℂ
788mul01i 11153 . . . . . . . . . . . 12 (7 · 0) = 0
7928dec0h 12447 . . . . . . . . . . . . 13 0 = 00
8079eqcomi 2747 . . . . . . . . . . . 12 00 = 0
8178, 80eqtr4i 2769 . . . . . . . . . . 11 (7 · 0) = 00
828, 77, 81mulcomli 10972 . . . . . . . . . 10 (0 · 7) = 00
8359, 60, 28, 65, 28, 28, 76, 82decmul1c 12490 . . . . . . . . 9 (240 · 7) = 1680
84 00id 11138 . . . . . . . . 9 (0 + 0) = 0
8564, 28, 28, 83, 84decaddi 12485 . . . . . . . 8 ((240 · 7) + 0) = 1680
86 ax-1cn 10917 . . . . . . . . 9 1 ∈ ℂ
878mulid1i 10967 . . . . . . . . . 10 (7 · 1) = 7
8859dec0h 12447 . . . . . . . . . . 11 7 = 07
8988eqcomi 2747 . . . . . . . . . 10 07 = 7
9087, 89eqtr4i 2769 . . . . . . . . 9 (7 · 1) = 07
918, 86, 90mulcomli 10972 . . . . . . . 8 (1 · 7) = 07
9259, 61, 25, 62, 59, 28, 85, 91decmul1c 12490 . . . . . . 7 (2401 · 7) = 16807
9358, 92eqtri 2766 . . . . . 6 (7↑5) = 16807
9493oveq2i 7279 . . . . 5 (9 · (7↑5)) = (9 · 16807)
9564, 28deccl 12440 . . . . . . . . 9 1680 ∈ ℕ0
9695, 59deccl 12440 . . . . . . . 8 16807 ∈ ℕ0
9796nn0cni 12233 . . . . . . 7 16807 ∈ ℂ
9848, 97mulcomi 10971 . . . . . 6 (9 · 16807) = (16807 · 9)
99 eqid 2738 . . . . . . . 8 16807 = 16807
100 eqid 2738 . . . . . . . . 9 1680 = 1680
10129dec0h 12447 . . . . . . . . 9 6 = 06
102 5nn0 12241 . . . . . . . . . . . 12 5 ∈ ℕ0
10325, 102deccl 12440 . . . . . . . . . . 11 15 ∈ ℕ0
104103, 25deccl 12440 . . . . . . . . . 10 151 ∈ ℕ0
105 eqid 2738 . . . . . . . . . . 11 168 = 168
106 eqid 2738 . . . . . . . . . . . 12 16 = 16
10748mulid2i 10968 . . . . . . . . . . . . . 14 (1 · 9) = 9
10836addid2i 11151 . . . . . . . . . . . . . 14 (0 + 6) = 6
109107, 108oveq12i 7280 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 6)) = (9 + 6)
110 9p6e15 12516 . . . . . . . . . . . . 13 (9 + 6) = 15
111109, 110eqtri 2766 . . . . . . . . . . . 12 ((1 · 9) + (0 + 6)) = 15
112 9t6e54 12551 . . . . . . . . . . . . . 14 (9 · 6) = 54
11348, 36, 112mulcomli 10972 . . . . . . . . . . . . 13 (6 · 9) = 54
114 5p1e6 12108 . . . . . . . . . . . . 13 (5 + 1) = 6
115 7p4e11 12501 . . . . . . . . . . . . . 14 (7 + 4) = 11
1168, 49, 115addcomli 11155 . . . . . . . . . . . . 13 (4 + 7) = 11
117102, 21, 59, 113, 114, 25, 116decaddci 12486 . . . . . . . . . . . 12 ((6 · 9) + 7) = 61
11825, 29, 28, 59, 106, 88, 22, 25, 29, 111, 117decmac 12477 . . . . . . . . . . 11 ((16 · 9) + 7) = 151
119 9t8e72 12553 . . . . . . . . . . . 12 (9 · 8) = 72
12048, 35, 119mulcomli 10972 . . . . . . . . . . 11 (8 · 9) = 72
12122, 63, 47, 105, 9, 59, 118, 120decmul1c 12490 . . . . . . . . . 10 (168 · 9) = 1512
12267addid1i 11150 . . . . . . . . . 10 (2 + 0) = 2
123104, 9, 28, 121, 122decaddi 12485 . . . . . . . . 9 ((168 · 9) + 0) = 1512
12448mul02i 11152 . . . . . . . . . . 11 (0 · 9) = 0
125124oveq1i 7278 . . . . . . . . . 10 ((0 · 9) + 6) = (0 + 6)
126125, 108eqtri 2766 . . . . . . . . 9 ((0 · 9) + 6) = 6
12764, 28, 28, 29, 100, 101, 22, 123, 126decma 12476 . . . . . . . 8 ((1680 · 9) + 6) = 15126
128 9t7e63 12552 . . . . . . . . 9 (9 · 7) = 63
12948, 8, 128mulcomli 10972 . . . . . . . 8 (7 · 9) = 63
13022, 95, 59, 99, 41, 29, 127, 129decmul1c 12490 . . . . . . 7 (16807 · 9) = 151263
131104, 9deccl 12440 . . . . . . . . 9 1512 ∈ ℕ0
132131, 29deccl 12440 . . . . . . . 8 15126 ∈ ℕ0
13363, 25deccl 12440 . . . . . . . . . 10 161 ∈ ℕ0
134133, 28deccl 12440 . . . . . . . . 9 1610 ∈ ℕ0
135134, 102deccl 12440 . . . . . . . 8 16105 ∈ ℕ0
136 3lt10 12562 . . . . . . . 8 3 < 10
137 6lt10 12559 . . . . . . . . 9 6 < 10
138 2lt10 12563 . . . . . . . . . 10 2 < 10
139 1lt10 12564 . . . . . . . . . . 11 1 < 10
140 6nn 12050 . . . . . . . . . . . 12 6 ∈ ℕ
141 5lt6 12142 . . . . . . . . . . . 12 5 < 6
14225, 102, 140, 141declt 12453 . . . . . . . . . . 11 15 < 16
143103, 63, 25, 25, 139, 142decltc 12454 . . . . . . . . . 10 151 < 161
144104, 133, 9, 28, 138, 143decltc 12454 . . . . . . . . 9 1512 < 1610
145131, 134, 29, 102, 137, 144decltc 12454 . . . . . . . 8 15126 < 16105
146132, 135, 41, 25, 136, 145decltc 12454 . . . . . . 7 151263 < 161051
147130, 146eqbrtri 5095 . . . . . 6 (16807 · 9) < 161051
14898, 147eqbrtri 5095 . . . . 5 (9 · 16807) < 161051
14994, 148eqbrtri 5095 . . . 4 (9 · (7↑5)) < 161051
1504eqcomi 2747 . . . . . . . 8 5 = (4 + 1)
151150oveq2i 7279 . . . . . . 7 (11↑5) = (11↑(4 + 1))
15225, 25deccl 12440 . . . . . . . . . . 11 11 ∈ ℕ0
153152nn0cni 12233 . . . . . . . . . 10 11 ∈ ℂ
154153, 21pm3.2i 471 . . . . . . . . 9 (11 ∈ ℂ ∧ 4 ∈ ℕ0)
155 expp1 13777 . . . . . . . . 9 ((11 ∈ ℂ ∧ 4 ∈ ℕ0) → (11↑(4 + 1)) = ((11↑4) · 11))
156154, 155ax-mp 5 . . . . . . . 8 (11↑(4 + 1)) = ((11↑4) · 11)
1572eqcomi 2747 . . . . . . . . . . 11 4 = (2 + 2)
158157oveq2i 7279 . . . . . . . . . 10 (11↑4) = (11↑(2 + 2))
159153, 9, 93pm3.2i 1338 . . . . . . . . . . . 12 (11 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
160 expadd 13813 . . . . . . . . . . . 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 13885 . . . . . . . . . . . . . 14 (11↑2) = (11 · 11)
163 eqid 2738 . . . . . . . . . . . . . . 15 11 = 11
164153mulid2i 10968 . . . . . . . . . . . . . . . 16 (1 · 11) = 11
16525, 25, 32, 164decsuc 12456 . . . . . . . . . . . . . . 15 ((1 · 11) + 1) = 12
166152, 25, 25, 163, 25, 25, 165, 164decmul1c 12490 . . . . . . . . . . . . . 14 (11 · 11) = 121
167162, 166eqtri 2766 . . . . . . . . . . . . 13 (11↑2) = 121
168167, 167oveq12i 7280 . . . . . . . . . . . 12 ((11↑2) · (11↑2)) = (121 · 121)
16925, 9deccl 12440 . . . . . . . . . . . . . 14 12 ∈ ℕ0
170169, 25deccl 12440 . . . . . . . . . . . . 13 121 ∈ ℕ0
171 eqid 2738 . . . . . . . . . . . . 13 121 = 121
172 eqid 2738 . . . . . . . . . . . . . 14 12 = 12
173170nn0cni 12233 . . . . . . . . . . . . . . . 16 121 ∈ ℂ
174173mulid2i 10968 . . . . . . . . . . . . . . 15 (1 · 121) = 121
17525dec0h 12447 . . . . . . . . . . . . . . . 16 1 = 01
17667addid2i 11151 . . . . . . . . . . . . . . . 16 (0 + 2) = 2
17749, 86, 4addcomli 11155 . . . . . . . . . . . . . . . 16 (1 + 4) = 5
17828, 25, 9, 21, 175, 66, 176, 177decadd 12479 . . . . . . . . . . . . . . 15 (1 + 24) = 25
17925, 9, 9, 172, 2decaddi 12485 . . . . . . . . . . . . . . 15 (12 + 2) = 14
180 5cn 12049 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
181180, 86, 114addcomli 11155 . . . . . . . . . . . . . . 15 (1 + 5) = 6
182169, 25, 9, 102, 174, 178, 179, 181decadd 12479 . . . . . . . . . . . . . 14 ((1 · 121) + (1 + 24)) = 146
1839dec0h 12447 . . . . . . . . . . . . . . 15 2 = 02
18428, 28nn0addcli 12258 . . . . . . . . . . . . . . . 16 (0 + 0) ∈ ℕ0
185 2t1e2 12124 . . . . . . . . . . . . . . . . . . 19 (2 · 1) = 2
186185oveq1i 7278 . . . . . . . . . . . . . . . . . 18 ((2 · 1) + 0) = (2 + 0)
187186, 122eqtri 2766 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 0) = 2
188 2t2e4 12125 . . . . . . . . . . . . . . . . . 18 (2 · 2) = 4
18921dec0h 12447 . . . . . . . . . . . . . . . . . . 19 4 = 04
190189eqcomi 2747 . . . . . . . . . . . . . . . . . 18 04 = 4
191188, 190eqtr4i 2769 . . . . . . . . . . . . . . . . 17 (2 · 2) = 04
1929, 25, 9, 172, 21, 28, 187, 191decmul2c 12491 . . . . . . . . . . . . . . . 16 (2 · 12) = 24
19384oveq2i 7279 . . . . . . . . . . . . . . . . 17 (4 + (0 + 0)) = (4 + 0)
19449addid1i 11150 . . . . . . . . . . . . . . . . 17 (4 + 0) = 4
195193, 194eqtri 2766 . . . . . . . . . . . . . . . 16 (4 + (0 + 0)) = 4
1969, 21, 184, 192, 195decaddi 12485 . . . . . . . . . . . . . . 15 ((2 · 12) + (0 + 0)) = 24
197185oveq1i 7278 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 2) = (2 + 2)
198197, 2eqtri 2766 . . . . . . . . . . . . . . . 16 ((2 · 1) + 2) = 4
199198, 190eqtr4i 2769 . . . . . . . . . . . . . . 15 ((2 · 1) + 2) = 04
200169, 25, 28, 9, 171, 183, 9, 21, 28, 196, 199decma2c 12478 . . . . . . . . . . . . . 14 ((2 · 121) + 2) = 244
20125, 9, 25, 9, 172, 172, 170, 21, 60, 182, 200decmac 12477 . . . . . . . . . . . . 13 ((12 · 121) + 12) = 1464
202170, 169, 25, 171, 25, 169, 201, 174decmul1c 12490 . . . . . . . . . . . 12 (121 · 121) = 14641
203168, 202eqtri 2766 . . . . . . . . . . 11 ((11↑2) · (11↑2)) = 14641
204161, 203eqtri 2766 . . . . . . . . . 10 (11↑(2 + 2)) = 14641
205158, 204eqtri 2766 . . . . . . . . 9 (11↑4) = 14641
206205oveq1i 7278 . . . . . . . 8 ((11↑4) · 11) = (14641 · 11)
207156, 206eqtri 2766 . . . . . . 7 (11↑(4 + 1)) = (14641 · 11)
208151, 207eqtri 2766 . . . . . 6 (11↑5) = (14641 · 11)
20925, 21deccl 12440 . . . . . . . . 9 14 ∈ ℕ0
210209, 29deccl 12440 . . . . . . . 8 146 ∈ ℕ0
211210, 21deccl 12440 . . . . . . 7 1464 ∈ ℕ0
212 eqid 2738 . . . . . . 7 14641 = 14641
213 eqid 2738 . . . . . . . 8 1464 = 1464
214 eqid 2738 . . . . . . . . 9 146 = 146
215194, 190eqtr4i 2769 . . . . . . . . . 10 (4 + 0) = 04
21649, 77, 215addcomli 11155 . . . . . . . . 9 (0 + 4) = 04
217 eqid 2738 . . . . . . . . . 10 14 = 14
2188addid1i 11150 . . . . . . . . . . . 12 (7 + 0) = 7
219218, 89eqtr4i 2769 . . . . . . . . . . 11 (7 + 0) = 07
2208, 77, 219addcomli 11155 . . . . . . . . . 10 (0 + 7) = 07
22128, 102nn0addcli 12258 . . . . . . . . . . 11 (0 + 5) ∈ ℕ0
222180addid2i 11151 . . . . . . . . . . . . 13 (0 + 5) = 5
223222oveq2i 7279 . . . . . . . . . . . 12 (1 + (0 + 5)) = (1 + 5)
224223, 181eqtri 2766 . . . . . . . . . . 11 (1 + (0 + 5)) = 6
22525, 25, 221, 164, 224decaddi 12485 . . . . . . . . . 10 ((1 · 11) + (0 + 5)) = 16
22649mulid1i 10967 . . . . . . . . . . . . 13 (4 · 1) = 4
227 0p1e1 12083 . . . . . . . . . . . . 13 (0 + 1) = 1
228226, 227oveq12i 7280 . . . . . . . . . . . 12 ((4 · 1) + (0 + 1)) = (4 + 1)
229228, 4eqtri 2766 . . . . . . . . . . 11 ((4 · 1) + (0 + 1)) = 5
230226oveq1i 7278 . . . . . . . . . . . 12 ((4 · 1) + 7) = (4 + 7)
231230, 116eqtri 2766 . . . . . . . . . . 11 ((4 · 1) + 7) = 11
23225, 25, 28, 59, 163, 88, 21, 25, 25, 229, 231decma2c 12478 . . . . . . . . . 10 ((4 · 11) + 7) = 51
23325, 21, 28, 59, 217, 220, 152, 25, 102, 225, 232decmac 12477 . . . . . . . . 9 ((14 · 11) + (0 + 7)) = 161
23436mulid1i 10967 . . . . . . . . . . . 12 (6 · 1) = 6
23586addid2i 11151 . . . . . . . . . . . 12 (0 + 1) = 1
236234, 235oveq12i 7280 . . . . . . . . . . 11 ((6 · 1) + (0 + 1)) = (6 + 1)
237 6p1e7 12109 . . . . . . . . . . 11 (6 + 1) = 7
238236, 237eqtri 2766 . . . . . . . . . 10 ((6 · 1) + (0 + 1)) = 7
239 eqid 2738 . . . . . . . . . . . 12 4 = 4
240234, 239oveq12i 7280 . . . . . . . . . . 11 ((6 · 1) + 4) = (6 + 4)
241240, 44eqtri 2766 . . . . . . . . . 10 ((6 · 1) + 4) = 10
24225, 25, 28, 21, 163, 189, 29, 28, 25, 238, 241decma2c 12478 . . . . . . . . 9 ((6 · 11) + 4) = 70
243209, 29, 28, 21, 214, 216, 152, 28, 59, 233, 242decmac 12477 . . . . . . . 8 ((146 · 11) + (0 + 4)) = 1610
244226, 84oveq12i 7280 . . . . . . . . . 10 ((4 · 1) + (0 + 0)) = (4 + 0)
245244, 194eqtri 2766 . . . . . . . . 9 ((4 · 1) + (0 + 0)) = 4
246226oveq1i 7278 . . . . . . . . . . 11 ((4 · 1) + 1) = (4 + 1)
247246, 4eqtri 2766 . . . . . . . . . 10 ((4 · 1) + 1) = 5
248102dec0h 12447 . . . . . . . . . . 11 5 = 05
249248eqcomi 2747 . . . . . . . . . 10 05 = 5
250247, 249eqtr4i 2769 . . . . . . . . 9 ((4 · 1) + 1) = 05
25125, 25, 28, 25, 163, 175, 21, 102, 28, 245, 250decma2c 12478 . . . . . . . 8 ((4 · 11) + 1) = 45
252210, 21, 28, 25, 213, 175, 152, 102, 21, 243, 251decmac 12477 . . . . . . 7 ((1464 · 11) + 1) = 16105
253152, 211, 25, 212, 25, 25, 252, 164decmul1c 12490 . . . . . 6 (14641 · 11) = 161051
254208, 253eqtri 2766 . . . . 5 (11↑5) = 161051
255254eqcomi 2747 . . . 4 161051 = (11↑5)
256149, 255breqtri 5099 . . 3 (9 · (7↑5)) < (11↑5)
257 7re 12054 . . . . . 6 7 ∈ ℝ
258 5nn 12047 . . . . . . 7 5 ∈ ℕ
259258nnzi 12332 . . . . . 6 5 ∈ ℤ
260 7pos 12072 . . . . . 6 0 < 7
261257, 259, 2603pm3.2i 1338 . . . . 5 (7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7)
262 expgt0 13804 . . . . 5 ((7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) → 0 < (7↑5))
263261, 262ax-mp 5 . . . 4 0 < (7↑5)
264 9re 12060 . . . . 5 9 ∈ ℝ
265 1nn 11972 . . . . . . . . 9 1 ∈ ℕ
26625, 265decnncl 12445 . . . . . . . 8 11 ∈ ℕ
267266nnrei 11970 . . . . . . 7 11 ∈ ℝ
268267, 102pm3.2i 471 . . . . . 6 (11 ∈ ℝ ∧ 5 ∈ ℕ0)
269 reexpcl 13787 . . . . . 6 ((11 ∈ ℝ ∧ 5 ∈ ℕ0) → (11↑5) ∈ ℝ)
270268, 269ax-mp 5 . . . . 5 (11↑5) ∈ ℝ
271257, 102pm3.2i 471 . . . . . 6 (7 ∈ ℝ ∧ 5 ∈ ℕ0)
272 reexpcl 13787 . . . . . 6 ((7 ∈ ℝ ∧ 5 ∈ ℕ0) → (7↑5) ∈ ℝ)
273271, 272ax-mp 5 . . . . 5 (7↑5) ∈ ℝ
274264, 270, 273ltmuldivi 11883 . . . 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 10966 . . . . . . 7 (⊤ → 0 ∈ ℝ)
280260a1i 11 . . . . . . 7 (⊤ → 0 < 7)
281279, 280ltned 11099 . . . . . 6 (⊤ → 0 ≠ 7)
282281necomd 2999 . . . . 5 (⊤ → 7 ≠ 0)
283102a1i 11 . . . . 5 (⊤ → 5 ∈ ℕ0)
284277, 278, 282, 283expdivd 13866 . . . 4 (⊤ → ((11 / 7)↑5) = ((11↑5) / (7↑5)))
285284eqcomd 2744 . . 3 (⊤ → ((11↑5) / (7↑5)) = ((11 / 7)↑5))
286285mptru 1546 . 2 ((11↑5) / (7↑5)) = ((11 / 7)↑5)
287276, 286breqtri 5099 1 9 < ((11 / 7)↑5)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  w3a 1086   = wceq 1539  wtru 1540  wcel 2106   class class class wbr 5074  (class class class)co 7268  cc 10857  cr 10858  0cc0 10859  1c1 10860   + caddc 10862   · cmul 10864   < clt 10997   / cdiv 11620  2c2 12016  3c3 12017  4c4 12018  5c5 12019  6c6 12020  7c7 12021  8c8 12022  9c9 12023  0cn0 12221  cz 12307  cdc 12425  cexp 13770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5222  ax-nul 5229  ax-pow 5287  ax-pr 5351  ax-un 7579  ax-cnex 10915  ax-resscn 10916  ax-1cn 10917  ax-icn 10918  ax-addcl 10919  ax-addrcl 10920  ax-mulcl 10921  ax-mulrcl 10922  ax-mulcom 10923  ax-addass 10924  ax-mulass 10925  ax-distr 10926  ax-i2m1 10927  ax-1ne0 10928  ax-1rid 10929  ax-rnegex 10930  ax-rrecex 10931  ax-cnre 10932  ax-pre-lttri 10933  ax-pre-lttrn 10934  ax-pre-ltadd 10935  ax-pre-mulgt0 10936
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3432  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5485  df-eprel 5491  df-po 5499  df-so 5500  df-fr 5540  df-we 5542  df-xp 5591  df-rel 5592  df-cnv 5593  df-co 5594  df-dm 5595  df-rn 5596  df-res 5597  df-ima 5598  df-pred 6196  df-ord 6263  df-on 6264  df-lim 6265  df-suc 6266  df-iota 6385  df-fun 6429  df-fn 6430  df-f 6431  df-f1 6432  df-fo 6433  df-f1o 6434  df-fv 6435  df-riota 7225  df-ov 7271  df-oprab 7272  df-mpo 7273  df-om 7704  df-2nd 7822  df-frecs 8085  df-wrecs 8116  df-recs 8190  df-rdg 8229  df-er 8486  df-en 8722  df-dom 8723  df-sdom 8724  df-pnf 10999  df-mnf 11000  df-xr 11001  df-ltxr 11002  df-le 11003  df-sub 11195  df-neg 11196  df-div 11621  df-nn 11962  df-2 12024  df-3 12025  df-4 12026  df-5 12027  df-6 12028  df-7 12029  df-8 12030  df-9 12031  df-n0 12222  df-z 12308  df-dec 12426  df-uz 12571  df-rp 12719  df-seq 13710  df-exp 13771
This theorem is referenced by:  3lexlogpow5ineq4  40050
  Copyright terms: Public domain W3C validator