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 40919
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 2733 . . . . . . . . . 10 5 = 5
2 2p2e4 12347 . . . . . . . . . . . 12 (2 + 2) = 4
32oveq1i 7419 . . . . . . . . . . 11 ((2 + 2) + 1) = (4 + 1)
4 4p1e5 12358 . . . . . . . . . . 11 (4 + 1) = 5
53, 4eqtri 2761 . . . . . . . . . 10 ((2 + 2) + 1) = 5
61, 5eqtr4i 2764 . . . . . . . . 9 5 = ((2 + 2) + 1)
76oveq2i 7420 . . . . . . . 8 (7↑5) = (7↑((2 + 2) + 1))
8 7cn 12306 . . . . . . . . . 10 7 ∈ ℂ
9 2nn0 12489 . . . . . . . . . . 11 2 ∈ ℕ0
109, 9nn0addcli 12509 . . . . . . . . . 10 (2 + 2) ∈ ℕ0
118, 10pm3.2i 472 . . . . . . . . 9 (7 ∈ ℂ ∧ (2 + 2) ∈ ℕ0)
12 expp1 14034 . . . . . . . . 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 14070 . . . . . . . . . . 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 14144 . . . . . . . . . . . . 13 (7↑2) = (7 · 7)
18 7t7e49 12791 . . . . . . . . . . . . 13 (7 · 7) = 49
1917, 18eqtri 2761 . . . . . . . . . . . 12 (7↑2) = 49
2019, 19oveq12i 7421 . . . . . . . . . . 11 ((7↑2) · (7↑2)) = (49 · 49)
21 4nn0 12491 . . . . . . . . . . . . 13 4 ∈ ℕ0
22 9nn0 12496 . . . . . . . . . . . . 13 9 ∈ ℕ0
2321, 22deccl 12692 . . . . . . . . . . . 12 49 ∈ ℕ0
24 eqid 2733 . . . . . . . . . . . 12 49 = 49
25 1nn0 12488 . . . . . . . . . . . 12 1 ∈ ℕ0
2621, 21deccl 12692 . . . . . . . . . . . 12 44 ∈ ℕ0
27 eqid 2733 . . . . . . . . . . . . 13 44 = 44
28 0nn0 12487 . . . . . . . . . . . . 13 0 ∈ ℕ0
29 6nn0 12493 . . . . . . . . . . . . . 14 6 ∈ ℕ0
3021, 21nn0addcli 12509 . . . . . . . . . . . . . 14 (4 + 4) ∈ ℕ0
31 4t4e16 12776 . . . . . . . . . . . . . 14 (4 · 4) = 16
32 1p1e2 12337 . . . . . . . . . . . . . 14 (1 + 1) = 2
33 4p4e8 12367 . . . . . . . . . . . . . . . 16 (4 + 4) = 8
3433oveq2i 7420 . . . . . . . . . . . . . . 15 (6 + (4 + 4)) = (6 + 8)
35 8cn 12309 . . . . . . . . . . . . . . . 16 8 ∈ ℂ
36 6cn 12303 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
37 8p6e14 12761 . . . . . . . . . . . . . . . 16 (8 + 6) = 14
3835, 36, 37addcomli 11406 . . . . . . . . . . . . . . 15 (6 + 8) = 14
3934, 38eqtri 2761 . . . . . . . . . . . . . 14 (6 + (4 + 4)) = 14
4025, 29, 30, 31, 32, 21, 39decaddci 12738 . . . . . . . . . . . . 13 ((4 · 4) + (4 + 4)) = 24
41 3nn0 12490 . . . . . . . . . . . . . 14 3 ∈ ℕ0
42 9t4e36 12801 . . . . . . . . . . . . . 14 (9 · 4) = 36
43 3p1e4 12357 . . . . . . . . . . . . . 14 (3 + 1) = 4
44 6p4e10 12749 . . . . . . . . . . . . . 14 (6 + 4) = 10
4541, 29, 21, 42, 43, 44decaddci2 12739 . . . . . . . . . . . . 13 ((9 · 4) + 4) = 40
4621, 22, 21, 21, 24, 27, 21, 28, 21, 40, 45decmac 12729 . . . . . . . . . . . 12 ((49 · 4) + 44) = 240
47 8nn0 12495 . . . . . . . . . . . . 13 8 ∈ ℕ0
48 9cn 12312 . . . . . . . . . . . . . . 15 9 ∈ ℂ
49 4cn 12297 . . . . . . . . . . . . . . 15 4 ∈ ℂ
5048, 49, 42mulcomli 11223 . . . . . . . . . . . . . 14 (4 · 9) = 36
5141, 29, 47, 50, 43, 21, 38decaddci 12738 . . . . . . . . . . . . 13 ((4 · 9) + 8) = 44
52 9t9e81 12806 . . . . . . . . . . . . 13 (9 · 9) = 81
5322, 21, 22, 24, 25, 47, 51, 52decmul1c 12742 . . . . . . . . . . . 12 (49 · 9) = 441
5423, 21, 22, 24, 25, 26, 46, 53decmul2c 12743 . . . . . . . . . . 11 (49 · 49) = 2401
5520, 54eqtri 2761 . . . . . . . . . 10 ((7↑2) · (7↑2)) = 2401
5616, 55eqtri 2761 . . . . . . . . 9 (7↑(2 + 2)) = 2401
5756oveq1i 7419 . . . . . . . 8 ((7↑(2 + 2)) · 7) = (2401 · 7)
587, 13, 573eqtri 2765 . . . . . . 7 (7↑5) = (2401 · 7)
59 7nn0 12494 . . . . . . . 8 7 ∈ ℕ0
609, 21deccl 12692 . . . . . . . . 9 24 ∈ ℕ0
6160, 28deccl 12692 . . . . . . . 8 240 ∈ ℕ0
62 eqid 2733 . . . . . . . 8 2401 = 2401
6325, 29deccl 12692 . . . . . . . . . 10 16 ∈ ℕ0
6463, 47deccl 12692 . . . . . . . . 9 168 ∈ ℕ0
65 eqid 2733 . . . . . . . . . 10 240 = 240
66 eqid 2733 . . . . . . . . . . . 12 24 = 24
67 2cn 12287 . . . . . . . . . . . . . 14 2 ∈ ℂ
68 7t2e14 12786 . . . . . . . . . . . . . 14 (7 · 2) = 14
698, 67, 68mulcomli 11223 . . . . . . . . . . . . 13 (2 · 7) = 14
70 4p2e6 12365 . . . . . . . . . . . . 13 (4 + 2) = 6
7125, 21, 9, 69, 70decaddi 12737 . . . . . . . . . . . 12 ((2 · 7) + 2) = 16
72 7t4e28 12788 . . . . . . . . . . . . 13 (7 · 4) = 28
738, 49, 72mulcomli 11223 . . . . . . . . . . . 12 (4 · 7) = 28
7459, 9, 21, 66, 47, 9, 71, 73decmul1c 12742 . . . . . . . . . . 11 (24 · 7) = 168
7535addridi 11401 . . . . . . . . . . 11 (8 + 0) = 8
7663, 47, 28, 74, 75decaddi 12737 . . . . . . . . . 10 ((24 · 7) + 0) = 168
77 0cn 11206 . . . . . . . . . . 11 0 ∈ ℂ
788mul01i 11404 . . . . . . . . . . . 12 (7 · 0) = 0
7928dec0h 12699 . . . . . . . . . . . . 13 0 = 00
8079eqcomi 2742 . . . . . . . . . . . 12 00 = 0
8178, 80eqtr4i 2764 . . . . . . . . . . 11 (7 · 0) = 00
828, 77, 81mulcomli 11223 . . . . . . . . . 10 (0 · 7) = 00
8359, 60, 28, 65, 28, 28, 76, 82decmul1c 12742 . . . . . . . . 9 (240 · 7) = 1680
84 00id 11389 . . . . . . . . 9 (0 + 0) = 0
8564, 28, 28, 83, 84decaddi 12737 . . . . . . . 8 ((240 · 7) + 0) = 1680
86 ax-1cn 11168 . . . . . . . . 9 1 ∈ ℂ
878mulridi 11218 . . . . . . . . . 10 (7 · 1) = 7
8859dec0h 12699 . . . . . . . . . . 11 7 = 07
8988eqcomi 2742 . . . . . . . . . 10 07 = 7
9087, 89eqtr4i 2764 . . . . . . . . 9 (7 · 1) = 07
918, 86, 90mulcomli 11223 . . . . . . . 8 (1 · 7) = 07
9259, 61, 25, 62, 59, 28, 85, 91decmul1c 12742 . . . . . . 7 (2401 · 7) = 16807
9358, 92eqtri 2761 . . . . . 6 (7↑5) = 16807
9493oveq2i 7420 . . . . 5 (9 · (7↑5)) = (9 · 16807)
9564, 28deccl 12692 . . . . . . . . 9 1680 ∈ ℕ0
9695, 59deccl 12692 . . . . . . . 8 16807 ∈ ℕ0
9796nn0cni 12484 . . . . . . 7 16807 ∈ ℂ
9848, 97mulcomi 11222 . . . . . 6 (9 · 16807) = (16807 · 9)
99 eqid 2733 . . . . . . . 8 16807 = 16807
100 eqid 2733 . . . . . . . . 9 1680 = 1680
10129dec0h 12699 . . . . . . . . 9 6 = 06
102 5nn0 12492 . . . . . . . . . . . 12 5 ∈ ℕ0
10325, 102deccl 12692 . . . . . . . . . . 11 15 ∈ ℕ0
104103, 25deccl 12692 . . . . . . . . . 10 151 ∈ ℕ0
105 eqid 2733 . . . . . . . . . . 11 168 = 168
106 eqid 2733 . . . . . . . . . . . 12 16 = 16
10748mullidi 11219 . . . . . . . . . . . . . 14 (1 · 9) = 9
10836addlidi 11402 . . . . . . . . . . . . . 14 (0 + 6) = 6
109107, 108oveq12i 7421 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 6)) = (9 + 6)
110 9p6e15 12768 . . . . . . . . . . . . 13 (9 + 6) = 15
111109, 110eqtri 2761 . . . . . . . . . . . 12 ((1 · 9) + (0 + 6)) = 15
112 9t6e54 12803 . . . . . . . . . . . . . 14 (9 · 6) = 54
11348, 36, 112mulcomli 11223 . . . . . . . . . . . . 13 (6 · 9) = 54
114 5p1e6 12359 . . . . . . . . . . . . 13 (5 + 1) = 6
115 7p4e11 12753 . . . . . . . . . . . . . 14 (7 + 4) = 11
1168, 49, 115addcomli 11406 . . . . . . . . . . . . 13 (4 + 7) = 11
117102, 21, 59, 113, 114, 25, 116decaddci 12738 . . . . . . . . . . . 12 ((6 · 9) + 7) = 61
11825, 29, 28, 59, 106, 88, 22, 25, 29, 111, 117decmac 12729 . . . . . . . . . . 11 ((16 · 9) + 7) = 151
119 9t8e72 12805 . . . . . . . . . . . 12 (9 · 8) = 72
12048, 35, 119mulcomli 11223 . . . . . . . . . . 11 (8 · 9) = 72
12122, 63, 47, 105, 9, 59, 118, 120decmul1c 12742 . . . . . . . . . 10 (168 · 9) = 1512
12267addridi 11401 . . . . . . . . . 10 (2 + 0) = 2
123104, 9, 28, 121, 122decaddi 12737 . . . . . . . . 9 ((168 · 9) + 0) = 1512
12448mul02i 11403 . . . . . . . . . . 11 (0 · 9) = 0
125124oveq1i 7419 . . . . . . . . . 10 ((0 · 9) + 6) = (0 + 6)
126125, 108eqtri 2761 . . . . . . . . 9 ((0 · 9) + 6) = 6
12764, 28, 28, 29, 100, 101, 22, 123, 126decma 12728 . . . . . . . 8 ((1680 · 9) + 6) = 15126
128 9t7e63 12804 . . . . . . . . 9 (9 · 7) = 63
12948, 8, 128mulcomli 11223 . . . . . . . 8 (7 · 9) = 63
13022, 95, 59, 99, 41, 29, 127, 129decmul1c 12742 . . . . . . 7 (16807 · 9) = 151263
131104, 9deccl 12692 . . . . . . . . 9 1512 ∈ ℕ0
132131, 29deccl 12692 . . . . . . . 8 15126 ∈ ℕ0
13363, 25deccl 12692 . . . . . . . . . 10 161 ∈ ℕ0
134133, 28deccl 12692 . . . . . . . . 9 1610 ∈ ℕ0
135134, 102deccl 12692 . . . . . . . 8 16105 ∈ ℕ0
136 3lt10 12814 . . . . . . . 8 3 < 10
137 6lt10 12811 . . . . . . . . 9 6 < 10
138 2lt10 12815 . . . . . . . . . 10 2 < 10
139 1lt10 12816 . . . . . . . . . . 11 1 < 10
140 6nn 12301 . . . . . . . . . . . 12 6 ∈ ℕ
141 5lt6 12393 . . . . . . . . . . . 12 5 < 6
14225, 102, 140, 141declt 12705 . . . . . . . . . . 11 15 < 16
143103, 63, 25, 25, 139, 142decltc 12706 . . . . . . . . . 10 151 < 161
144104, 133, 9, 28, 138, 143decltc 12706 . . . . . . . . 9 1512 < 1610
145131, 134, 29, 102, 137, 144decltc 12706 . . . . . . . 8 15126 < 16105
146132, 135, 41, 25, 136, 145decltc 12706 . . . . . . 7 151263 < 161051
147130, 146eqbrtri 5170 . . . . . 6 (16807 · 9) < 161051
14898, 147eqbrtri 5170 . . . . 5 (9 · 16807) < 161051
14994, 148eqbrtri 5170 . . . 4 (9 · (7↑5)) < 161051
1504eqcomi 2742 . . . . . . . 8 5 = (4 + 1)
151150oveq2i 7420 . . . . . . 7 (11↑5) = (11↑(4 + 1))
15225, 25deccl 12692 . . . . . . . . . . 11 11 ∈ ℕ0
153152nn0cni 12484 . . . . . . . . . 10 11 ∈ ℂ
154153, 21pm3.2i 472 . . . . . . . . 9 (11 ∈ ℂ ∧ 4 ∈ ℕ0)
155 expp1 14034 . . . . . . . . 9 ((11 ∈ ℂ ∧ 4 ∈ ℕ0) → (11↑(4 + 1)) = ((11↑4) · 11))
156154, 155ax-mp 5 . . . . . . . 8 (11↑(4 + 1)) = ((11↑4) · 11)
1572eqcomi 2742 . . . . . . . . . . 11 4 = (2 + 2)
158157oveq2i 7420 . . . . . . . . . 10 (11↑4) = (11↑(2 + 2))
159153, 9, 93pm3.2i 1340 . . . . . . . . . . . 12 (11 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
160 expadd 14070 . . . . . . . . . . . 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 14144 . . . . . . . . . . . . . 14 (11↑2) = (11 · 11)
163 eqid 2733 . . . . . . . . . . . . . . 15 11 = 11
164153mullidi 11219 . . . . . . . . . . . . . . . 16 (1 · 11) = 11
16525, 25, 32, 164decsuc 12708 . . . . . . . . . . . . . . 15 ((1 · 11) + 1) = 12
166152, 25, 25, 163, 25, 25, 165, 164decmul1c 12742 . . . . . . . . . . . . . 14 (11 · 11) = 121
167162, 166eqtri 2761 . . . . . . . . . . . . 13 (11↑2) = 121
168167, 167oveq12i 7421 . . . . . . . . . . . 12 ((11↑2) · (11↑2)) = (121 · 121)
16925, 9deccl 12692 . . . . . . . . . . . . . 14 12 ∈ ℕ0
170169, 25deccl 12692 . . . . . . . . . . . . 13 121 ∈ ℕ0
171 eqid 2733 . . . . . . . . . . . . 13 121 = 121
172 eqid 2733 . . . . . . . . . . . . . 14 12 = 12
173170nn0cni 12484 . . . . . . . . . . . . . . . 16 121 ∈ ℂ
174173mullidi 11219 . . . . . . . . . . . . . . 15 (1 · 121) = 121
17525dec0h 12699 . . . . . . . . . . . . . . . 16 1 = 01
17667addlidi 11402 . . . . . . . . . . . . . . . 16 (0 + 2) = 2
17749, 86, 4addcomli 11406 . . . . . . . . . . . . . . . 16 (1 + 4) = 5
17828, 25, 9, 21, 175, 66, 176, 177decadd 12731 . . . . . . . . . . . . . . 15 (1 + 24) = 25
17925, 9, 9, 172, 2decaddi 12737 . . . . . . . . . . . . . . 15 (12 + 2) = 14
180 5cn 12300 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
181180, 86, 114addcomli 11406 . . . . . . . . . . . . . . 15 (1 + 5) = 6
182169, 25, 9, 102, 174, 178, 179, 181decadd 12731 . . . . . . . . . . . . . 14 ((1 · 121) + (1 + 24)) = 146
1839dec0h 12699 . . . . . . . . . . . . . . 15 2 = 02
18428, 28nn0addcli 12509 . . . . . . . . . . . . . . . 16 (0 + 0) ∈ ℕ0
185 2t1e2 12375 . . . . . . . . . . . . . . . . . . 19 (2 · 1) = 2
186185oveq1i 7419 . . . . . . . . . . . . . . . . . 18 ((2 · 1) + 0) = (2 + 0)
187186, 122eqtri 2761 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 0) = 2
188 2t2e4 12376 . . . . . . . . . . . . . . . . . 18 (2 · 2) = 4
18921dec0h 12699 . . . . . . . . . . . . . . . . . . 19 4 = 04
190189eqcomi 2742 . . . . . . . . . . . . . . . . . 18 04 = 4
191188, 190eqtr4i 2764 . . . . . . . . . . . . . . . . 17 (2 · 2) = 04
1929, 25, 9, 172, 21, 28, 187, 191decmul2c 12743 . . . . . . . . . . . . . . . 16 (2 · 12) = 24
19384oveq2i 7420 . . . . . . . . . . . . . . . . 17 (4 + (0 + 0)) = (4 + 0)
19449addridi 11401 . . . . . . . . . . . . . . . . 17 (4 + 0) = 4
195193, 194eqtri 2761 . . . . . . . . . . . . . . . 16 (4 + (0 + 0)) = 4
1969, 21, 184, 192, 195decaddi 12737 . . . . . . . . . . . . . . 15 ((2 · 12) + (0 + 0)) = 24
197185oveq1i 7419 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 2) = (2 + 2)
198197, 2eqtri 2761 . . . . . . . . . . . . . . . 16 ((2 · 1) + 2) = 4
199198, 190eqtr4i 2764 . . . . . . . . . . . . . . 15 ((2 · 1) + 2) = 04
200169, 25, 28, 9, 171, 183, 9, 21, 28, 196, 199decma2c 12730 . . . . . . . . . . . . . 14 ((2 · 121) + 2) = 244
20125, 9, 25, 9, 172, 172, 170, 21, 60, 182, 200decmac 12729 . . . . . . . . . . . . 13 ((12 · 121) + 12) = 1464
202170, 169, 25, 171, 25, 169, 201, 174decmul1c 12742 . . . . . . . . . . . 12 (121 · 121) = 14641
203168, 202eqtri 2761 . . . . . . . . . . 11 ((11↑2) · (11↑2)) = 14641
204161, 203eqtri 2761 . . . . . . . . . 10 (11↑(2 + 2)) = 14641
205158, 204eqtri 2761 . . . . . . . . 9 (11↑4) = 14641
206205oveq1i 7419 . . . . . . . 8 ((11↑4) · 11) = (14641 · 11)
207156, 206eqtri 2761 . . . . . . 7 (11↑(4 + 1)) = (14641 · 11)
208151, 207eqtri 2761 . . . . . 6 (11↑5) = (14641 · 11)
20925, 21deccl 12692 . . . . . . . . 9 14 ∈ ℕ0
210209, 29deccl 12692 . . . . . . . 8 146 ∈ ℕ0
211210, 21deccl 12692 . . . . . . 7 1464 ∈ ℕ0
212 eqid 2733 . . . . . . 7 14641 = 14641
213 eqid 2733 . . . . . . . 8 1464 = 1464
214 eqid 2733 . . . . . . . . 9 146 = 146
215194, 190eqtr4i 2764 . . . . . . . . . 10 (4 + 0) = 04
21649, 77, 215addcomli 11406 . . . . . . . . 9 (0 + 4) = 04
217 eqid 2733 . . . . . . . . . 10 14 = 14
2188addridi 11401 . . . . . . . . . . . 12 (7 + 0) = 7
219218, 89eqtr4i 2764 . . . . . . . . . . 11 (7 + 0) = 07
2208, 77, 219addcomli 11406 . . . . . . . . . 10 (0 + 7) = 07
22128, 102nn0addcli 12509 . . . . . . . . . . 11 (0 + 5) ∈ ℕ0
222180addlidi 11402 . . . . . . . . . . . . 13 (0 + 5) = 5
223222oveq2i 7420 . . . . . . . . . . . 12 (1 + (0 + 5)) = (1 + 5)
224223, 181eqtri 2761 . . . . . . . . . . 11 (1 + (0 + 5)) = 6
22525, 25, 221, 164, 224decaddi 12737 . . . . . . . . . 10 ((1 · 11) + (0 + 5)) = 16
22649mulridi 11218 . . . . . . . . . . . . 13 (4 · 1) = 4
227 0p1e1 12334 . . . . . . . . . . . . 13 (0 + 1) = 1
228226, 227oveq12i 7421 . . . . . . . . . . . 12 ((4 · 1) + (0 + 1)) = (4 + 1)
229228, 4eqtri 2761 . . . . . . . . . . 11 ((4 · 1) + (0 + 1)) = 5
230226oveq1i 7419 . . . . . . . . . . . 12 ((4 · 1) + 7) = (4 + 7)
231230, 116eqtri 2761 . . . . . . . . . . 11 ((4 · 1) + 7) = 11
23225, 25, 28, 59, 163, 88, 21, 25, 25, 229, 231decma2c 12730 . . . . . . . . . 10 ((4 · 11) + 7) = 51
23325, 21, 28, 59, 217, 220, 152, 25, 102, 225, 232decmac 12729 . . . . . . . . 9 ((14 · 11) + (0 + 7)) = 161
23436mulridi 11218 . . . . . . . . . . . 12 (6 · 1) = 6
23586addlidi 11402 . . . . . . . . . . . 12 (0 + 1) = 1
236234, 235oveq12i 7421 . . . . . . . . . . 11 ((6 · 1) + (0 + 1)) = (6 + 1)
237 6p1e7 12360 . . . . . . . . . . 11 (6 + 1) = 7
238236, 237eqtri 2761 . . . . . . . . . 10 ((6 · 1) + (0 + 1)) = 7
239 eqid 2733 . . . . . . . . . . . 12 4 = 4
240234, 239oveq12i 7421 . . . . . . . . . . 11 ((6 · 1) + 4) = (6 + 4)
241240, 44eqtri 2761 . . . . . . . . . 10 ((6 · 1) + 4) = 10
24225, 25, 28, 21, 163, 189, 29, 28, 25, 238, 241decma2c 12730 . . . . . . . . 9 ((6 · 11) + 4) = 70
243209, 29, 28, 21, 214, 216, 152, 28, 59, 233, 242decmac 12729 . . . . . . . 8 ((146 · 11) + (0 + 4)) = 1610
244226, 84oveq12i 7421 . . . . . . . . . 10 ((4 · 1) + (0 + 0)) = (4 + 0)
245244, 194eqtri 2761 . . . . . . . . 9 ((4 · 1) + (0 + 0)) = 4
246226oveq1i 7419 . . . . . . . . . . 11 ((4 · 1) + 1) = (4 + 1)
247246, 4eqtri 2761 . . . . . . . . . 10 ((4 · 1) + 1) = 5
248102dec0h 12699 . . . . . . . . . . 11 5 = 05
249248eqcomi 2742 . . . . . . . . . 10 05 = 5
250247, 249eqtr4i 2764 . . . . . . . . 9 ((4 · 1) + 1) = 05
25125, 25, 28, 25, 163, 175, 21, 102, 28, 245, 250decma2c 12730 . . . . . . . 8 ((4 · 11) + 1) = 45
252210, 21, 28, 25, 213, 175, 152, 102, 21, 243, 251decmac 12729 . . . . . . 7 ((1464 · 11) + 1) = 16105
253152, 211, 25, 212, 25, 25, 252, 164decmul1c 12742 . . . . . 6 (14641 · 11) = 161051
254208, 253eqtri 2761 . . . . 5 (11↑5) = 161051
255254eqcomi 2742 . . . 4 161051 = (11↑5)
256149, 255breqtri 5174 . . 3 (9 · (7↑5)) < (11↑5)
257 7re 12305 . . . . . 6 7 ∈ ℝ
258 5nn 12298 . . . . . . 7 5 ∈ ℕ
259258nnzi 12586 . . . . . 6 5 ∈ ℤ
260 7pos 12323 . . . . . 6 0 < 7
261257, 259, 2603pm3.2i 1340 . . . . 5 (7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7)
262 expgt0 14061 . . . . 5 ((7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) → 0 < (7↑5))
263261, 262ax-mp 5 . . . 4 0 < (7↑5)
264 9re 12311 . . . . 5 9 ∈ ℝ
265 1nn 12223 . . . . . . . . 9 1 ∈ ℕ
26625, 265decnncl 12697 . . . . . . . 8 11 ∈ ℕ
267266nnrei 12221 . . . . . . 7 11 ∈ ℝ
268267, 102pm3.2i 472 . . . . . 6 (11 ∈ ℝ ∧ 5 ∈ ℕ0)
269 reexpcl 14044 . . . . . 6 ((11 ∈ ℝ ∧ 5 ∈ ℕ0) → (11↑5) ∈ ℝ)
270268, 269ax-mp 5 . . . . 5 (11↑5) ∈ ℝ
271257, 102pm3.2i 472 . . . . . 6 (7 ∈ ℝ ∧ 5 ∈ ℕ0)
272 reexpcl 14044 . . . . . 6 ((7 ∈ ℝ ∧ 5 ∈ ℕ0) → (7↑5) ∈ ℝ)
273271, 272ax-mp 5 . . . . 5 (7↑5) ∈ ℝ
274264, 270, 273ltmuldivi 12134 . . . 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 11217 . . . . . . 7 (⊤ → 0 ∈ ℝ)
280260a1i 11 . . . . . . 7 (⊤ → 0 < 7)
281279, 280ltned 11350 . . . . . 6 (⊤ → 0 ≠ 7)
282281necomd 2997 . . . . 5 (⊤ → 7 ≠ 0)
283102a1i 11 . . . . 5 (⊤ → 5 ∈ ℕ0)
284277, 278, 282, 283expdivd 14125 . . . 4 (⊤ → ((11 / 7)↑5) = ((11↑5) / (7↑5)))
285284eqcomd 2739 . . 3 (⊤ → ((11↑5) / (7↑5)) = ((11 / 7)↑5))
286285mptru 1549 . 2 ((11↑5) / (7↑5)) = ((11 / 7)↑5)
287276, 286breqtri 5174 1 9 < ((11 / 7)↑5)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  w3a 1088   = wceq 1542  wtru 1543  wcel 2107   class class class wbr 5149  (class class class)co 7409  cc 11108  cr 11109  0cc0 11110  1c1 11111   + caddc 11113   · cmul 11115   < clt 11248   / cdiv 11871  2c2 12267  3c3 12268  4c4 12269  5c5 12270  6c6 12271  7c7 12272  8c8 12273  9c9 12274  0cn0 12472  cz 12558  cdc 12677  cexp 14027
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-rp 12975  df-seq 13967  df-exp 14028
This theorem is referenced by:  3lexlogpow5ineq4  40921
  Copyright terms: Public domain W3C validator