Proof of Theorem 3lexlogpow5ineq5
| Step | Hyp | Ref
| Expression |
| 1 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 2 | 1 | a1i 11 |
. . . . 5
⊢ (⊤
→ 2 ∈ ℝ) |
| 3 | | 2pos 12369 |
. . . . . 6
⊢ 0 <
2 |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (⊤
→ 0 < 2) |
| 5 | | 3re 12346 |
. . . . . 6
⊢ 3 ∈
ℝ |
| 6 | 5 | a1i 11 |
. . . . 5
⊢ (⊤
→ 3 ∈ ℝ) |
| 7 | | 3pos 12371 |
. . . . . 6
⊢ 0 <
3 |
| 8 | 7 | a1i 11 |
. . . . 5
⊢ (⊤
→ 0 < 3) |
| 9 | | 1red 11262 |
. . . . . . 7
⊢ (⊤
→ 1 ∈ ℝ) |
| 10 | | 1lt2 12437 |
. . . . . . . 8
⊢ 1 <
2 |
| 11 | 10 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 1 < 2) |
| 12 | 9, 11 | ltned 11397 |
. . . . . 6
⊢ (⊤
→ 1 ≠ 2) |
| 13 | 12 | necomd 2996 |
. . . . 5
⊢ (⊤
→ 2 ≠ 1) |
| 14 | 2, 4, 6, 8, 13 | relogbcld 41974 |
. . . 4
⊢ (⊤
→ (2 logb 3) ∈ ℝ) |
| 15 | | 5nn0 12546 |
. . . . 5
⊢ 5 ∈
ℕ0 |
| 16 | 15 | a1i 11 |
. . . 4
⊢ (⊤
→ 5 ∈ ℕ0) |
| 17 | 14, 16 | reexpcld 14203 |
. . 3
⊢ (⊤
→ ((2 logb 3)↑5) ∈ ℝ) |
| 18 | 16 | nn0red 12588 |
. . . . 5
⊢ (⊤
→ 5 ∈ ℝ) |
| 19 | 8 | gt0ne0d 11827 |
. . . . 5
⊢ (⊤
→ 3 ≠ 0) |
| 20 | 18, 6, 19 | redivcld 12095 |
. . . 4
⊢ (⊤
→ (5 / 3) ∈ ℝ) |
| 21 | 20, 16 | reexpcld 14203 |
. . 3
⊢ (⊤
→ ((5 / 3)↑5) ∈ ℝ) |
| 22 | | 1nn0 12542 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
| 23 | | 5nn 12352 |
. . . . . 6
⊢ 5 ∈
ℕ |
| 24 | 22, 23 | decnncl 12753 |
. . . . 5
⊢ ;15 ∈ ℕ |
| 25 | 24 | a1i 11 |
. . . 4
⊢ (⊤
→ ;15 ∈
ℕ) |
| 26 | 25 | nnred 12281 |
. . 3
⊢ (⊤
→ ;15 ∈
ℝ) |
| 27 | | 0red 11264 |
. . . . 5
⊢ (⊤
→ 0 ∈ ℝ) |
| 28 | 6 | rehalfcld 12513 |
. . . . . 6
⊢ (⊤
→ (3 / 2) ∈ ℝ) |
| 29 | 6, 2, 8, 4 | divgt0d 12203 |
. . . . . 6
⊢ (⊤
→ 0 < (3 / 2)) |
| 30 | | 3lexlogpow2ineq1 42059 |
. . . . . . . 8
⊢ ((3 / 2)
< (2 logb 3) ∧ (2 logb 3) < (5 /
3)) |
| 31 | 30 | simpli 483 |
. . . . . . 7
⊢ (3 / 2)
< (2 logb 3) |
| 32 | 31 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (3 / 2) < (2 logb 3)) |
| 33 | 27, 28, 14, 29, 32 | lttrd 11422 |
. . . . 5
⊢ (⊤
→ 0 < (2 logb 3)) |
| 34 | 27, 14, 33 | ltled 11409 |
. . . 4
⊢ (⊤
→ 0 ≤ (2 logb 3)) |
| 35 | 30 | simpri 485 |
. . . . . 6
⊢ (2
logb 3) < (5 / 3) |
| 36 | 35 | a1i 11 |
. . . . 5
⊢ (⊤
→ (2 logb 3) < (5 / 3)) |
| 37 | 14, 20, 36 | ltled 11409 |
. . . 4
⊢ (⊤
→ (2 logb 3) ≤ (5 / 3)) |
| 38 | 14, 20, 16, 34, 37 | leexp1ad 41973 |
. . 3
⊢ (⊤
→ ((2 logb 3)↑5) ≤ ((5 / 3)↑5)) |
| 39 | | df-5 12332 |
. . . . . . 7
⊢ 5 = (4 +
1) |
| 40 | 39 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 5 = (4 + 1)) |
| 41 | 40 | oveq2d 7447 |
. . . . 5
⊢ (⊤
→ ((5 / 3)↑5) = ((5 / 3)↑(4 + 1))) |
| 42 | 20 | recnd 11289 |
. . . . . 6
⊢ (⊤
→ (5 / 3) ∈ ℂ) |
| 43 | | 4nn0 12545 |
. . . . . . 7
⊢ 4 ∈
ℕ0 |
| 44 | 43 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 4 ∈ ℕ0) |
| 45 | 42, 44 | expp1d 14187 |
. . . . 5
⊢ (⊤
→ ((5 / 3)↑(4 + 1)) = (((5 / 3)↑4) · (5 /
3))) |
| 46 | 41, 45 | eqtrd 2777 |
. . . 4
⊢ (⊤
→ ((5 / 3)↑5) = (((5 / 3)↑4) · (5 / 3))) |
| 47 | | 6nn0 12547 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℕ0 |
| 48 | | 2nn0 12543 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
| 49 | 47, 48 | deccl 12748 |
. . . . . . . . . . 11
⊢ ;62 ∈
ℕ0 |
| 50 | | 7nn0 12548 |
. . . . . . . . . . . 12
⊢ 7 ∈
ℕ0 |
| 51 | 50, 48 | deccl 12748 |
. . . . . . . . . . 11
⊢ ;72 ∈
ℕ0 |
| 52 | | 9nn0 12550 |
. . . . . . . . . . 11
⊢ 9 ∈
ℕ0 |
| 53 | | 9re 12365 |
. . . . . . . . . . . . . 14
⊢ 9 ∈
ℝ |
| 54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 9 ∈ ℝ) |
| 55 | | 5lt9 12468 |
. . . . . . . . . . . . . 14
⊢ 5 <
9 |
| 56 | 55 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 5 < 9) |
| 57 | 18, 54, 56 | ltled 11409 |
. . . . . . . . . . . 12
⊢ (⊤
→ 5 ≤ 9) |
| 58 | 57 | mptru 1547 |
. . . . . . . . . . 11
⊢ 5 ≤
9 |
| 59 | | 2lt10 12871 |
. . . . . . . . . . . 12
⊢ 2 <
;10 |
| 60 | | 6lt7 12452 |
. . . . . . . . . . . 12
⊢ 6 <
7 |
| 61 | 47, 50, 48, 48, 59, 60 | decltc 12762 |
. . . . . . . . . . 11
⊢ ;62 < ;72 |
| 62 | 49, 51, 15, 52, 58, 61 | decleh 12768 |
. . . . . . . . . 10
⊢ ;;625 ≤ ;;729 |
| 63 | 62 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ ;;625 ≤ ;;729) |
| 64 | | 8nn0 12549 |
. . . . . . . . . . . 12
⊢ 8 ∈
ℕ0 |
| 65 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ;81 = ;81 |
| 66 | | 0nn0 12541 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
| 67 | | 9cn 12366 |
. . . . . . . . . . . . . 14
⊢ 9 ∈
ℂ |
| 68 | | 8cn 12363 |
. . . . . . . . . . . . . 14
⊢ 8 ∈
ℂ |
| 69 | | 9t8e72 12861 |
. . . . . . . . . . . . . 14
⊢ (9
· 8) = ;72 |
| 70 | 67, 68, 69 | mulcomli 11270 |
. . . . . . . . . . . . 13
⊢ (8
· 9) = ;72 |
| 71 | | 2cn 12341 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
| 72 | 71 | addridi 11448 |
. . . . . . . . . . . . 13
⊢ (2 + 0) =
2 |
| 73 | 50, 48, 66, 70, 72 | decaddi 12793 |
. . . . . . . . . . . 12
⊢ ((8
· 9) + 0) = ;72 |
| 74 | | ax-1cn 11213 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
| 75 | 67 | mulridi 11265 |
. . . . . . . . . . . . . 14
⊢ (9
· 1) = 9 |
| 76 | 52 | dec0h 12755 |
. . . . . . . . . . . . . . 15
⊢ 9 = ;09 |
| 77 | 76 | eqcomi 2746 |
. . . . . . . . . . . . . 14
⊢ ;09 = 9 |
| 78 | 75, 77 | eqtr4i 2768 |
. . . . . . . . . . . . 13
⊢ (9
· 1) = ;09 |
| 79 | 67, 74, 78 | mulcomli 11270 |
. . . . . . . . . . . 12
⊢ (1
· 9) = ;09 |
| 80 | 52, 64, 22, 65, 52, 66, 73, 79 | decmul1c 12798 |
. . . . . . . . . . 11
⊢ (;81 · 9) = ;;729 |
| 81 | 80 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (;81 · 9) = ;;729) |
| 82 | 81 | eqcomd 2743 |
. . . . . . . . 9
⊢ (⊤
→ ;;729 = (;81 · 9)) |
| 83 | 63, 82 | breqtrd 5169 |
. . . . . . . 8
⊢ (⊤
→ ;;625 ≤ (;81 · 9)) |
| 84 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ 4 =
4 |
| 85 | | 2p2e4 12401 |
. . . . . . . . . . . . 13
⊢ (2 + 2) =
4 |
| 86 | 84, 85 | eqtr4i 2768 |
. . . . . . . . . . . 12
⊢ 4 = (2 +
2) |
| 87 | 86 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 4 = (2 + 2)) |
| 88 | 87 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (⊤
→ (5↑4) = (5↑(2 + 2))) |
| 89 | 23 | nncni 12276 |
. . . . . . . . . . . 12
⊢ 5 ∈
ℂ |
| 90 | 89 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 5 ∈ ℂ) |
| 91 | 48 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 2 ∈ ℕ0) |
| 92 | 90, 91, 91 | expaddd 14188 |
. . . . . . . . . 10
⊢ (⊤
→ (5↑(2 + 2)) = ((5↑2) · (5↑2))) |
| 93 | 89 | sqvali 14219 |
. . . . . . . . . . . . 13
⊢
(5↑2) = (5 · 5) |
| 94 | | 5t5e25 12836 |
. . . . . . . . . . . . 13
⊢ (5
· 5) = ;25 |
| 95 | 93, 94 | eqtri 2765 |
. . . . . . . . . . . 12
⊢
(5↑2) = ;25 |
| 96 | 95 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (5↑2) = ;25) |
| 97 | 96, 96 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (⊤
→ ((5↑2) · (5↑2)) = (;25 · ;25)) |
| 98 | 88, 92, 97 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (⊤
→ (5↑4) = (;25 ·
;25)) |
| 99 | 48, 15 | deccl 12748 |
. . . . . . . . . . 11
⊢ ;25 ∈
ℕ0 |
| 100 | | eqid 2737 |
. . . . . . . . . . 11
⊢ ;25 = ;25 |
| 101 | 22, 48 | deccl 12748 |
. . . . . . . . . . 11
⊢ ;12 ∈
ℕ0 |
| 102 | 48 | dec0h 12755 |
. . . . . . . . . . . 12
⊢ 2 = ;02 |
| 103 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ;12 = ;12 |
| 104 | 99 | nn0cni 12538 |
. . . . . . . . . . . . . . 15
⊢ ;25 ∈ ℂ |
| 105 | 104 | mul02i 11450 |
. . . . . . . . . . . . . 14
⊢ (0
· ;25) = 0 |
| 106 | | 5p1e6 12413 |
. . . . . . . . . . . . . . 15
⊢ (5 + 1) =
6 |
| 107 | 89, 74, 106 | addcomli 11453 |
. . . . . . . . . . . . . 14
⊢ (1 + 5) =
6 |
| 108 | 105, 107 | oveq12i 7443 |
. . . . . . . . . . . . 13
⊢ ((0
· ;25) + (1 + 5)) = (0 +
6) |
| 109 | | 6cn 12357 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℂ |
| 110 | 109 | addlidi 11449 |
. . . . . . . . . . . . 13
⊢ (0 + 6) =
6 |
| 111 | 108, 110 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((0
· ;25) + (1 + 5)) =
6 |
| 112 | | 2t2e4 12430 |
. . . . . . . . . . . . . . 15
⊢ (2
· 2) = 4 |
| 113 | | 0p1e1 12388 |
. . . . . . . . . . . . . . 15
⊢ (0 + 1) =
1 |
| 114 | 112, 113 | oveq12i 7443 |
. . . . . . . . . . . . . 14
⊢ ((2
· 2) + (0 + 1)) = (4 + 1) |
| 115 | | 4p1e5 12412 |
. . . . . . . . . . . . . 14
⊢ (4 + 1) =
5 |
| 116 | 114, 115 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ((2
· 2) + (0 + 1)) = 5 |
| 117 | | 5t2e10 12833 |
. . . . . . . . . . . . . . 15
⊢ (5
· 2) = ;10 |
| 118 | 89, 71, 117 | mulcomli 11270 |
. . . . . . . . . . . . . 14
⊢ (2
· 5) = ;10 |
| 119 | 71 | addlidi 11449 |
. . . . . . . . . . . . . 14
⊢ (0 + 2) =
2 |
| 120 | 22, 66, 48, 118, 119 | decaddi 12793 |
. . . . . . . . . . . . 13
⊢ ((2
· 5) + 2) = ;12 |
| 121 | 48, 15, 66, 48, 100, 102, 48, 48, 22, 116, 120 | decma2c 12786 |
. . . . . . . . . . . 12
⊢ ((2
· ;25) + 2) = ;52 |
| 122 | 66, 48, 22, 48, 102, 103, 99, 48, 15, 111, 121 | decmac 12785 |
. . . . . . . . . . 11
⊢ ((2
· ;25) + ;12) = ;62 |
| 123 | 22, 66, 48, 117, 119 | decaddi 12793 |
. . . . . . . . . . . 12
⊢ ((5
· 2) + 2) = ;12 |
| 124 | 15, 48, 15, 100, 15, 48, 123, 94 | decmul2c 12799 |
. . . . . . . . . . 11
⊢ (5
· ;25) = ;;125 |
| 125 | 99, 48, 15, 100, 15, 101, 122, 124 | decmul1c 12798 |
. . . . . . . . . 10
⊢ (;25 · ;25) = ;;625 |
| 126 | 125 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (;25 · ;25) = ;;625) |
| 127 | 98, 126 | eqtr2d 2778 |
. . . . . . . 8
⊢ (⊤
→ ;;625 = (5↑4)) |
| 128 | 87 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (⊤
→ (3↑4) = (3↑(2 + 2))) |
| 129 | | 3cn 12347 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
| 130 | 129 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 3 ∈ ℂ) |
| 131 | 130, 91, 91 | expaddd 14188 |
. . . . . . . . . . 11
⊢ (⊤
→ (3↑(2 + 2)) = ((3↑2) · (3↑2))) |
| 132 | 129 | sqvali 14219 |
. . . . . . . . . . . . . . 15
⊢
(3↑2) = (3 · 3) |
| 133 | | 3t3e9 12433 |
. . . . . . . . . . . . . . 15
⊢ (3
· 3) = 9 |
| 134 | 132, 133 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢
(3↑2) = 9 |
| 135 | 134 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (3↑2) = 9) |
| 136 | 135, 135 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (⊤
→ ((3↑2) · (3↑2)) = (9 · 9)) |
| 137 | | 9t9e81 12862 |
. . . . . . . . . . . . 13
⊢ (9
· 9) = ;81 |
| 138 | 137 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ (9 · 9) = ;81) |
| 139 | 136, 138 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (⊤
→ ((3↑2) · (3↑2)) = ;81) |
| 140 | 128, 131,
139 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ (⊤
→ (3↑4) = ;81) |
| 141 | 140 | eqcomd 2743 |
. . . . . . . . 9
⊢ (⊤
→ ;81 =
(3↑4)) |
| 142 | 141 | oveq1d 7446 |
. . . . . . . 8
⊢ (⊤
→ (;81 · 9) =
((3↑4) · 9)) |
| 143 | 83, 127, 142 | 3brtr3d 5174 |
. . . . . . 7
⊢ (⊤
→ (5↑4) ≤ ((3↑4) · 9)) |
| 144 | 18, 44 | reexpcld 14203 |
. . . . . . . 8
⊢ (⊤
→ (5↑4) ∈ ℝ) |
| 145 | | 3rp 13040 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ+ |
| 146 | 145 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 3 ∈ ℝ+) |
| 147 | | 4z 12651 |
. . . . . . . . . 10
⊢ 4 ∈
ℤ |
| 148 | 147 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 4 ∈ ℤ) |
| 149 | 146, 148 | rpexpcld 14286 |
. . . . . . . 8
⊢ (⊤
→ (3↑4) ∈ ℝ+) |
| 150 | 144, 54, 149 | ledivmuld 13130 |
. . . . . . 7
⊢ (⊤
→ (((5↑4) / (3↑4)) ≤ 9 ↔ (5↑4) ≤ ((3↑4)
· 9))) |
| 151 | 143, 150 | mpbird 257 |
. . . . . 6
⊢ (⊤
→ ((5↑4) / (3↑4)) ≤ 9) |
| 152 | 18 | recnd 11289 |
. . . . . . . 8
⊢ (⊤
→ 5 ∈ ℂ) |
| 153 | 152, 130,
19, 44 | expdivd 14200 |
. . . . . . 7
⊢ (⊤
→ ((5 / 3)↑4) = ((5↑4) / (3↑4))) |
| 154 | 153 | eqcomd 2743 |
. . . . . 6
⊢ (⊤
→ ((5↑4) / (3↑4)) = ((5 / 3)↑4)) |
| 155 | 26 | recnd 11289 |
. . . . . . . 8
⊢ (⊤
→ ;15 ∈
ℂ) |
| 156 | 23 | nngt0i 12305 |
. . . . . . . . . . 11
⊢ 0 <
5 |
| 157 | 156 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 0 < 5) |
| 158 | 27, 157 | ltned 11397 |
. . . . . . . . 9
⊢ (⊤
→ 0 ≠ 5) |
| 159 | 158 | necomd 2996 |
. . . . . . . 8
⊢ (⊤
→ 5 ≠ 0) |
| 160 | 155, 152,
130, 159, 19 | divdiv2d 12075 |
. . . . . . 7
⊢ (⊤
→ (;15 / (5 / 3)) = ((;15 · 3) / 5)) |
| 161 | | 5cn 12354 |
. . . . . . . . . . 11
⊢ 5 ∈
ℂ |
| 162 | | 9t5e45 12858 |
. . . . . . . . . . 11
⊢ (9
· 5) = ;45 |
| 163 | 67, 161, 162 | mulcomli 11270 |
. . . . . . . . . 10
⊢ (5
· 9) = ;45 |
| 164 | 163 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (5 · 9) = ;45) |
| 165 | | 3nn0 12544 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℕ0 |
| 166 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ;15 = ;15 |
| 167 | 129 | mullidi 11266 |
. . . . . . . . . . . . . 14
⊢ (1
· 3) = 3 |
| 168 | 167 | oveq1i 7441 |
. . . . . . . . . . . . 13
⊢ ((1
· 3) + 1) = (3 + 1) |
| 169 | | 3p1e4 12411 |
. . . . . . . . . . . . 13
⊢ (3 + 1) =
4 |
| 170 | 168, 169 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ ((1
· 3) + 1) = 4 |
| 171 | | 5t3e15 12834 |
. . . . . . . . . . . 12
⊢ (5
· 3) = ;15 |
| 172 | 165, 22, 15, 166, 15, 22, 170, 171 | decmul1c 12798 |
. . . . . . . . . . 11
⊢ (;15 · 3) = ;45 |
| 173 | 172 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (;15 · 3) = ;45) |
| 174 | 173 | eqcomd 2743 |
. . . . . . . . 9
⊢ (⊤
→ ;45 = (;15 · 3)) |
| 175 | 164, 174 | eqtrd 2777 |
. . . . . . . 8
⊢ (⊤
→ (5 · 9) = (;15
· 3)) |
| 176 | 155, 130 | mulcld 11281 |
. . . . . . . . 9
⊢ (⊤
→ (;15 · 3) ∈
ℂ) |
| 177 | 67 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 9 ∈ ℂ) |
| 178 | 176, 152,
177, 159 | divmuld 12065 |
. . . . . . . 8
⊢ (⊤
→ (((;15 · 3) / 5) = 9
↔ (5 · 9) = (;15
· 3))) |
| 179 | 175, 178 | mpbird 257 |
. . . . . . 7
⊢ (⊤
→ ((;15 · 3) / 5) =
9) |
| 180 | 160, 179 | eqtr2d 2778 |
. . . . . 6
⊢ (⊤
→ 9 = (;15 / (5 /
3))) |
| 181 | 151, 154,
180 | 3brtr3d 5174 |
. . . . 5
⊢ (⊤
→ ((5 / 3)↑4) ≤ (;15
/ (5 / 3))) |
| 182 | 20, 44 | reexpcld 14203 |
. . . . . 6
⊢ (⊤
→ ((5 / 3)↑4) ∈ ℝ) |
| 183 | 18, 157 | elrpd 13074 |
. . . . . . 7
⊢ (⊤
→ 5 ∈ ℝ+) |
| 184 | 183, 146 | rpdivcld 13094 |
. . . . . 6
⊢ (⊤
→ (5 / 3) ∈ ℝ+) |
| 185 | 182, 26, 184 | lemuldivd 13126 |
. . . . 5
⊢ (⊤
→ ((((5 / 3)↑4) · (5 / 3)) ≤ ;15 ↔ ((5 / 3)↑4) ≤ (;15 / (5 / 3)))) |
| 186 | 181, 185 | mpbird 257 |
. . . 4
⊢ (⊤
→ (((5 / 3)↑4) · (5 / 3)) ≤ ;15) |
| 187 | 46, 186 | eqbrtrd 5165 |
. . 3
⊢ (⊤
→ ((5 / 3)↑5) ≤ ;15) |
| 188 | 17, 21, 26, 38, 187 | letrd 11418 |
. 2
⊢ (⊤
→ ((2 logb 3)↑5) ≤ ;15) |
| 189 | 188 | mptru 1547 |
1
⊢ ((2
logb 3)↑5) ≤ ;15 |