Proof of Theorem 3lexlogpow5ineq1
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . . . . . . 10
⊢ 5 =
5 |
2 | | 2p2e4 12096 |
. . . . . . . . . . . 12
⊢ (2 + 2) =
4 |
3 | 2 | oveq1i 7278 |
. . . . . . . . . . 11
⊢ ((2 + 2)
+ 1) = (4 + 1) |
4 | | 4p1e5 12107 |
. . . . . . . . . . 11
⊢ (4 + 1) =
5 |
5 | 3, 4 | eqtri 2766 |
. . . . . . . . . 10
⊢ ((2 + 2)
+ 1) = 5 |
6 | 1, 5 | eqtr4i 2769 |
. . . . . . . . 9
⊢ 5 = ((2 +
2) + 1) |
7 | 6 | oveq2i 7279 |
. . . . . . . 8
⊢
(7↑5) = (7↑((2 + 2) + 1)) |
8 | | 7cn 12055 |
. . . . . . . . . 10
⊢ 7 ∈
ℂ |
9 | | 2nn0 12238 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
10 | 9, 9 | nn0addcli 12258 |
. . . . . . . . . 10
⊢ (2 + 2)
∈ ℕ0 |
11 | 8, 10 | pm3.2i 471 |
. . . . . . . . 9
⊢ (7 ∈
ℂ ∧ (2 + 2) ∈ ℕ0) |
12 | | expp1 13777 |
. . . . . . . . 9
⊢ ((7
∈ ℂ ∧ (2 + 2) ∈ ℕ0) → (7↑((2 +
2) + 1)) = ((7↑(2 + 2)) · 7)) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . 8
⊢
(7↑((2 + 2) + 1)) = ((7↑(2 + 2)) · 7) |
14 | 8, 9, 9 | 3pm3.2i 1338 |
. . . . . . . . . . 11
⊢ (7 ∈
ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈
ℕ0) |
15 | | expadd 13813 |
. . . . . . . . . . 11
⊢ ((7
∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈
ℕ0) → (7↑(2 + 2)) = ((7↑2) ·
(7↑2))) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . 10
⊢
(7↑(2 + 2)) = ((7↑2) · (7↑2)) |
17 | 8 | sqvali 13885 |
. . . . . . . . . . . . 13
⊢
(7↑2) = (7 · 7) |
18 | | 7t7e49 12539 |
. . . . . . . . . . . . 13
⊢ (7
· 7) = ;49 |
19 | 17, 18 | eqtri 2766 |
. . . . . . . . . . . 12
⊢
(7↑2) = ;49 |
20 | 19, 19 | oveq12i 7280 |
. . . . . . . . . . 11
⊢
((7↑2) · (7↑2)) = (;49 · ;49) |
21 | | 4nn0 12240 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℕ0 |
22 | | 9nn0 12245 |
. . . . . . . . . . . . 13
⊢ 9 ∈
ℕ0 |
23 | 21, 22 | deccl 12440 |
. . . . . . . . . . . 12
⊢ ;49 ∈
ℕ0 |
24 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ;49 = ;49 |
25 | | 1nn0 12237 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 |
26 | 21, 21 | deccl 12440 |
. . . . . . . . . . . 12
⊢ ;44 ∈
ℕ0 |
27 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ;44 = ;44 |
28 | | 0nn0 12236 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
29 | | 6nn0 12242 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℕ0 |
30 | 21, 21 | nn0addcli 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 |
34 | 33 | oveq2i 7279 |
. . . . . . . . . . . . . . 15
⊢ (6 + (4 +
4)) = (6 + 8) |
35 | | 8cn 12058 |
. . . . . . . . . . . . . . . 16
⊢ 8 ∈
ℂ |
36 | | 6cn 12052 |
. . . . . . . . . . . . . . . 16
⊢ 6 ∈
ℂ |
37 | | 8p6e14 12509 |
. . . . . . . . . . . . . . . 16
⊢ (8 + 6) =
;14 |
38 | 35, 36, 37 | addcomli 11155 |
. . . . . . . . . . . . . . 15
⊢ (6 + 8) =
;14 |
39 | 34, 38 | eqtri 2766 |
. . . . . . . . . . . . . 14
⊢ (6 + (4 +
4)) = ;14 |
40 | 25, 29, 30, 31, 32, 21, 39 | decaddci 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 |
45 | 41, 29, 21, 42, 43, 44 | decaddci2 12487 |
. . . . . . . . . . . . 13
⊢ ((9
· 4) + 4) = ;40 |
46 | 21, 22, 21, 21, 24, 27, 21, 28, 21, 40, 45 | decmac 12477 |
. . . . . . . . . . . 12
⊢ ((;49 · 4) + ;44) = ;;240 |
47 | | 8nn0 12244 |
. . . . . . . . . . . . 13
⊢ 8 ∈
ℕ0 |
48 | | 9cn 12061 |
. . . . . . . . . . . . . . 15
⊢ 9 ∈
ℂ |
49 | | 4cn 12046 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℂ |
50 | 48, 49, 42 | mulcomli 10972 |
. . . . . . . . . . . . . 14
⊢ (4
· 9) = ;36 |
51 | 41, 29, 47, 50, 43, 21, 38 | decaddci 12486 |
. . . . . . . . . . . . 13
⊢ ((4
· 9) + 8) = ;44 |
52 | | 9t9e81 12554 |
. . . . . . . . . . . . 13
⊢ (9
· 9) = ;81 |
53 | 22, 21, 22, 24, 25, 47, 51, 52 | decmul1c 12490 |
. . . . . . . . . . . 12
⊢ (;49 · 9) = ;;441 |
54 | 23, 21, 22, 24, 25, 26, 46, 53 | decmul2c 12491 |
. . . . . . . . . . 11
⊢ (;49 · ;49) = ;;;2401 |
55 | 20, 54 | eqtri 2766 |
. . . . . . . . . 10
⊢
((7↑2) · (7↑2)) = ;;;2401 |
56 | 16, 55 | eqtri 2766 |
. . . . . . . . 9
⊢
(7↑(2 + 2)) = ;;;2401 |
57 | 56 | oveq1i 7278 |
. . . . . . . 8
⊢
((7↑(2 + 2)) · 7) = (;;;2401 · 7) |
58 | 7, 13, 57 | 3eqtri 2770 |
. . . . . . 7
⊢
(7↑5) = (;;;2401 · 7) |
59 | | 7nn0 12243 |
. . . . . . . 8
⊢ 7 ∈
ℕ0 |
60 | 9, 21 | deccl 12440 |
. . . . . . . . 9
⊢ ;24 ∈
ℕ0 |
61 | 60, 28 | deccl 12440 |
. . . . . . . 8
⊢ ;;240 ∈ ℕ0 |
62 | | eqid 2738 |
. . . . . . . 8
⊢ ;;;2401 =
;;;2401 |
63 | 25, 29 | deccl 12440 |
. . . . . . . . . 10
⊢ ;16 ∈
ℕ0 |
64 | 63, 47 | deccl 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 |
69 | 8, 67, 68 | mulcomli 10972 |
. . . . . . . . . . . . 13
⊢ (2
· 7) = ;14 |
70 | | 4p2e6 12114 |
. . . . . . . . . . . . 13
⊢ (4 + 2) =
6 |
71 | 25, 21, 9, 69, 70 | decaddi 12485 |
. . . . . . . . . . . 12
⊢ ((2
· 7) + 2) = ;16 |
72 | | 7t4e28 12536 |
. . . . . . . . . . . . 13
⊢ (7
· 4) = ;28 |
73 | 8, 49, 72 | mulcomli 10972 |
. . . . . . . . . . . 12
⊢ (4
· 7) = ;28 |
74 | 59, 9, 21, 66, 47, 9, 71, 73 | decmul1c 12490 |
. . . . . . . . . . 11
⊢ (;24 · 7) = ;;168 |
75 | 35 | addid1i 11150 |
. . . . . . . . . . 11
⊢ (8 + 0) =
8 |
76 | 63, 47, 28, 74, 75 | decaddi 12485 |
. . . . . . . . . 10
⊢ ((;24 · 7) + 0) = ;;168 |
77 | | 0cn 10955 |
. . . . . . . . . . 11
⊢ 0 ∈
ℂ |
78 | 8 | mul01i 11153 |
. . . . . . . . . . . 12
⊢ (7
· 0) = 0 |
79 | 28 | dec0h 12447 |
. . . . . . . . . . . . 13
⊢ 0 = ;00 |
80 | 79 | eqcomi 2747 |
. . . . . . . . . . . 12
⊢ ;00 = 0 |
81 | 78, 80 | eqtr4i 2769 |
. . . . . . . . . . 11
⊢ (7
· 0) = ;00 |
82 | 8, 77, 81 | mulcomli 10972 |
. . . . . . . . . 10
⊢ (0
· 7) = ;00 |
83 | 59, 60, 28, 65, 28, 28, 76, 82 | decmul1c 12490 |
. . . . . . . . 9
⊢ (;;240 · 7) = ;;;1680 |
84 | | 00id 11138 |
. . . . . . . . 9
⊢ (0 + 0) =
0 |
85 | 64, 28, 28, 83, 84 | decaddi 12485 |
. . . . . . . 8
⊢ ((;;240 · 7) + 0) = ;;;1680 |
86 | | ax-1cn 10917 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
87 | 8 | mulid1i 10967 |
. . . . . . . . . 10
⊢ (7
· 1) = 7 |
88 | 59 | dec0h 12447 |
. . . . . . . . . . 11
⊢ 7 = ;07 |
89 | 88 | eqcomi 2747 |
. . . . . . . . . 10
⊢ ;07 = 7 |
90 | 87, 89 | eqtr4i 2769 |
. . . . . . . . 9
⊢ (7
· 1) = ;07 |
91 | 8, 86, 90 | mulcomli 10972 |
. . . . . . . 8
⊢ (1
· 7) = ;07 |
92 | 59, 61, 25, 62, 59, 28, 85, 91 | decmul1c 12490 |
. . . . . . 7
⊢ (;;;2401
· 7) = ;;;;16807 |
93 | 58, 92 | eqtri 2766 |
. . . . . 6
⊢
(7↑5) = ;;;;16807 |
94 | 93 | oveq2i 7279 |
. . . . 5
⊢ (9
· (7↑5)) = (9 · ;;;;16807) |
95 | 64, 28 | deccl 12440 |
. . . . . . . . 9
⊢ ;;;1680
∈ ℕ0 |
96 | 95, 59 | deccl 12440 |
. . . . . . . 8
⊢ ;;;;16807 ∈
ℕ0 |
97 | 96 | nn0cni 12233 |
. . . . . . 7
⊢ ;;;;16807 ∈ ℂ |
98 | 48, 97 | mulcomi 10971 |
. . . . . 6
⊢ (9
· ;;;;16807) = (;;;;16807 · 9) |
99 | | eqid 2738 |
. . . . . . . 8
⊢ ;;;;16807 = ;;;;16807 |
100 | | eqid 2738 |
. . . . . . . . 9
⊢ ;;;1680 =
;;;1680 |
101 | 29 | dec0h 12447 |
. . . . . . . . 9
⊢ 6 = ;06 |
102 | | 5nn0 12241 |
. . . . . . . . . . . 12
⊢ 5 ∈
ℕ0 |
103 | 25, 102 | deccl 12440 |
. . . . . . . . . . 11
⊢ ;15 ∈
ℕ0 |
104 | 103, 25 | deccl 12440 |
. . . . . . . . . 10
⊢ ;;151 ∈ ℕ0 |
105 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ;;168 = ;;168 |
106 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ;16 = ;16 |
107 | 48 | mulid2i 10968 |
. . . . . . . . . . . . . 14
⊢ (1
· 9) = 9 |
108 | 36 | addid2i 11151 |
. . . . . . . . . . . . . 14
⊢ (0 + 6) =
6 |
109 | 107, 108 | oveq12i 7280 |
. . . . . . . . . . . . 13
⊢ ((1
· 9) + (0 + 6)) = (9 + 6) |
110 | | 9p6e15 12516 |
. . . . . . . . . . . . 13
⊢ (9 + 6) =
;15 |
111 | 109, 110 | eqtri 2766 |
. . . . . . . . . . . 12
⊢ ((1
· 9) + (0 + 6)) = ;15 |
112 | | 9t6e54 12551 |
. . . . . . . . . . . . . 14
⊢ (9
· 6) = ;54 |
113 | 48, 36, 112 | mulcomli 10972 |
. . . . . . . . . . . . 13
⊢ (6
· 9) = ;54 |
114 | | 5p1e6 12108 |
. . . . . . . . . . . . 13
⊢ (5 + 1) =
6 |
115 | | 7p4e11 12501 |
. . . . . . . . . . . . . 14
⊢ (7 + 4) =
;11 |
116 | 8, 49, 115 | addcomli 11155 |
. . . . . . . . . . . . 13
⊢ (4 + 7) =
;11 |
117 | 102, 21, 59, 113, 114, 25, 116 | decaddci 12486 |
. . . . . . . . . . . 12
⊢ ((6
· 9) + 7) = ;61 |
118 | 25, 29, 28, 59, 106, 88, 22, 25, 29, 111, 117 | decmac 12477 |
. . . . . . . . . . 11
⊢ ((;16 · 9) + 7) = ;;151 |
119 | | 9t8e72 12553 |
. . . . . . . . . . . 12
⊢ (9
· 8) = ;72 |
120 | 48, 35, 119 | mulcomli 10972 |
. . . . . . . . . . 11
⊢ (8
· 9) = ;72 |
121 | 22, 63, 47, 105, 9, 59, 118, 120 | decmul1c 12490 |
. . . . . . . . . 10
⊢ (;;168 · 9) = ;;;1512 |
122 | 67 | addid1i 11150 |
. . . . . . . . . 10
⊢ (2 + 0) =
2 |
123 | 104, 9, 28, 121, 122 | decaddi 12485 |
. . . . . . . . 9
⊢ ((;;168 · 9) + 0) = ;;;1512 |
124 | 48 | mul02i 11152 |
. . . . . . . . . . 11
⊢ (0
· 9) = 0 |
125 | 124 | oveq1i 7278 |
. . . . . . . . . 10
⊢ ((0
· 9) + 6) = (0 + 6) |
126 | 125, 108 | eqtri 2766 |
. . . . . . . . 9
⊢ ((0
· 9) + 6) = 6 |
127 | 64, 28, 28, 29, 100, 101, 22, 123, 126 | decma 12476 |
. . . . . . . 8
⊢ ((;;;1680
· 9) + 6) = ;;;;15126 |
128 | | 9t7e63 12552 |
. . . . . . . . 9
⊢ (9
· 7) = ;63 |
129 | 48, 8, 128 | mulcomli 10972 |
. . . . . . . 8
⊢ (7
· 9) = ;63 |
130 | 22, 95, 59, 99, 41, 29, 127, 129 | decmul1c 12490 |
. . . . . . 7
⊢ (;;;;16807 · 9) = ;;;;;151263 |
131 | 104, 9 | deccl 12440 |
. . . . . . . . 9
⊢ ;;;1512
∈ ℕ0 |
132 | 131, 29 | deccl 12440 |
. . . . . . . 8
⊢ ;;;;15126 ∈
ℕ0 |
133 | 63, 25 | deccl 12440 |
. . . . . . . . . 10
⊢ ;;161 ∈ ℕ0 |
134 | 133, 28 | deccl 12440 |
. . . . . . . . 9
⊢ ;;;1610
∈ ℕ0 |
135 | 134, 102 | deccl 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 |
142 | 25, 102, 140, 141 | declt 12453 |
. . . . . . . . . . 11
⊢ ;15 < ;16 |
143 | 103, 63, 25, 25, 139, 142 | decltc 12454 |
. . . . . . . . . 10
⊢ ;;151 < ;;161 |
144 | 104, 133,
9, 28, 138, 143 | decltc 12454 |
. . . . . . . . 9
⊢ ;;;1512
< ;;;1610 |
145 | 131, 134,
29, 102, 137, 144 | decltc 12454 |
. . . . . . . 8
⊢ ;;;;15126 < ;;;;16105 |
146 | 132, 135,
41, 25, 136, 145 | decltc 12454 |
. . . . . . 7
⊢ ;;;;;151263 < ;;;;;161051 |
147 | 130, 146 | eqbrtri 5095 |
. . . . . 6
⊢ (;;;;16807 · 9) < ;;;;;161051 |
148 | 98, 147 | eqbrtri 5095 |
. . . . 5
⊢ (9
· ;;;;16807) < ;;;;;161051 |
149 | 94, 148 | eqbrtri 5095 |
. . . 4
⊢ (9
· (7↑5)) < ;;;;;161051 |
150 | 4 | eqcomi 2747 |
. . . . . . . 8
⊢ 5 = (4 +
1) |
151 | 150 | oveq2i 7279 |
. . . . . . 7
⊢ (;11↑5) = (;11↑(4 + 1)) |
152 | 25, 25 | deccl 12440 |
. . . . . . . . . . 11
⊢ ;11 ∈
ℕ0 |
153 | 152 | nn0cni 12233 |
. . . . . . . . . 10
⊢ ;11 ∈ ℂ |
154 | 153, 21 | pm3.2i 471 |
. . . . . . . . 9
⊢ (;11 ∈ ℂ ∧ 4 ∈
ℕ0) |
155 | | expp1 13777 |
. . . . . . . . 9
⊢ ((;11 ∈ ℂ ∧ 4 ∈
ℕ0) → (;11↑(4 + 1)) = ((;11↑4) · ;11)) |
156 | 154, 155 | ax-mp 5 |
. . . . . . . 8
⊢ (;11↑(4 + 1)) = ((;11↑4) · ;11) |
157 | 2 | eqcomi 2747 |
. . . . . . . . . . 11
⊢ 4 = (2 +
2) |
158 | 157 | oveq2i 7279 |
. . . . . . . . . 10
⊢ (;11↑4) = (;11↑(2 + 2)) |
159 | 153, 9, 9 | 3pm3.2i 1338 |
. . . . . . . . . . . 12
⊢ (;11 ∈ ℂ ∧ 2 ∈
ℕ0 ∧ 2 ∈ ℕ0) |
160 | | expadd 13813 |
. . . . . . . . . . . 12
⊢ ((;11 ∈ ℂ ∧ 2 ∈
ℕ0 ∧ 2 ∈ ℕ0) → (;11↑(2 + 2)) = ((;11↑2) · (;11↑2))) |
161 | 159, 160 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (;11↑(2 + 2)) = ((;11↑2) · (;11↑2)) |
162 | 153 | sqvali 13885 |
. . . . . . . . . . . . . 14
⊢ (;11↑2) = (;11 · ;11) |
163 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ ;11 = ;11 |
164 | 153 | mulid2i 10968 |
. . . . . . . . . . . . . . . 16
⊢ (1
· ;11) = ;11 |
165 | 25, 25, 32, 164 | decsuc 12456 |
. . . . . . . . . . . . . . 15
⊢ ((1
· ;11) + 1) = ;12 |
166 | 152, 25, 25, 163, 25, 25, 165, 164 | decmul1c 12490 |
. . . . . . . . . . . . . 14
⊢ (;11 · ;11) = ;;121 |
167 | 162, 166 | eqtri 2766 |
. . . . . . . . . . . . 13
⊢ (;11↑2) = ;;121 |
168 | 167, 167 | oveq12i 7280 |
. . . . . . . . . . . 12
⊢ ((;11↑2) · (;11↑2)) = (;;121
· ;;121) |
169 | 25, 9 | deccl 12440 |
. . . . . . . . . . . . . 14
⊢ ;12 ∈
ℕ0 |
170 | 169, 25 | deccl 12440 |
. . . . . . . . . . . . 13
⊢ ;;121 ∈ ℕ0 |
171 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ ;;121 = ;;121 |
172 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ ;12 = ;12 |
173 | 170 | nn0cni 12233 |
. . . . . . . . . . . . . . . 16
⊢ ;;121 ∈ ℂ |
174 | 173 | mulid2i 10968 |
. . . . . . . . . . . . . . 15
⊢ (1
· ;;121) = ;;121 |
175 | 25 | dec0h 12447 |
. . . . . . . . . . . . . . . 16
⊢ 1 = ;01 |
176 | 67 | addid2i 11151 |
. . . . . . . . . . . . . . . 16
⊢ (0 + 2) =
2 |
177 | 49, 86, 4 | addcomli 11155 |
. . . . . . . . . . . . . . . 16
⊢ (1 + 4) =
5 |
178 | 28, 25, 9, 21, 175, 66, 176, 177 | decadd 12479 |
. . . . . . . . . . . . . . 15
⊢ (1 +
;24) = ;25 |
179 | 25, 9, 9, 172, 2 | decaddi 12485 |
. . . . . . . . . . . . . . 15
⊢ (;12 + 2) = ;14 |
180 | | 5cn 12049 |
. . . . . . . . . . . . . . . 16
⊢ 5 ∈
ℂ |
181 | 180, 86, 114 | addcomli 11155 |
. . . . . . . . . . . . . . 15
⊢ (1 + 5) =
6 |
182 | 169, 25, 9, 102, 174, 178, 179, 181 | decadd 12479 |
. . . . . . . . . . . . . 14
⊢ ((1
· ;;121) + (1 + ;24)) = ;;146 |
183 | 9 | dec0h 12447 |
. . . . . . . . . . . . . . 15
⊢ 2 = ;02 |
184 | 28, 28 | nn0addcli 12258 |
. . . . . . . . . . . . . . . 16
⊢ (0 + 0)
∈ ℕ0 |
185 | | 2t1e2 12124 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· 1) = 2 |
186 | 185 | oveq1i 7278 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
· 1) + 0) = (2 + 0) |
187 | 186, 122 | eqtri 2766 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
· 1) + 0) = 2 |
188 | | 2t2e4 12125 |
. . . . . . . . . . . . . . . . . 18
⊢ (2
· 2) = 4 |
189 | 21 | dec0h 12447 |
. . . . . . . . . . . . . . . . . . 19
⊢ 4 = ;04 |
190 | 189 | eqcomi 2747 |
. . . . . . . . . . . . . . . . . 18
⊢ ;04 = 4 |
191 | 188, 190 | eqtr4i 2769 |
. . . . . . . . . . . . . . . . 17
⊢ (2
· 2) = ;04 |
192 | 9, 25, 9, 172, 21, 28, 187, 191 | decmul2c 12491 |
. . . . . . . . . . . . . . . 16
⊢ (2
· ;12) = ;24 |
193 | 84 | oveq2i 7279 |
. . . . . . . . . . . . . . . . 17
⊢ (4 + (0 +
0)) = (4 + 0) |
194 | 49 | addid1i 11150 |
. . . . . . . . . . . . . . . . 17
⊢ (4 + 0) =
4 |
195 | 193, 194 | eqtri 2766 |
. . . . . . . . . . . . . . . 16
⊢ (4 + (0 +
0)) = 4 |
196 | 9, 21, 184, 192, 195 | decaddi 12485 |
. . . . . . . . . . . . . . 15
⊢ ((2
· ;12) + (0 + 0)) = ;24 |
197 | 185 | oveq1i 7278 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
· 1) + 2) = (2 + 2) |
198 | 197, 2 | eqtri 2766 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 1) + 2) = 4 |
199 | 198, 190 | eqtr4i 2769 |
. . . . . . . . . . . . . . 15
⊢ ((2
· 1) + 2) = ;04 |
200 | 169, 25, 28, 9, 171, 183, 9, 21, 28, 196, 199 | decma2c 12478 |
. . . . . . . . . . . . . 14
⊢ ((2
· ;;121) + 2) = ;;244 |
201 | 25, 9, 25, 9, 172, 172, 170, 21, 60, 182, 200 | decmac 12477 |
. . . . . . . . . . . . 13
⊢ ((;12 · ;;121) +
;12) = ;;;1464 |
202 | 170, 169,
25, 171, 25, 169, 201, 174 | decmul1c 12490 |
. . . . . . . . . . . 12
⊢ (;;121 · ;;121) =
;;;;14641 |
203 | 168, 202 | eqtri 2766 |
. . . . . . . . . . 11
⊢ ((;11↑2) · (;11↑2)) = ;;;;14641 |
204 | 161, 203 | eqtri 2766 |
. . . . . . . . . 10
⊢ (;11↑(2 + 2)) = ;;;;14641 |
205 | 158, 204 | eqtri 2766 |
. . . . . . . . 9
⊢ (;11↑4) = ;;;;14641 |
206 | 205 | oveq1i 7278 |
. . . . . . . 8
⊢ ((;11↑4) · ;11) = (;;;;14641 · ;11) |
207 | 156, 206 | eqtri 2766 |
. . . . . . 7
⊢ (;11↑(4 + 1)) = (;;;;14641 · ;11) |
208 | 151, 207 | eqtri 2766 |
. . . . . 6
⊢ (;11↑5) = (;;;;14641 · ;11) |
209 | 25, 21 | deccl 12440 |
. . . . . . . . 9
⊢ ;14 ∈
ℕ0 |
210 | 209, 29 | deccl 12440 |
. . . . . . . 8
⊢ ;;146 ∈ ℕ0 |
211 | 210, 21 | deccl 12440 |
. . . . . . 7
⊢ ;;;1464
∈ ℕ0 |
212 | | eqid 2738 |
. . . . . . 7
⊢ ;;;;14641 = ;;;;14641 |
213 | | eqid 2738 |
. . . . . . . 8
⊢ ;;;1464 =
;;;1464 |
214 | | eqid 2738 |
. . . . . . . . 9
⊢ ;;146 = ;;146 |
215 | 194, 190 | eqtr4i 2769 |
. . . . . . . . . 10
⊢ (4 + 0) =
;04 |
216 | 49, 77, 215 | addcomli 11155 |
. . . . . . . . 9
⊢ (0 + 4) =
;04 |
217 | | eqid 2738 |
. . . . . . . . . 10
⊢ ;14 = ;14 |
218 | 8 | addid1i 11150 |
. . . . . . . . . . . 12
⊢ (7 + 0) =
7 |
219 | 218, 89 | eqtr4i 2769 |
. . . . . . . . . . 11
⊢ (7 + 0) =
;07 |
220 | 8, 77, 219 | addcomli 11155 |
. . . . . . . . . 10
⊢ (0 + 7) =
;07 |
221 | 28, 102 | nn0addcli 12258 |
. . . . . . . . . . 11
⊢ (0 + 5)
∈ ℕ0 |
222 | 180 | addid2i 11151 |
. . . . . . . . . . . . 13
⊢ (0 + 5) =
5 |
223 | 222 | oveq2i 7279 |
. . . . . . . . . . . 12
⊢ (1 + (0 +
5)) = (1 + 5) |
224 | 223, 181 | eqtri 2766 |
. . . . . . . . . . 11
⊢ (1 + (0 +
5)) = 6 |
225 | 25, 25, 221, 164, 224 | decaddi 12485 |
. . . . . . . . . 10
⊢ ((1
· ;11) + (0 + 5)) = ;16 |
226 | 49 | mulid1i 10967 |
. . . . . . . . . . . . 13
⊢ (4
· 1) = 4 |
227 | | 0p1e1 12083 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
228 | 226, 227 | oveq12i 7280 |
. . . . . . . . . . . 12
⊢ ((4
· 1) + (0 + 1)) = (4 + 1) |
229 | 228, 4 | eqtri 2766 |
. . . . . . . . . . 11
⊢ ((4
· 1) + (0 + 1)) = 5 |
230 | 226 | oveq1i 7278 |
. . . . . . . . . . . 12
⊢ ((4
· 1) + 7) = (4 + 7) |
231 | 230, 116 | eqtri 2766 |
. . . . . . . . . . 11
⊢ ((4
· 1) + 7) = ;11 |
232 | 25, 25, 28, 59, 163, 88, 21, 25, 25, 229, 231 | decma2c 12478 |
. . . . . . . . . 10
⊢ ((4
· ;11) + 7) = ;51 |
233 | 25, 21, 28, 59, 217, 220, 152, 25, 102, 225, 232 | decmac 12477 |
. . . . . . . . 9
⊢ ((;14 · ;11) + (0 + 7)) = ;;161 |
234 | 36 | mulid1i 10967 |
. . . . . . . . . . . 12
⊢ (6
· 1) = 6 |
235 | 86 | addid2i 11151 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
236 | 234, 235 | oveq12i 7280 |
. . . . . . . . . . 11
⊢ ((6
· 1) + (0 + 1)) = (6 + 1) |
237 | | 6p1e7 12109 |
. . . . . . . . . . 11
⊢ (6 + 1) =
7 |
238 | 236, 237 | eqtri 2766 |
. . . . . . . . . 10
⊢ ((6
· 1) + (0 + 1)) = 7 |
239 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ 4 =
4 |
240 | 234, 239 | oveq12i 7280 |
. . . . . . . . . . 11
⊢ ((6
· 1) + 4) = (6 + 4) |
241 | 240, 44 | eqtri 2766 |
. . . . . . . . . 10
⊢ ((6
· 1) + 4) = ;10 |
242 | 25, 25, 28, 21, 163, 189, 29, 28, 25, 238, 241 | decma2c 12478 |
. . . . . . . . 9
⊢ ((6
· ;11) + 4) = ;70 |
243 | 209, 29, 28, 21, 214, 216, 152, 28, 59, 233, 242 | decmac 12477 |
. . . . . . . 8
⊢ ((;;146 · ;11) + (0 + 4)) = ;;;1610 |
244 | 226, 84 | oveq12i 7280 |
. . . . . . . . . 10
⊢ ((4
· 1) + (0 + 0)) = (4 + 0) |
245 | 244, 194 | eqtri 2766 |
. . . . . . . . 9
⊢ ((4
· 1) + (0 + 0)) = 4 |
246 | 226 | oveq1i 7278 |
. . . . . . . . . . 11
⊢ ((4
· 1) + 1) = (4 + 1) |
247 | 246, 4 | eqtri 2766 |
. . . . . . . . . 10
⊢ ((4
· 1) + 1) = 5 |
248 | 102 | dec0h 12447 |
. . . . . . . . . . 11
⊢ 5 = ;05 |
249 | 248 | eqcomi 2747 |
. . . . . . . . . 10
⊢ ;05 = 5 |
250 | 247, 249 | eqtr4i 2769 |
. . . . . . . . 9
⊢ ((4
· 1) + 1) = ;05 |
251 | 25, 25, 28, 25, 163, 175, 21, 102, 28, 245, 250 | decma2c 12478 |
. . . . . . . 8
⊢ ((4
· ;11) + 1) = ;45 |
252 | 210, 21, 28, 25, 213, 175, 152, 102, 21, 243, 251 | decmac 12477 |
. . . . . . 7
⊢ ((;;;1464
· ;11) + 1) = ;;;;16105 |
253 | 152, 211,
25, 212, 25, 25, 252, 164 | decmul1c 12490 |
. . . . . 6
⊢ (;;;;14641 · ;11) = ;;;;;161051 |
254 | 208, 253 | eqtri 2766 |
. . . . 5
⊢ (;11↑5) = ;;;;;161051 |
255 | 254 | eqcomi 2747 |
. . . 4
⊢ ;;;;;161051 = (;11↑5) |
256 | 149, 255 | breqtri 5099 |
. . 3
⊢ (9
· (7↑5)) < (;11↑5) |
257 | | 7re 12054 |
. . . . . 6
⊢ 7 ∈
ℝ |
258 | | 5nn 12047 |
. . . . . . 7
⊢ 5 ∈
ℕ |
259 | 258 | nnzi 12332 |
. . . . . 6
⊢ 5 ∈
ℤ |
260 | | 7pos 12072 |
. . . . . 6
⊢ 0 <
7 |
261 | 257, 259,
260 | 3pm3.2i 1338 |
. . . . 5
⊢ (7 ∈
ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) |
262 | | expgt0 13804 |
. . . . 5
⊢ ((7
∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) → 0 <
(7↑5)) |
263 | 261, 262 | ax-mp 5 |
. . . 4
⊢ 0 <
(7↑5) |
264 | | 9re 12060 |
. . . . 5
⊢ 9 ∈
ℝ |
265 | | 1nn 11972 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
266 | 25, 265 | decnncl 12445 |
. . . . . . . 8
⊢ ;11 ∈ ℕ |
267 | 266 | nnrei 11970 |
. . . . . . 7
⊢ ;11 ∈ ℝ |
268 | 267, 102 | pm3.2i 471 |
. . . . . 6
⊢ (;11 ∈ ℝ ∧ 5 ∈
ℕ0) |
269 | | reexpcl 13787 |
. . . . . 6
⊢ ((;11 ∈ ℝ ∧ 5 ∈
ℕ0) → (;11↑5) ∈ ℝ) |
270 | 268, 269 | ax-mp 5 |
. . . . 5
⊢ (;11↑5) ∈
ℝ |
271 | 257, 102 | pm3.2i 471 |
. . . . . 6
⊢ (7 ∈
ℝ ∧ 5 ∈ ℕ0) |
272 | | reexpcl 13787 |
. . . . . 6
⊢ ((7
∈ ℝ ∧ 5 ∈ ℕ0) → (7↑5) ∈
ℝ) |
273 | 271, 272 | ax-mp 5 |
. . . . 5
⊢
(7↑5) ∈ ℝ |
274 | 264, 270,
273 | ltmuldivi 11883 |
. . . 4
⊢ (0 <
(7↑5) → ((9 · (7↑5)) < (;11↑5) ↔ 9 < ((;11↑5) / (7↑5)))) |
275 | 263, 274 | ax-mp 5 |
. . 3
⊢ ((9
· (7↑5)) < (;11↑5) ↔ 9 < ((;11↑5) / (7↑5))) |
276 | 256, 275 | mpbi 229 |
. 2
⊢ 9 <
((;11↑5) /
(7↑5)) |
277 | 153 | a1i 11 |
. . . . 5
⊢ (⊤
→ ;11 ∈
ℂ) |
278 | 8 | a1i 11 |
. . . . 5
⊢ (⊤
→ 7 ∈ ℂ) |
279 | | 0red 10966 |
. . . . . . 7
⊢ (⊤
→ 0 ∈ ℝ) |
280 | 260 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 0 < 7) |
281 | 279, 280 | ltned 11099 |
. . . . . 6
⊢ (⊤
→ 0 ≠ 7) |
282 | 281 | necomd 2999 |
. . . . 5
⊢ (⊤
→ 7 ≠ 0) |
283 | 102 | a1i 11 |
. . . . 5
⊢ (⊤
→ 5 ∈ ℕ0) |
284 | 277, 278,
282, 283 | expdivd 13866 |
. . . 4
⊢ (⊤
→ ((;11 / 7)↑5) =
((;11↑5) /
(7↑5))) |
285 | 284 | eqcomd 2744 |
. . 3
⊢ (⊤
→ ((;11↑5) / (7↑5))
= ((;11 /
7)↑5)) |
286 | 285 | mptru 1546 |
. 2
⊢ ((;11↑5) / (7↑5)) = ((;11 / 7)↑5) |
287 | 276, 286 | breqtri 5099 |
1
⊢ 9 <
((;11 /
7)↑5) |