Proof of Theorem 3lexlogpow5ineq1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . . . . . . 10
⊢ 5 =
5 | 
| 2 |  | 2p2e4 12401 | . . . . . . . . . . . 12
⊢ (2 + 2) =
4 | 
| 3 | 2 | oveq1i 7441 | . . . . . . . . . . 11
⊢ ((2 + 2)
+ 1) = (4 + 1) | 
| 4 |  | 4p1e5 12412 | . . . . . . . . . . 11
⊢ (4 + 1) =
5 | 
| 5 | 3, 4 | eqtri 2765 | . . . . . . . . . 10
⊢ ((2 + 2)
+ 1) = 5 | 
| 6 | 1, 5 | eqtr4i 2768 | . . . . . . . . 9
⊢ 5 = ((2 +
2) + 1) | 
| 7 | 6 | oveq2i 7442 | . . . . . . . 8
⊢
(7↑5) = (7↑((2 + 2) + 1)) | 
| 8 |  | 7cn 12360 | . . . . . . . . . 10
⊢ 7 ∈
ℂ | 
| 9 |  | 2nn0 12543 | . . . . . . . . . . 11
⊢ 2 ∈
ℕ0 | 
| 10 | 9, 9 | nn0addcli 12563 | . . . . . . . . . 10
⊢ (2 + 2)
∈ ℕ0 | 
| 11 | 8, 10 | pm3.2i 470 | . . . . . . . . 9
⊢ (7 ∈
ℂ ∧ (2 + 2) ∈ ℕ0) | 
| 12 |  | expp1 14109 | . . . . . . . . 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 1340 | . . . . . . . . . . 11
⊢ (7 ∈
ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈
ℕ0) | 
| 15 |  | expadd 14145 | . . . . . . . . . . 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 14219 | . . . . . . . . . . . . 13
⊢
(7↑2) = (7 · 7) | 
| 18 |  | 7t7e49 12847 | . . . . . . . . . . . . 13
⊢ (7
· 7) = ;49 | 
| 19 | 17, 18 | eqtri 2765 | . . . . . . . . . . . 12
⊢
(7↑2) = ;49 | 
| 20 | 19, 19 | oveq12i 7443 | . . . . . . . . . . 11
⊢
((7↑2) · (7↑2)) = (;49 · ;49) | 
| 21 |  | 4nn0 12545 | . . . . . . . . . . . . 13
⊢ 4 ∈
ℕ0 | 
| 22 |  | 9nn0 12550 | . . . . . . . . . . . . 13
⊢ 9 ∈
ℕ0 | 
| 23 | 21, 22 | deccl 12748 | . . . . . . . . . . . 12
⊢ ;49 ∈
ℕ0 | 
| 24 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ ;49 = ;49 | 
| 25 |  | 1nn0 12542 | . . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 | 
| 26 | 21, 21 | deccl 12748 | . . . . . . . . . . . 12
⊢ ;44 ∈
ℕ0 | 
| 27 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ ;44 = ;44 | 
| 28 |  | 0nn0 12541 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 | 
| 29 |  | 6nn0 12547 | . . . . . . . . . . . . . 14
⊢ 6 ∈
ℕ0 | 
| 30 | 21, 21 | nn0addcli 12563 | . . . . . . . . . . . . . 14
⊢ (4 + 4)
∈ ℕ0 | 
| 31 |  | 4t4e16 12832 | . . . . . . . . . . . . . 14
⊢ (4
· 4) = ;16 | 
| 32 |  | 1p1e2 12391 | . . . . . . . . . . . . . 14
⊢ (1 + 1) =
2 | 
| 33 |  | 4p4e8 12421 | . . . . . . . . . . . . . . . 16
⊢ (4 + 4) =
8 | 
| 34 | 33 | oveq2i 7442 | . . . . . . . . . . . . . . 15
⊢ (6 + (4 +
4)) = (6 + 8) | 
| 35 |  | 8cn 12363 | . . . . . . . . . . . . . . . 16
⊢ 8 ∈
ℂ | 
| 36 |  | 6cn 12357 | . . . . . . . . . . . . . . . 16
⊢ 6 ∈
ℂ | 
| 37 |  | 8p6e14 12817 | . . . . . . . . . . . . . . . 16
⊢ (8 + 6) =
;14 | 
| 38 | 35, 36, 37 | addcomli 11453 | . . . . . . . . . . . . . . 15
⊢ (6 + 8) =
;14 | 
| 39 | 34, 38 | eqtri 2765 | . . . . . . . . . . . . . 14
⊢ (6 + (4 +
4)) = ;14 | 
| 40 | 25, 29, 30, 31, 32, 21, 39 | decaddci 12794 | . . . . . . . . . . . . 13
⊢ ((4
· 4) + (4 + 4)) = ;24 | 
| 41 |  | 3nn0 12544 | . . . . . . . . . . . . . 14
⊢ 3 ∈
ℕ0 | 
| 42 |  | 9t4e36 12857 | . . . . . . . . . . . . . 14
⊢ (9
· 4) = ;36 | 
| 43 |  | 3p1e4 12411 | . . . . . . . . . . . . . 14
⊢ (3 + 1) =
4 | 
| 44 |  | 6p4e10 12805 | . . . . . . . . . . . . . 14
⊢ (6 + 4) =
;10 | 
| 45 | 41, 29, 21, 42, 43, 44 | decaddci2 12795 | . . . . . . . . . . . . 13
⊢ ((9
· 4) + 4) = ;40 | 
| 46 | 21, 22, 21, 21, 24, 27, 21, 28, 21, 40, 45 | decmac 12785 | . . . . . . . . . . . 12
⊢ ((;49 · 4) + ;44) = ;;240 | 
| 47 |  | 8nn0 12549 | . . . . . . . . . . . . 13
⊢ 8 ∈
ℕ0 | 
| 48 |  | 9cn 12366 | . . . . . . . . . . . . . . 15
⊢ 9 ∈
ℂ | 
| 49 |  | 4cn 12351 | . . . . . . . . . . . . . . 15
⊢ 4 ∈
ℂ | 
| 50 | 48, 49, 42 | mulcomli 11270 | . . . . . . . . . . . . . 14
⊢ (4
· 9) = ;36 | 
| 51 | 41, 29, 47, 50, 43, 21, 38 | decaddci 12794 | . . . . . . . . . . . . 13
⊢ ((4
· 9) + 8) = ;44 | 
| 52 |  | 9t9e81 12862 | . . . . . . . . . . . . 13
⊢ (9
· 9) = ;81 | 
| 53 | 22, 21, 22, 24, 25, 47, 51, 52 | decmul1c 12798 | . . . . . . . . . . . 12
⊢ (;49 · 9) = ;;441 | 
| 54 | 23, 21, 22, 24, 25, 26, 46, 53 | decmul2c 12799 | . . . . . . . . . . 11
⊢ (;49 · ;49) = ;;;2401 | 
| 55 | 20, 54 | eqtri 2765 | . . . . . . . . . 10
⊢
((7↑2) · (7↑2)) = ;;;2401 | 
| 56 | 16, 55 | eqtri 2765 | . . . . . . . . 9
⊢
(7↑(2 + 2)) = ;;;2401 | 
| 57 | 56 | oveq1i 7441 | . . . . . . . 8
⊢
((7↑(2 + 2)) · 7) = (;;;2401 · 7) | 
| 58 | 7, 13, 57 | 3eqtri 2769 | . . . . . . 7
⊢
(7↑5) = (;;;2401 · 7) | 
| 59 |  | 7nn0 12548 | . . . . . . . 8
⊢ 7 ∈
ℕ0 | 
| 60 | 9, 21 | deccl 12748 | . . . . . . . . 9
⊢ ;24 ∈
ℕ0 | 
| 61 | 60, 28 | deccl 12748 | . . . . . . . 8
⊢ ;;240 ∈ ℕ0 | 
| 62 |  | eqid 2737 | . . . . . . . 8
⊢ ;;;2401 =
;;;2401 | 
| 63 | 25, 29 | deccl 12748 | . . . . . . . . . 10
⊢ ;16 ∈
ℕ0 | 
| 64 | 63, 47 | deccl 12748 | . . . . . . . . 9
⊢ ;;168 ∈ ℕ0 | 
| 65 |  | eqid 2737 | . . . . . . . . . 10
⊢ ;;240 = ;;240 | 
| 66 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ ;24 = ;24 | 
| 67 |  | 2cn 12341 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ | 
| 68 |  | 7t2e14 12842 | . . . . . . . . . . . . . 14
⊢ (7
· 2) = ;14 | 
| 69 | 8, 67, 68 | mulcomli 11270 | . . . . . . . . . . . . 13
⊢ (2
· 7) = ;14 | 
| 70 |  | 4p2e6 12419 | . . . . . . . . . . . . 13
⊢ (4 + 2) =
6 | 
| 71 | 25, 21, 9, 69, 70 | decaddi 12793 | . . . . . . . . . . . 12
⊢ ((2
· 7) + 2) = ;16 | 
| 72 |  | 7t4e28 12844 | . . . . . . . . . . . . 13
⊢ (7
· 4) = ;28 | 
| 73 | 8, 49, 72 | mulcomli 11270 | . . . . . . . . . . . 12
⊢ (4
· 7) = ;28 | 
| 74 | 59, 9, 21, 66, 47, 9, 71, 73 | decmul1c 12798 | . . . . . . . . . . 11
⊢ (;24 · 7) = ;;168 | 
| 75 | 35 | addridi 11448 | . . . . . . . . . . 11
⊢ (8 + 0) =
8 | 
| 76 | 63, 47, 28, 74, 75 | decaddi 12793 | . . . . . . . . . 10
⊢ ((;24 · 7) + 0) = ;;168 | 
| 77 |  | 0cn 11253 | . . . . . . . . . . 11
⊢ 0 ∈
ℂ | 
| 78 | 8 | mul01i 11451 | . . . . . . . . . . . 12
⊢ (7
· 0) = 0 | 
| 79 | 28 | dec0h 12755 | . . . . . . . . . . . . 13
⊢ 0 = ;00 | 
| 80 | 79 | eqcomi 2746 | . . . . . . . . . . . 12
⊢ ;00 = 0 | 
| 81 | 78, 80 | eqtr4i 2768 | . . . . . . . . . . 11
⊢ (7
· 0) = ;00 | 
| 82 | 8, 77, 81 | mulcomli 11270 | . . . . . . . . . 10
⊢ (0
· 7) = ;00 | 
| 83 | 59, 60, 28, 65, 28, 28, 76, 82 | decmul1c 12798 | . . . . . . . . 9
⊢ (;;240 · 7) = ;;;1680 | 
| 84 |  | 00id 11436 | . . . . . . . . 9
⊢ (0 + 0) =
0 | 
| 85 | 64, 28, 28, 83, 84 | decaddi 12793 | . . . . . . . 8
⊢ ((;;240 · 7) + 0) = ;;;1680 | 
| 86 |  | ax-1cn 11213 | . . . . . . . . 9
⊢ 1 ∈
ℂ | 
| 87 | 8 | mulridi 11265 | . . . . . . . . . 10
⊢ (7
· 1) = 7 | 
| 88 | 59 | dec0h 12755 | . . . . . . . . . . 11
⊢ 7 = ;07 | 
| 89 | 88 | eqcomi 2746 | . . . . . . . . . 10
⊢ ;07 = 7 | 
| 90 | 87, 89 | eqtr4i 2768 | . . . . . . . . 9
⊢ (7
· 1) = ;07 | 
| 91 | 8, 86, 90 | mulcomli 11270 | . . . . . . . 8
⊢ (1
· 7) = ;07 | 
| 92 | 59, 61, 25, 62, 59, 28, 85, 91 | decmul1c 12798 | . . . . . . 7
⊢ (;;;2401
· 7) = ;;;;16807 | 
| 93 | 58, 92 | eqtri 2765 | . . . . . 6
⊢
(7↑5) = ;;;;16807 | 
| 94 | 93 | oveq2i 7442 | . . . . 5
⊢ (9
· (7↑5)) = (9 · ;;;;16807) | 
| 95 | 64, 28 | deccl 12748 | . . . . . . . . 9
⊢ ;;;1680
∈ ℕ0 | 
| 96 | 95, 59 | deccl 12748 | . . . . . . . 8
⊢ ;;;;16807 ∈
ℕ0 | 
| 97 | 96 | nn0cni 12538 | . . . . . . 7
⊢ ;;;;16807 ∈ ℂ | 
| 98 | 48, 97 | mulcomi 11269 | . . . . . 6
⊢ (9
· ;;;;16807) = (;;;;16807 · 9) | 
| 99 |  | eqid 2737 | . . . . . . . 8
⊢ ;;;;16807 = ;;;;16807 | 
| 100 |  | eqid 2737 | . . . . . . . . 9
⊢ ;;;1680 =
;;;1680 | 
| 101 | 29 | dec0h 12755 | . . . . . . . . 9
⊢ 6 = ;06 | 
| 102 |  | 5nn0 12546 | . . . . . . . . . . . 12
⊢ 5 ∈
ℕ0 | 
| 103 | 25, 102 | deccl 12748 | . . . . . . . . . . 11
⊢ ;15 ∈
ℕ0 | 
| 104 | 103, 25 | deccl 12748 | . . . . . . . . . 10
⊢ ;;151 ∈ ℕ0 | 
| 105 |  | eqid 2737 | . . . . . . . . . . 11
⊢ ;;168 = ;;168 | 
| 106 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ ;16 = ;16 | 
| 107 | 48 | mullidi 11266 | . . . . . . . . . . . . . 14
⊢ (1
· 9) = 9 | 
| 108 | 36 | addlidi 11449 | . . . . . . . . . . . . . 14
⊢ (0 + 6) =
6 | 
| 109 | 107, 108 | oveq12i 7443 | . . . . . . . . . . . . 13
⊢ ((1
· 9) + (0 + 6)) = (9 + 6) | 
| 110 |  | 9p6e15 12824 | . . . . . . . . . . . . 13
⊢ (9 + 6) =
;15 | 
| 111 | 109, 110 | eqtri 2765 | . . . . . . . . . . . 12
⊢ ((1
· 9) + (0 + 6)) = ;15 | 
| 112 |  | 9t6e54 12859 | . . . . . . . . . . . . . 14
⊢ (9
· 6) = ;54 | 
| 113 | 48, 36, 112 | mulcomli 11270 | . . . . . . . . . . . . 13
⊢ (6
· 9) = ;54 | 
| 114 |  | 5p1e6 12413 | . . . . . . . . . . . . 13
⊢ (5 + 1) =
6 | 
| 115 |  | 7p4e11 12809 | . . . . . . . . . . . . . 14
⊢ (7 + 4) =
;11 | 
| 116 | 8, 49, 115 | addcomli 11453 | . . . . . . . . . . . . 13
⊢ (4 + 7) =
;11 | 
| 117 | 102, 21, 59, 113, 114, 25, 116 | decaddci 12794 | . . . . . . . . . . . 12
⊢ ((6
· 9) + 7) = ;61 | 
| 118 | 25, 29, 28, 59, 106, 88, 22, 25, 29, 111, 117 | decmac 12785 | . . . . . . . . . . 11
⊢ ((;16 · 9) + 7) = ;;151 | 
| 119 |  | 9t8e72 12861 | . . . . . . . . . . . 12
⊢ (9
· 8) = ;72 | 
| 120 | 48, 35, 119 | mulcomli 11270 | . . . . . . . . . . 11
⊢ (8
· 9) = ;72 | 
| 121 | 22, 63, 47, 105, 9, 59, 118, 120 | decmul1c 12798 | . . . . . . . . . 10
⊢ (;;168 · 9) = ;;;1512 | 
| 122 | 67 | addridi 11448 | . . . . . . . . . 10
⊢ (2 + 0) =
2 | 
| 123 | 104, 9, 28, 121, 122 | decaddi 12793 | . . . . . . . . 9
⊢ ((;;168 · 9) + 0) = ;;;1512 | 
| 124 | 48 | mul02i 11450 | . . . . . . . . . . 11
⊢ (0
· 9) = 0 | 
| 125 | 124 | oveq1i 7441 | . . . . . . . . . 10
⊢ ((0
· 9) + 6) = (0 + 6) | 
| 126 | 125, 108 | eqtri 2765 | . . . . . . . . 9
⊢ ((0
· 9) + 6) = 6 | 
| 127 | 64, 28, 28, 29, 100, 101, 22, 123, 126 | decma 12784 | . . . . . . . 8
⊢ ((;;;1680
· 9) + 6) = ;;;;15126 | 
| 128 |  | 9t7e63 12860 | . . . . . . . . 9
⊢ (9
· 7) = ;63 | 
| 129 | 48, 8, 128 | mulcomli 11270 | . . . . . . . 8
⊢ (7
· 9) = ;63 | 
| 130 | 22, 95, 59, 99, 41, 29, 127, 129 | decmul1c 12798 | . . . . . . 7
⊢ (;;;;16807 · 9) = ;;;;;151263 | 
| 131 | 104, 9 | deccl 12748 | . . . . . . . . 9
⊢ ;;;1512
∈ ℕ0 | 
| 132 | 131, 29 | deccl 12748 | . . . . . . . 8
⊢ ;;;;15126 ∈
ℕ0 | 
| 133 | 63, 25 | deccl 12748 | . . . . . . . . . 10
⊢ ;;161 ∈ ℕ0 | 
| 134 | 133, 28 | deccl 12748 | . . . . . . . . 9
⊢ ;;;1610
∈ ℕ0 | 
| 135 | 134, 102 | deccl 12748 | . . . . . . . 8
⊢ ;;;;16105 ∈
ℕ0 | 
| 136 |  | 3lt10 12870 | . . . . . . . 8
⊢ 3 <
;10 | 
| 137 |  | 6lt10 12867 | . . . . . . . . 9
⊢ 6 <
;10 | 
| 138 |  | 2lt10 12871 | . . . . . . . . . 10
⊢ 2 <
;10 | 
| 139 |  | 1lt10 12872 | . . . . . . . . . . 11
⊢ 1 <
;10 | 
| 140 |  | 6nn 12355 | . . . . . . . . . . . 12
⊢ 6 ∈
ℕ | 
| 141 |  | 5lt6 12447 | . . . . . . . . . . . 12
⊢ 5 <
6 | 
| 142 | 25, 102, 140, 141 | declt 12761 | . . . . . . . . . . 11
⊢ ;15 < ;16 | 
| 143 | 103, 63, 25, 25, 139, 142 | decltc 12762 | . . . . . . . . . 10
⊢ ;;151 < ;;161 | 
| 144 | 104, 133,
9, 28, 138, 143 | decltc 12762 | . . . . . . . . 9
⊢ ;;;1512
< ;;;1610 | 
| 145 | 131, 134,
29, 102, 137, 144 | decltc 12762 | . . . . . . . 8
⊢ ;;;;15126 < ;;;;16105 | 
| 146 | 132, 135,
41, 25, 136, 145 | decltc 12762 | . . . . . . 7
⊢ ;;;;;151263 < ;;;;;161051 | 
| 147 | 130, 146 | eqbrtri 5164 | . . . . . 6
⊢ (;;;;16807 · 9) < ;;;;;161051 | 
| 148 | 98, 147 | eqbrtri 5164 | . . . . 5
⊢ (9
· ;;;;16807) < ;;;;;161051 | 
| 149 | 94, 148 | eqbrtri 5164 | . . . 4
⊢ (9
· (7↑5)) < ;;;;;161051 | 
| 150 | 4 | eqcomi 2746 | . . . . . . . 8
⊢ 5 = (4 +
1) | 
| 151 | 150 | oveq2i 7442 | . . . . . . 7
⊢ (;11↑5) = (;11↑(4 + 1)) | 
| 152 | 25, 25 | deccl 12748 | . . . . . . . . . . 11
⊢ ;11 ∈
ℕ0 | 
| 153 | 152 | nn0cni 12538 | . . . . . . . . . 10
⊢ ;11 ∈ ℂ | 
| 154 | 153, 21 | pm3.2i 470 | . . . . . . . . 9
⊢ (;11 ∈ ℂ ∧ 4 ∈
ℕ0) | 
| 155 |  | expp1 14109 | . . . . . . . . 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 2746 | . . . . . . . . . . 11
⊢ 4 = (2 +
2) | 
| 158 | 157 | oveq2i 7442 | . . . . . . . . . 10
⊢ (;11↑4) = (;11↑(2 + 2)) | 
| 159 | 153, 9, 9 | 3pm3.2i 1340 | . . . . . . . . . . . 12
⊢ (;11 ∈ ℂ ∧ 2 ∈
ℕ0 ∧ 2 ∈ ℕ0) | 
| 160 |  | expadd 14145 | . . . . . . . . . . . 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 14219 | . . . . . . . . . . . . . 14
⊢ (;11↑2) = (;11 · ;11) | 
| 163 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢ ;11 = ;11 | 
| 164 | 153 | mullidi 11266 | . . . . . . . . . . . . . . . 16
⊢ (1
· ;11) = ;11 | 
| 165 | 25, 25, 32, 164 | decsuc 12764 | . . . . . . . . . . . . . . 15
⊢ ((1
· ;11) + 1) = ;12 | 
| 166 | 152, 25, 25, 163, 25, 25, 165, 164 | decmul1c 12798 | . . . . . . . . . . . . . 14
⊢ (;11 · ;11) = ;;121 | 
| 167 | 162, 166 | eqtri 2765 | . . . . . . . . . . . . 13
⊢ (;11↑2) = ;;121 | 
| 168 | 167, 167 | oveq12i 7443 | . . . . . . . . . . . 12
⊢ ((;11↑2) · (;11↑2)) = (;;121
· ;;121) | 
| 169 | 25, 9 | deccl 12748 | . . . . . . . . . . . . . 14
⊢ ;12 ∈
ℕ0 | 
| 170 | 169, 25 | deccl 12748 | . . . . . . . . . . . . 13
⊢ ;;121 ∈ ℕ0 | 
| 171 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢ ;;121 = ;;121 | 
| 172 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢ ;12 = ;12 | 
| 173 | 170 | nn0cni 12538 | . . . . . . . . . . . . . . . 16
⊢ ;;121 ∈ ℂ | 
| 174 | 173 | mullidi 11266 | . . . . . . . . . . . . . . 15
⊢ (1
· ;;121) = ;;121 | 
| 175 | 25 | dec0h 12755 | . . . . . . . . . . . . . . . 16
⊢ 1 = ;01 | 
| 176 | 67 | addlidi 11449 | . . . . . . . . . . . . . . . 16
⊢ (0 + 2) =
2 | 
| 177 | 49, 86, 4 | addcomli 11453 | . . . . . . . . . . . . . . . 16
⊢ (1 + 4) =
5 | 
| 178 | 28, 25, 9, 21, 175, 66, 176, 177 | decadd 12787 | . . . . . . . . . . . . . . 15
⊢ (1 +
;24) = ;25 | 
| 179 | 25, 9, 9, 172, 2 | decaddi 12793 | . . . . . . . . . . . . . . 15
⊢ (;12 + 2) = ;14 | 
| 180 |  | 5cn 12354 | . . . . . . . . . . . . . . . 16
⊢ 5 ∈
ℂ | 
| 181 | 180, 86, 114 | addcomli 11453 | . . . . . . . . . . . . . . 15
⊢ (1 + 5) =
6 | 
| 182 | 169, 25, 9, 102, 174, 178, 179, 181 | decadd 12787 | . . . . . . . . . . . . . 14
⊢ ((1
· ;;121) + (1 + ;24)) = ;;146 | 
| 183 | 9 | dec0h 12755 | . . . . . . . . . . . . . . 15
⊢ 2 = ;02 | 
| 184 | 28, 28 | nn0addcli 12563 | . . . . . . . . . . . . . . . 16
⊢ (0 + 0)
∈ ℕ0 | 
| 185 |  | 2t1e2 12429 | . . . . . . . . . . . . . . . . . . 19
⊢ (2
· 1) = 2 | 
| 186 | 185 | oveq1i 7441 | . . . . . . . . . . . . . . . . . 18
⊢ ((2
· 1) + 0) = (2 + 0) | 
| 187 | 186, 122 | eqtri 2765 | . . . . . . . . . . . . . . . . 17
⊢ ((2
· 1) + 0) = 2 | 
| 188 |  | 2t2e4 12430 | . . . . . . . . . . . . . . . . . 18
⊢ (2
· 2) = 4 | 
| 189 | 21 | dec0h 12755 | . . . . . . . . . . . . . . . . . . 19
⊢ 4 = ;04 | 
| 190 | 189 | eqcomi 2746 | . . . . . . . . . . . . . . . . . 18
⊢ ;04 = 4 | 
| 191 | 188, 190 | eqtr4i 2768 | . . . . . . . . . . . . . . . . 17
⊢ (2
· 2) = ;04 | 
| 192 | 9, 25, 9, 172, 21, 28, 187, 191 | decmul2c 12799 | . . . . . . . . . . . . . . . 16
⊢ (2
· ;12) = ;24 | 
| 193 | 84 | oveq2i 7442 | . . . . . . . . . . . . . . . . 17
⊢ (4 + (0 +
0)) = (4 + 0) | 
| 194 | 49 | addridi 11448 | . . . . . . . . . . . . . . . . 17
⊢ (4 + 0) =
4 | 
| 195 | 193, 194 | eqtri 2765 | . . . . . . . . . . . . . . . 16
⊢ (4 + (0 +
0)) = 4 | 
| 196 | 9, 21, 184, 192, 195 | decaddi 12793 | . . . . . . . . . . . . . . 15
⊢ ((2
· ;12) + (0 + 0)) = ;24 | 
| 197 | 185 | oveq1i 7441 | . . . . . . . . . . . . . . . . 17
⊢ ((2
· 1) + 2) = (2 + 2) | 
| 198 | 197, 2 | eqtri 2765 | . . . . . . . . . . . . . . . 16
⊢ ((2
· 1) + 2) = 4 | 
| 199 | 198, 190 | eqtr4i 2768 | . . . . . . . . . . . . . . 15
⊢ ((2
· 1) + 2) = ;04 | 
| 200 | 169, 25, 28, 9, 171, 183, 9, 21, 28, 196, 199 | decma2c 12786 | . . . . . . . . . . . . . 14
⊢ ((2
· ;;121) + 2) = ;;244 | 
| 201 | 25, 9, 25, 9, 172, 172, 170, 21, 60, 182, 200 | decmac 12785 | . . . . . . . . . . . . 13
⊢ ((;12 · ;;121) +
;12) = ;;;1464 | 
| 202 | 170, 169,
25, 171, 25, 169, 201, 174 | decmul1c 12798 | . . . . . . . . . . . 12
⊢ (;;121 · ;;121) =
;;;;14641 | 
| 203 | 168, 202 | eqtri 2765 | . . . . . . . . . . 11
⊢ ((;11↑2) · (;11↑2)) = ;;;;14641 | 
| 204 | 161, 203 | eqtri 2765 | . . . . . . . . . 10
⊢ (;11↑(2 + 2)) = ;;;;14641 | 
| 205 | 158, 204 | eqtri 2765 | . . . . . . . . 9
⊢ (;11↑4) = ;;;;14641 | 
| 206 | 205 | oveq1i 7441 | . . . . . . . 8
⊢ ((;11↑4) · ;11) = (;;;;14641 · ;11) | 
| 207 | 156, 206 | eqtri 2765 | . . . . . . 7
⊢ (;11↑(4 + 1)) = (;;;;14641 · ;11) | 
| 208 | 151, 207 | eqtri 2765 | . . . . . 6
⊢ (;11↑5) = (;;;;14641 · ;11) | 
| 209 | 25, 21 | deccl 12748 | . . . . . . . . 9
⊢ ;14 ∈
ℕ0 | 
| 210 | 209, 29 | deccl 12748 | . . . . . . . 8
⊢ ;;146 ∈ ℕ0 | 
| 211 | 210, 21 | deccl 12748 | . . . . . . 7
⊢ ;;;1464
∈ ℕ0 | 
| 212 |  | eqid 2737 | . . . . . . 7
⊢ ;;;;14641 = ;;;;14641 | 
| 213 |  | eqid 2737 | . . . . . . . 8
⊢ ;;;1464 =
;;;1464 | 
| 214 |  | eqid 2737 | . . . . . . . . 9
⊢ ;;146 = ;;146 | 
| 215 | 194, 190 | eqtr4i 2768 | . . . . . . . . . 10
⊢ (4 + 0) =
;04 | 
| 216 | 49, 77, 215 | addcomli 11453 | . . . . . . . . 9
⊢ (0 + 4) =
;04 | 
| 217 |  | eqid 2737 | . . . . . . . . . 10
⊢ ;14 = ;14 | 
| 218 | 8 | addridi 11448 | . . . . . . . . . . . 12
⊢ (7 + 0) =
7 | 
| 219 | 218, 89 | eqtr4i 2768 | . . . . . . . . . . 11
⊢ (7 + 0) =
;07 | 
| 220 | 8, 77, 219 | addcomli 11453 | . . . . . . . . . 10
⊢ (0 + 7) =
;07 | 
| 221 | 28, 102 | nn0addcli 12563 | . . . . . . . . . . 11
⊢ (0 + 5)
∈ ℕ0 | 
| 222 | 180 | addlidi 11449 | . . . . . . . . . . . . 13
⊢ (0 + 5) =
5 | 
| 223 | 222 | oveq2i 7442 | . . . . . . . . . . . 12
⊢ (1 + (0 +
5)) = (1 + 5) | 
| 224 | 223, 181 | eqtri 2765 | . . . . . . . . . . 11
⊢ (1 + (0 +
5)) = 6 | 
| 225 | 25, 25, 221, 164, 224 | decaddi 12793 | . . . . . . . . . 10
⊢ ((1
· ;11) + (0 + 5)) = ;16 | 
| 226 | 49 | mulridi 11265 | . . . . . . . . . . . . 13
⊢ (4
· 1) = 4 | 
| 227 |  | 0p1e1 12388 | . . . . . . . . . . . . 13
⊢ (0 + 1) =
1 | 
| 228 | 226, 227 | oveq12i 7443 | . . . . . . . . . . . 12
⊢ ((4
· 1) + (0 + 1)) = (4 + 1) | 
| 229 | 228, 4 | eqtri 2765 | . . . . . . . . . . 11
⊢ ((4
· 1) + (0 + 1)) = 5 | 
| 230 | 226 | oveq1i 7441 | . . . . . . . . . . . 12
⊢ ((4
· 1) + 7) = (4 + 7) | 
| 231 | 230, 116 | eqtri 2765 | . . . . . . . . . . 11
⊢ ((4
· 1) + 7) = ;11 | 
| 232 | 25, 25, 28, 59, 163, 88, 21, 25, 25, 229, 231 | decma2c 12786 | . . . . . . . . . 10
⊢ ((4
· ;11) + 7) = ;51 | 
| 233 | 25, 21, 28, 59, 217, 220, 152, 25, 102, 225, 232 | decmac 12785 | . . . . . . . . 9
⊢ ((;14 · ;11) + (0 + 7)) = ;;161 | 
| 234 | 36 | mulridi 11265 | . . . . . . . . . . . 12
⊢ (6
· 1) = 6 | 
| 235 | 86 | addlidi 11449 | . . . . . . . . . . . 12
⊢ (0 + 1) =
1 | 
| 236 | 234, 235 | oveq12i 7443 | . . . . . . . . . . 11
⊢ ((6
· 1) + (0 + 1)) = (6 + 1) | 
| 237 |  | 6p1e7 12414 | . . . . . . . . . . 11
⊢ (6 + 1) =
7 | 
| 238 | 236, 237 | eqtri 2765 | . . . . . . . . . 10
⊢ ((6
· 1) + (0 + 1)) = 7 | 
| 239 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ 4 =
4 | 
| 240 | 234, 239 | oveq12i 7443 | . . . . . . . . . . 11
⊢ ((6
· 1) + 4) = (6 + 4) | 
| 241 | 240, 44 | eqtri 2765 | . . . . . . . . . 10
⊢ ((6
· 1) + 4) = ;10 | 
| 242 | 25, 25, 28, 21, 163, 189, 29, 28, 25, 238, 241 | decma2c 12786 | . . . . . . . . 9
⊢ ((6
· ;11) + 4) = ;70 | 
| 243 | 209, 29, 28, 21, 214, 216, 152, 28, 59, 233, 242 | decmac 12785 | . . . . . . . 8
⊢ ((;;146 · ;11) + (0 + 4)) = ;;;1610 | 
| 244 | 226, 84 | oveq12i 7443 | . . . . . . . . . 10
⊢ ((4
· 1) + (0 + 0)) = (4 + 0) | 
| 245 | 244, 194 | eqtri 2765 | . . . . . . . . 9
⊢ ((4
· 1) + (0 + 0)) = 4 | 
| 246 | 226 | oveq1i 7441 | . . . . . . . . . . 11
⊢ ((4
· 1) + 1) = (4 + 1) | 
| 247 | 246, 4 | eqtri 2765 | . . . . . . . . . 10
⊢ ((4
· 1) + 1) = 5 | 
| 248 | 102 | dec0h 12755 | . . . . . . . . . . 11
⊢ 5 = ;05 | 
| 249 | 248 | eqcomi 2746 | . . . . . . . . . 10
⊢ ;05 = 5 | 
| 250 | 247, 249 | eqtr4i 2768 | . . . . . . . . 9
⊢ ((4
· 1) + 1) = ;05 | 
| 251 | 25, 25, 28, 25, 163, 175, 21, 102, 28, 245, 250 | decma2c 12786 | . . . . . . . 8
⊢ ((4
· ;11) + 1) = ;45 | 
| 252 | 210, 21, 28, 25, 213, 175, 152, 102, 21, 243, 251 | decmac 12785 | . . . . . . 7
⊢ ((;;;1464
· ;11) + 1) = ;;;;16105 | 
| 253 | 152, 211,
25, 212, 25, 25, 252, 164 | decmul1c 12798 | . . . . . 6
⊢ (;;;;14641 · ;11) = ;;;;;161051 | 
| 254 | 208, 253 | eqtri 2765 | . . . . 5
⊢ (;11↑5) = ;;;;;161051 | 
| 255 | 254 | eqcomi 2746 | . . . 4
⊢ ;;;;;161051 = (;11↑5) | 
| 256 | 149, 255 | breqtri 5168 | . . 3
⊢ (9
· (7↑5)) < (;11↑5) | 
| 257 |  | 7re 12359 | . . . . . 6
⊢ 7 ∈
ℝ | 
| 258 |  | 5nn 12352 | . . . . . . 7
⊢ 5 ∈
ℕ | 
| 259 | 258 | nnzi 12641 | . . . . . 6
⊢ 5 ∈
ℤ | 
| 260 |  | 7pos 12377 | . . . . . 6
⊢ 0 <
7 | 
| 261 | 257, 259,
260 | 3pm3.2i 1340 | . . . . 5
⊢ (7 ∈
ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) | 
| 262 |  | expgt0 14136 | . . . . 5
⊢ ((7
∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < 7) → 0 <
(7↑5)) | 
| 263 | 261, 262 | ax-mp 5 | . . . 4
⊢ 0 <
(7↑5) | 
| 264 |  | 9re 12365 | . . . . 5
⊢ 9 ∈
ℝ | 
| 265 |  | 1nn 12277 | . . . . . . . . 9
⊢ 1 ∈
ℕ | 
| 266 | 25, 265 | decnncl 12753 | . . . . . . . 8
⊢ ;11 ∈ ℕ | 
| 267 | 266 | nnrei 12275 | . . . . . . 7
⊢ ;11 ∈ ℝ | 
| 268 | 267, 102 | pm3.2i 470 | . . . . . 6
⊢ (;11 ∈ ℝ ∧ 5 ∈
ℕ0) | 
| 269 |  | reexpcl 14119 | . . . . . 6
⊢ ((;11 ∈ ℝ ∧ 5 ∈
ℕ0) → (;11↑5) ∈ ℝ) | 
| 270 | 268, 269 | ax-mp 5 | . . . . 5
⊢ (;11↑5) ∈
ℝ | 
| 271 | 257, 102 | pm3.2i 470 | . . . . . 6
⊢ (7 ∈
ℝ ∧ 5 ∈ ℕ0) | 
| 272 |  | reexpcl 14119 | . . . . . 6
⊢ ((7
∈ ℝ ∧ 5 ∈ ℕ0) → (7↑5) ∈
ℝ) | 
| 273 | 271, 272 | ax-mp 5 | . . . . 5
⊢
(7↑5) ∈ ℝ | 
| 274 | 264, 270,
273 | ltmuldivi 12188 | . . . 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 230 | . 2
⊢ 9 <
((;11↑5) /
(7↑5)) | 
| 277 | 153 | a1i 11 | . . . . 5
⊢ (⊤
→ ;11 ∈
ℂ) | 
| 278 | 8 | a1i 11 | . . . . 5
⊢ (⊤
→ 7 ∈ ℂ) | 
| 279 |  | 0red 11264 | . . . . . . 7
⊢ (⊤
→ 0 ∈ ℝ) | 
| 280 | 260 | a1i 11 | . . . . . . 7
⊢ (⊤
→ 0 < 7) | 
| 281 | 279, 280 | ltned 11397 | . . . . . 6
⊢ (⊤
→ 0 ≠ 7) | 
| 282 | 281 | necomd 2996 | . . . . 5
⊢ (⊤
→ 7 ≠ 0) | 
| 283 | 102 | a1i 11 | . . . . 5
⊢ (⊤
→ 5 ∈ ℕ0) | 
| 284 | 277, 278,
282, 283 | expdivd 14200 | . . . 4
⊢ (⊤
→ ((;11 / 7)↑5) =
((;11↑5) /
(7↑5))) | 
| 285 | 284 | eqcomd 2743 | . . 3
⊢ (⊤
→ ((;11↑5) / (7↑5))
= ((;11 /
7)↑5)) | 
| 286 | 285 | mptru 1547 | . 2
⊢ ((;11↑5) / (7↑5)) = ((;11 / 7)↑5) | 
| 287 | 276, 286 | breqtri 5168 | 1
⊢ 9 <
((;11 /
7)↑5) |