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 41227
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 2730 . . . . . . . . . 10 5 = 5
2 2p2e4 12353 . . . . . . . . . . . 12 (2 + 2) = 4
32oveq1i 7423 . . . . . . . . . . 11 ((2 + 2) + 1) = (4 + 1)
4 4p1e5 12364 . . . . . . . . . . 11 (4 + 1) = 5
53, 4eqtri 2758 . . . . . . . . . 10 ((2 + 2) + 1) = 5
61, 5eqtr4i 2761 . . . . . . . . 9 5 = ((2 + 2) + 1)
76oveq2i 7424 . . . . . . . 8 (7↑5) = (7↑((2 + 2) + 1))
8 7cn 12312 . . . . . . . . . 10 7 ∈ ℂ
9 2nn0 12495 . . . . . . . . . . 11 2 ∈ ℕ0
109, 9nn0addcli 12515 . . . . . . . . . 10 (2 + 2) ∈ ℕ0
118, 10pm3.2i 469 . . . . . . . . 9 (7 ∈ ℂ ∧ (2 + 2) ∈ ℕ0)
12 expp1 14040 . . . . . . . . 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 1337 . . . . . . . . . . 11 (7 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
15 expadd 14076 . . . . . . . . . . 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 14150 . . . . . . . . . . . . 13 (7↑2) = (7 · 7)
18 7t7e49 12797 . . . . . . . . . . . . 13 (7 · 7) = 49
1917, 18eqtri 2758 . . . . . . . . . . . 12 (7↑2) = 49
2019, 19oveq12i 7425 . . . . . . . . . . 11 ((7↑2) · (7↑2)) = (49 · 49)
21 4nn0 12497 . . . . . . . . . . . . 13 4 ∈ ℕ0
22 9nn0 12502 . . . . . . . . . . . . 13 9 ∈ ℕ0
2321, 22deccl 12698 . . . . . . . . . . . 12 49 ∈ ℕ0
24 eqid 2730 . . . . . . . . . . . 12 49 = 49
25 1nn0 12494 . . . . . . . . . . . 12 1 ∈ ℕ0
2621, 21deccl 12698 . . . . . . . . . . . 12 44 ∈ ℕ0
27 eqid 2730 . . . . . . . . . . . . 13 44 = 44
28 0nn0 12493 . . . . . . . . . . . . 13 0 ∈ ℕ0
29 6nn0 12499 . . . . . . . . . . . . . 14 6 ∈ ℕ0
3021, 21nn0addcli 12515 . . . . . . . . . . . . . 14 (4 + 4) ∈ ℕ0
31 4t4e16 12782 . . . . . . . . . . . . . 14 (4 · 4) = 16
32 1p1e2 12343 . . . . . . . . . . . . . 14 (1 + 1) = 2
33 4p4e8 12373 . . . . . . . . . . . . . . . 16 (4 + 4) = 8
3433oveq2i 7424 . . . . . . . . . . . . . . 15 (6 + (4 + 4)) = (6 + 8)
35 8cn 12315 . . . . . . . . . . . . . . . 16 8 ∈ ℂ
36 6cn 12309 . . . . . . . . . . . . . . . 16 6 ∈ ℂ
37 8p6e14 12767 . . . . . . . . . . . . . . . 16 (8 + 6) = 14
3835, 36, 37addcomli 11412 . . . . . . . . . . . . . . 15 (6 + 8) = 14
3934, 38eqtri 2758 . . . . . . . . . . . . . 14 (6 + (4 + 4)) = 14
4025, 29, 30, 31, 32, 21, 39decaddci 12744 . . . . . . . . . . . . 13 ((4 · 4) + (4 + 4)) = 24
41 3nn0 12496 . . . . . . . . . . . . . 14 3 ∈ ℕ0
42 9t4e36 12807 . . . . . . . . . . . . . 14 (9 · 4) = 36
43 3p1e4 12363 . . . . . . . . . . . . . 14 (3 + 1) = 4
44 6p4e10 12755 . . . . . . . . . . . . . 14 (6 + 4) = 10
4541, 29, 21, 42, 43, 44decaddci2 12745 . . . . . . . . . . . . 13 ((9 · 4) + 4) = 40
4621, 22, 21, 21, 24, 27, 21, 28, 21, 40, 45decmac 12735 . . . . . . . . . . . 12 ((49 · 4) + 44) = 240
47 8nn0 12501 . . . . . . . . . . . . 13 8 ∈ ℕ0
48 9cn 12318 . . . . . . . . . . . . . . 15 9 ∈ ℂ
49 4cn 12303 . . . . . . . . . . . . . . 15 4 ∈ ℂ
5048, 49, 42mulcomli 11229 . . . . . . . . . . . . . 14 (4 · 9) = 36
5141, 29, 47, 50, 43, 21, 38decaddci 12744 . . . . . . . . . . . . 13 ((4 · 9) + 8) = 44
52 9t9e81 12812 . . . . . . . . . . . . 13 (9 · 9) = 81
5322, 21, 22, 24, 25, 47, 51, 52decmul1c 12748 . . . . . . . . . . . 12 (49 · 9) = 441
5423, 21, 22, 24, 25, 26, 46, 53decmul2c 12749 . . . . . . . . . . 11 (49 · 49) = 2401
5520, 54eqtri 2758 . . . . . . . . . 10 ((7↑2) · (7↑2)) = 2401
5616, 55eqtri 2758 . . . . . . . . 9 (7↑(2 + 2)) = 2401
5756oveq1i 7423 . . . . . . . 8 ((7↑(2 + 2)) · 7) = (2401 · 7)
587, 13, 573eqtri 2762 . . . . . . 7 (7↑5) = (2401 · 7)
59 7nn0 12500 . . . . . . . 8 7 ∈ ℕ0
609, 21deccl 12698 . . . . . . . . 9 24 ∈ ℕ0
6160, 28deccl 12698 . . . . . . . 8 240 ∈ ℕ0
62 eqid 2730 . . . . . . . 8 2401 = 2401
6325, 29deccl 12698 . . . . . . . . . 10 16 ∈ ℕ0
6463, 47deccl 12698 . . . . . . . . 9 168 ∈ ℕ0
65 eqid 2730 . . . . . . . . . 10 240 = 240
66 eqid 2730 . . . . . . . . . . . 12 24 = 24
67 2cn 12293 . . . . . . . . . . . . . 14 2 ∈ ℂ
68 7t2e14 12792 . . . . . . . . . . . . . 14 (7 · 2) = 14
698, 67, 68mulcomli 11229 . . . . . . . . . . . . 13 (2 · 7) = 14
70 4p2e6 12371 . . . . . . . . . . . . 13 (4 + 2) = 6
7125, 21, 9, 69, 70decaddi 12743 . . . . . . . . . . . 12 ((2 · 7) + 2) = 16
72 7t4e28 12794 . . . . . . . . . . . . 13 (7 · 4) = 28
738, 49, 72mulcomli 11229 . . . . . . . . . . . 12 (4 · 7) = 28
7459, 9, 21, 66, 47, 9, 71, 73decmul1c 12748 . . . . . . . . . . 11 (24 · 7) = 168
7535addridi 11407 . . . . . . . . . . 11 (8 + 0) = 8
7663, 47, 28, 74, 75decaddi 12743 . . . . . . . . . 10 ((24 · 7) + 0) = 168
77 0cn 11212 . . . . . . . . . . 11 0 ∈ ℂ
788mul01i 11410 . . . . . . . . . . . 12 (7 · 0) = 0
7928dec0h 12705 . . . . . . . . . . . . 13 0 = 00
8079eqcomi 2739 . . . . . . . . . . . 12 00 = 0
8178, 80eqtr4i 2761 . . . . . . . . . . 11 (7 · 0) = 00
828, 77, 81mulcomli 11229 . . . . . . . . . 10 (0 · 7) = 00
8359, 60, 28, 65, 28, 28, 76, 82decmul1c 12748 . . . . . . . . 9 (240 · 7) = 1680
84 00id 11395 . . . . . . . . 9 (0 + 0) = 0
8564, 28, 28, 83, 84decaddi 12743 . . . . . . . 8 ((240 · 7) + 0) = 1680
86 ax-1cn 11172 . . . . . . . . 9 1 ∈ ℂ
878mulridi 11224 . . . . . . . . . 10 (7 · 1) = 7
8859dec0h 12705 . . . . . . . . . . 11 7 = 07
8988eqcomi 2739 . . . . . . . . . 10 07 = 7
9087, 89eqtr4i 2761 . . . . . . . . 9 (7 · 1) = 07
918, 86, 90mulcomli 11229 . . . . . . . 8 (1 · 7) = 07
9259, 61, 25, 62, 59, 28, 85, 91decmul1c 12748 . . . . . . 7 (2401 · 7) = 16807
9358, 92eqtri 2758 . . . . . 6 (7↑5) = 16807
9493oveq2i 7424 . . . . 5 (9 · (7↑5)) = (9 · 16807)
9564, 28deccl 12698 . . . . . . . . 9 1680 ∈ ℕ0
9695, 59deccl 12698 . . . . . . . 8 16807 ∈ ℕ0
9796nn0cni 12490 . . . . . . 7 16807 ∈ ℂ
9848, 97mulcomi 11228 . . . . . 6 (9 · 16807) = (16807 · 9)
99 eqid 2730 . . . . . . . 8 16807 = 16807
100 eqid 2730 . . . . . . . . 9 1680 = 1680
10129dec0h 12705 . . . . . . . . 9 6 = 06
102 5nn0 12498 . . . . . . . . . . . 12 5 ∈ ℕ0
10325, 102deccl 12698 . . . . . . . . . . 11 15 ∈ ℕ0
104103, 25deccl 12698 . . . . . . . . . 10 151 ∈ ℕ0
105 eqid 2730 . . . . . . . . . . 11 168 = 168
106 eqid 2730 . . . . . . . . . . . 12 16 = 16
10748mullidi 11225 . . . . . . . . . . . . . 14 (1 · 9) = 9
10836addlidi 11408 . . . . . . . . . . . . . 14 (0 + 6) = 6
109107, 108oveq12i 7425 . . . . . . . . . . . . 13 ((1 · 9) + (0 + 6)) = (9 + 6)
110 9p6e15 12774 . . . . . . . . . . . . 13 (9 + 6) = 15
111109, 110eqtri 2758 . . . . . . . . . . . 12 ((1 · 9) + (0 + 6)) = 15
112 9t6e54 12809 . . . . . . . . . . . . . 14 (9 · 6) = 54
11348, 36, 112mulcomli 11229 . . . . . . . . . . . . 13 (6 · 9) = 54
114 5p1e6 12365 . . . . . . . . . . . . 13 (5 + 1) = 6
115 7p4e11 12759 . . . . . . . . . . . . . 14 (7 + 4) = 11
1168, 49, 115addcomli 11412 . . . . . . . . . . . . 13 (4 + 7) = 11
117102, 21, 59, 113, 114, 25, 116decaddci 12744 . . . . . . . . . . . 12 ((6 · 9) + 7) = 61
11825, 29, 28, 59, 106, 88, 22, 25, 29, 111, 117decmac 12735 . . . . . . . . . . 11 ((16 · 9) + 7) = 151
119 9t8e72 12811 . . . . . . . . . . . 12 (9 · 8) = 72
12048, 35, 119mulcomli 11229 . . . . . . . . . . 11 (8 · 9) = 72
12122, 63, 47, 105, 9, 59, 118, 120decmul1c 12748 . . . . . . . . . 10 (168 · 9) = 1512
12267addridi 11407 . . . . . . . . . 10 (2 + 0) = 2
123104, 9, 28, 121, 122decaddi 12743 . . . . . . . . 9 ((168 · 9) + 0) = 1512
12448mul02i 11409 . . . . . . . . . . 11 (0 · 9) = 0
125124oveq1i 7423 . . . . . . . . . 10 ((0 · 9) + 6) = (0 + 6)
126125, 108eqtri 2758 . . . . . . . . 9 ((0 · 9) + 6) = 6
12764, 28, 28, 29, 100, 101, 22, 123, 126decma 12734 . . . . . . . 8 ((1680 · 9) + 6) = 15126
128 9t7e63 12810 . . . . . . . . 9 (9 · 7) = 63
12948, 8, 128mulcomli 11229 . . . . . . . 8 (7 · 9) = 63
13022, 95, 59, 99, 41, 29, 127, 129decmul1c 12748 . . . . . . 7 (16807 · 9) = 151263
131104, 9deccl 12698 . . . . . . . . 9 1512 ∈ ℕ0
132131, 29deccl 12698 . . . . . . . 8 15126 ∈ ℕ0
13363, 25deccl 12698 . . . . . . . . . 10 161 ∈ ℕ0
134133, 28deccl 12698 . . . . . . . . 9 1610 ∈ ℕ0
135134, 102deccl 12698 . . . . . . . 8 16105 ∈ ℕ0
136 3lt10 12820 . . . . . . . 8 3 < 10
137 6lt10 12817 . . . . . . . . 9 6 < 10
138 2lt10 12821 . . . . . . . . . 10 2 < 10
139 1lt10 12822 . . . . . . . . . . 11 1 < 10
140 6nn 12307 . . . . . . . . . . . 12 6 ∈ ℕ
141 5lt6 12399 . . . . . . . . . . . 12 5 < 6
14225, 102, 140, 141declt 12711 . . . . . . . . . . 11 15 < 16
143103, 63, 25, 25, 139, 142decltc 12712 . . . . . . . . . 10 151 < 161
144104, 133, 9, 28, 138, 143decltc 12712 . . . . . . . . 9 1512 < 1610
145131, 134, 29, 102, 137, 144decltc 12712 . . . . . . . 8 15126 < 16105
146132, 135, 41, 25, 136, 145decltc 12712 . . . . . . 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 2739 . . . . . . . 8 5 = (4 + 1)
151150oveq2i 7424 . . . . . . 7 (11↑5) = (11↑(4 + 1))
15225, 25deccl 12698 . . . . . . . . . . 11 11 ∈ ℕ0
153152nn0cni 12490 . . . . . . . . . 10 11 ∈ ℂ
154153, 21pm3.2i 469 . . . . . . . . 9 (11 ∈ ℂ ∧ 4 ∈ ℕ0)
155 expp1 14040 . . . . . . . . 9 ((11 ∈ ℂ ∧ 4 ∈ ℕ0) → (11↑(4 + 1)) = ((11↑4) · 11))
156154, 155ax-mp 5 . . . . . . . 8 (11↑(4 + 1)) = ((11↑4) · 11)
1572eqcomi 2739 . . . . . . . . . . 11 4 = (2 + 2)
158157oveq2i 7424 . . . . . . . . . 10 (11↑4) = (11↑(2 + 2))
159153, 9, 93pm3.2i 1337 . . . . . . . . . . . 12 (11 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0)
160 expadd 14076 . . . . . . . . . . . 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 14150 . . . . . . . . . . . . . 14 (11↑2) = (11 · 11)
163 eqid 2730 . . . . . . . . . . . . . . 15 11 = 11
164153mullidi 11225 . . . . . . . . . . . . . . . 16 (1 · 11) = 11
16525, 25, 32, 164decsuc 12714 . . . . . . . . . . . . . . 15 ((1 · 11) + 1) = 12
166152, 25, 25, 163, 25, 25, 165, 164decmul1c 12748 . . . . . . . . . . . . . 14 (11 · 11) = 121
167162, 166eqtri 2758 . . . . . . . . . . . . 13 (11↑2) = 121
168167, 167oveq12i 7425 . . . . . . . . . . . 12 ((11↑2) · (11↑2)) = (121 · 121)
16925, 9deccl 12698 . . . . . . . . . . . . . 14 12 ∈ ℕ0
170169, 25deccl 12698 . . . . . . . . . . . . 13 121 ∈ ℕ0
171 eqid 2730 . . . . . . . . . . . . 13 121 = 121
172 eqid 2730 . . . . . . . . . . . . . 14 12 = 12
173170nn0cni 12490 . . . . . . . . . . . . . . . 16 121 ∈ ℂ
174173mullidi 11225 . . . . . . . . . . . . . . 15 (1 · 121) = 121
17525dec0h 12705 . . . . . . . . . . . . . . . 16 1 = 01
17667addlidi 11408 . . . . . . . . . . . . . . . 16 (0 + 2) = 2
17749, 86, 4addcomli 11412 . . . . . . . . . . . . . . . 16 (1 + 4) = 5
17828, 25, 9, 21, 175, 66, 176, 177decadd 12737 . . . . . . . . . . . . . . 15 (1 + 24) = 25
17925, 9, 9, 172, 2decaddi 12743 . . . . . . . . . . . . . . 15 (12 + 2) = 14
180 5cn 12306 . . . . . . . . . . . . . . . 16 5 ∈ ℂ
181180, 86, 114addcomli 11412 . . . . . . . . . . . . . . 15 (1 + 5) = 6
182169, 25, 9, 102, 174, 178, 179, 181decadd 12737 . . . . . . . . . . . . . 14 ((1 · 121) + (1 + 24)) = 146
1839dec0h 12705 . . . . . . . . . . . . . . 15 2 = 02
18428, 28nn0addcli 12515 . . . . . . . . . . . . . . . 16 (0 + 0) ∈ ℕ0
185 2t1e2 12381 . . . . . . . . . . . . . . . . . . 19 (2 · 1) = 2
186185oveq1i 7423 . . . . . . . . . . . . . . . . . 18 ((2 · 1) + 0) = (2 + 0)
187186, 122eqtri 2758 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 0) = 2
188 2t2e4 12382 . . . . . . . . . . . . . . . . . 18 (2 · 2) = 4
18921dec0h 12705 . . . . . . . . . . . . . . . . . . 19 4 = 04
190189eqcomi 2739 . . . . . . . . . . . . . . . . . 18 04 = 4
191188, 190eqtr4i 2761 . . . . . . . . . . . . . . . . 17 (2 · 2) = 04
1929, 25, 9, 172, 21, 28, 187, 191decmul2c 12749 . . . . . . . . . . . . . . . 16 (2 · 12) = 24
19384oveq2i 7424 . . . . . . . . . . . . . . . . 17 (4 + (0 + 0)) = (4 + 0)
19449addridi 11407 . . . . . . . . . . . . . . . . 17 (4 + 0) = 4
195193, 194eqtri 2758 . . . . . . . . . . . . . . . 16 (4 + (0 + 0)) = 4
1969, 21, 184, 192, 195decaddi 12743 . . . . . . . . . . . . . . 15 ((2 · 12) + (0 + 0)) = 24
197185oveq1i 7423 . . . . . . . . . . . . . . . . 17 ((2 · 1) + 2) = (2 + 2)
198197, 2eqtri 2758 . . . . . . . . . . . . . . . 16 ((2 · 1) + 2) = 4
199198, 190eqtr4i 2761 . . . . . . . . . . . . . . 15 ((2 · 1) + 2) = 04
200169, 25, 28, 9, 171, 183, 9, 21, 28, 196, 199decma2c 12736 . . . . . . . . . . . . . 14 ((2 · 121) + 2) = 244
20125, 9, 25, 9, 172, 172, 170, 21, 60, 182, 200decmac 12735 . . . . . . . . . . . . 13 ((12 · 121) + 12) = 1464
202170, 169, 25, 171, 25, 169, 201, 174decmul1c 12748 . . . . . . . . . . . 12 (121 · 121) = 14641
203168, 202eqtri 2758 . . . . . . . . . . 11 ((11↑2) · (11↑2)) = 14641
204161, 203eqtri 2758 . . . . . . . . . 10 (11↑(2 + 2)) = 14641
205158, 204eqtri 2758 . . . . . . . . 9 (11↑4) = 14641
206205oveq1i 7423 . . . . . . . 8 ((11↑4) · 11) = (14641 · 11)
207156, 206eqtri 2758 . . . . . . 7 (11↑(4 + 1)) = (14641 · 11)
208151, 207eqtri 2758 . . . . . 6 (11↑5) = (14641 · 11)
20925, 21deccl 12698 . . . . . . . . 9 14 ∈ ℕ0
210209, 29deccl 12698 . . . . . . . 8 146 ∈ ℕ0
211210, 21deccl 12698 . . . . . . 7 1464 ∈ ℕ0
212 eqid 2730 . . . . . . 7 14641 = 14641
213 eqid 2730 . . . . . . . 8 1464 = 1464
214 eqid 2730 . . . . . . . . 9 146 = 146
215194, 190eqtr4i 2761 . . . . . . . . . 10 (4 + 0) = 04
21649, 77, 215addcomli 11412 . . . . . . . . 9 (0 + 4) = 04
217 eqid 2730 . . . . . . . . . 10 14 = 14
2188addridi 11407 . . . . . . . . . . . 12 (7 + 0) = 7
219218, 89eqtr4i 2761 . . . . . . . . . . 11 (7 + 0) = 07
2208, 77, 219addcomli 11412 . . . . . . . . . 10 (0 + 7) = 07
22128, 102nn0addcli 12515 . . . . . . . . . . 11 (0 + 5) ∈ ℕ0
222180addlidi 11408 . . . . . . . . . . . . 13 (0 + 5) = 5
223222oveq2i 7424 . . . . . . . . . . . 12 (1 + (0 + 5)) = (1 + 5)
224223, 181eqtri 2758 . . . . . . . . . . 11 (1 + (0 + 5)) = 6
22525, 25, 221, 164, 224decaddi 12743 . . . . . . . . . 10 ((1 · 11) + (0 + 5)) = 16
22649mulridi 11224 . . . . . . . . . . . . 13 (4 · 1) = 4
227 0p1e1 12340 . . . . . . . . . . . . 13 (0 + 1) = 1
228226, 227oveq12i 7425 . . . . . . . . . . . 12 ((4 · 1) + (0 + 1)) = (4 + 1)
229228, 4eqtri 2758 . . . . . . . . . . 11 ((4 · 1) + (0 + 1)) = 5
230226oveq1i 7423 . . . . . . . . . . . 12 ((4 · 1) + 7) = (4 + 7)
231230, 116eqtri 2758 . . . . . . . . . . 11 ((4 · 1) + 7) = 11
23225, 25, 28, 59, 163, 88, 21, 25, 25, 229, 231decma2c 12736 . . . . . . . . . 10 ((4 · 11) + 7) = 51
23325, 21, 28, 59, 217, 220, 152, 25, 102, 225, 232decmac 12735 . . . . . . . . 9 ((14 · 11) + (0 + 7)) = 161
23436mulridi 11224 . . . . . . . . . . . 12 (6 · 1) = 6
23586addlidi 11408 . . . . . . . . . . . 12 (0 + 1) = 1
236234, 235oveq12i 7425 . . . . . . . . . . 11 ((6 · 1) + (0 + 1)) = (6 + 1)
237 6p1e7 12366 . . . . . . . . . . 11 (6 + 1) = 7
238236, 237eqtri 2758 . . . . . . . . . 10 ((6 · 1) + (0 + 1)) = 7
239 eqid 2730 . . . . . . . . . . . 12 4 = 4
240234, 239oveq12i 7425 . . . . . . . . . . 11 ((6 · 1) + 4) = (6 + 4)
241240, 44eqtri 2758 . . . . . . . . . 10 ((6 · 1) + 4) = 10
24225, 25, 28, 21, 163, 189, 29, 28, 25, 238, 241decma2c 12736 . . . . . . . . 9 ((6 · 11) + 4) = 70
243209, 29, 28, 21, 214, 216, 152, 28, 59, 233, 242decmac 12735 . . . . . . . 8 ((146 · 11) + (0 + 4)) = 1610
244226, 84oveq12i 7425 . . . . . . . . . 10 ((4 · 1) + (0 + 0)) = (4 + 0)
245244, 194eqtri 2758 . . . . . . . . 9 ((4 · 1) + (0 + 0)) = 4
246226oveq1i 7423 . . . . . . . . . . 11 ((4 · 1) + 1) = (4 + 1)
247246, 4eqtri 2758 . . . . . . . . . 10 ((4 · 1) + 1) = 5
248102dec0h 12705 . . . . . . . . . . 11 5 = 05
249248eqcomi 2739 . . . . . . . . . 10 05 = 5
250247, 249eqtr4i 2761 . . . . . . . . 9 ((4 · 1) + 1) = 05
25125, 25, 28, 25, 163, 175, 21, 102, 28, 245, 250decma2c 12736 . . . . . . . 8 ((4 · 11) + 1) = 45
252210, 21, 28, 25, 213, 175, 152, 102, 21, 243, 251decmac 12735 . . . . . . 7 ((1464 · 11) + 1) = 16105
253152, 211, 25, 212, 25, 25, 252, 164decmul1c 12748 . . . . . 6 (14641 · 11) = 161051
254208, 253eqtri 2758 . . . . 5 (11↑5) = 161051
255254eqcomi 2739 . . . 4 161051 = (11↑5)
256149, 255breqtri 5174 . . 3 (9 · (7↑5)) < (11↑5)
257 7re 12311 . . . . . 6 7 ∈ ℝ
258 5nn 12304 . . . . . . 7 5 ∈ ℕ
259258nnzi 12592 . . . . . 6 5 ∈ ℤ
260 7pos 12329 . . . . . 6 0 < 7
261257, 259, 2603pm3.2i 1337 . . . . 5 (7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7)
262 expgt0 14067 . . . . 5 ((7 ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) → 0 < (7↑5))
263261, 262ax-mp 5 . . . 4 0 < (7↑5)
264 9re 12317 . . . . 5 9 ∈ ℝ
265 1nn 12229 . . . . . . . . 9 1 ∈ ℕ
26625, 265decnncl 12703 . . . . . . . 8 11 ∈ ℕ
267266nnrei 12227 . . . . . . 7 11 ∈ ℝ
268267, 102pm3.2i 469 . . . . . 6 (11 ∈ ℝ ∧ 5 ∈ ℕ0)
269 reexpcl 14050 . . . . . 6 ((11 ∈ ℝ ∧ 5 ∈ ℕ0) → (11↑5) ∈ ℝ)
270268, 269ax-mp 5 . . . . 5 (11↑5) ∈ ℝ
271257, 102pm3.2i 469 . . . . . 6 (7 ∈ ℝ ∧ 5 ∈ ℕ0)
272 reexpcl 14050 . . . . . 6 ((7 ∈ ℝ ∧ 5 ∈ ℕ0) → (7↑5) ∈ ℝ)
273271, 272ax-mp 5 . . . . 5 (7↑5) ∈ ℝ
274264, 270, 273ltmuldivi 12140 . . . 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 11223 . . . . . . 7 (⊤ → 0 ∈ ℝ)
280260a1i 11 . . . . . . 7 (⊤ → 0 < 7)
281279, 280ltned 11356 . . . . . 6 (⊤ → 0 ≠ 7)
282281necomd 2994 . . . . 5 (⊤ → 7 ≠ 0)
283102a1i 11 . . . . 5 (⊤ → 5 ∈ ℕ0)
284277, 278, 282, 283expdivd 14131 . . . 4 (⊤ → ((11 / 7)↑5) = ((11↑5) / (7↑5)))
285284eqcomd 2736 . . 3 (⊤ → ((11↑5) / (7↑5)) = ((11 / 7)↑5))
286285mptru 1546 . 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 394  w3a 1085   = wceq 1539  wtru 1540  wcel 2104   class class class wbr 5149  (class class class)co 7413  cc 11112  cr 11113  0cc0 11114  1c1 11115   + caddc 11117   · cmul 11119   < clt 11254   / cdiv 11877  2c2 12273  3c3 12274  4c4 12275  5c5 12276  6c6 12277  7c7 12278  8c8 12279  9c9 12280  0cn0 12478  cz 12564  cdc 12683  cexp 14033
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  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 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11452  df-neg 11453  df-div 11878  df-nn 12219  df-2 12281  df-3 12282  df-4 12283  df-5 12284  df-6 12285  df-7 12286  df-8 12287  df-9 12288  df-n0 12479  df-z 12565  df-dec 12684  df-uz 12829  df-rp 12981  df-seq 13973  df-exp 14034
This theorem is referenced by:  3lexlogpow5ineq4  41229
  Copyright terms: Public domain W3C validator