Proof of Theorem 3lexlogpow5ineq5
Step | Hyp | Ref
| Expression |
1 | | 2re 11790 |
. . . . . 6
⊢ 2 ∈
ℝ |
2 | 1 | a1i 11 |
. . . . 5
⊢ (⊤
→ 2 ∈ ℝ) |
3 | | 2pos 11819 |
. . . . . 6
⊢ 0 <
2 |
4 | 3 | a1i 11 |
. . . . 5
⊢ (⊤
→ 0 < 2) |
5 | | 3re 11796 |
. . . . . 6
⊢ 3 ∈
ℝ |
6 | 5 | a1i 11 |
. . . . 5
⊢ (⊤
→ 3 ∈ ℝ) |
7 | | 3pos 11821 |
. . . . . 6
⊢ 0 <
3 |
8 | 7 | a1i 11 |
. . . . 5
⊢ (⊤
→ 0 < 3) |
9 | | 1red 10720 |
. . . . . . 7
⊢ (⊤
→ 1 ∈ ℝ) |
10 | | 1lt2 11887 |
. . . . . . . 8
⊢ 1 <
2 |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ 1 < 2) |
12 | 9, 11 | ltned 10854 |
. . . . . 6
⊢ (⊤
→ 1 ≠ 2) |
13 | 12 | necomd 2989 |
. . . . 5
⊢ (⊤
→ 2 ≠ 1) |
14 | 2, 4, 6, 8, 13 | relogbcld 39600 |
. . . 4
⊢ (⊤
→ (2 logb 3) ∈ ℝ) |
15 | | 5nn0 11996 |
. . . . 5
⊢ 5 ∈
ℕ0 |
16 | 15 | a1i 11 |
. . . 4
⊢ (⊤
→ 5 ∈ ℕ0) |
17 | 14, 16 | reexpcld 13619 |
. . 3
⊢ (⊤
→ ((2 logb 3)↑5) ∈ ℝ) |
18 | 16 | nn0red 12037 |
. . . . 5
⊢ (⊤
→ 5 ∈ ℝ) |
19 | 8 | gt0ne0d 11282 |
. . . . 5
⊢ (⊤
→ 3 ≠ 0) |
20 | 18, 6, 19 | redivcld 11546 |
. . . 4
⊢ (⊤
→ (5 / 3) ∈ ℝ) |
21 | 20, 16 | reexpcld 13619 |
. . 3
⊢ (⊤
→ ((5 / 3)↑5) ∈ ℝ) |
22 | | 1nn0 11992 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
23 | | 5nn 11802 |
. . . . . 6
⊢ 5 ∈
ℕ |
24 | 22, 23 | decnncl 12199 |
. . . . 5
⊢ ;15 ∈ ℕ |
25 | 24 | a1i 11 |
. . . 4
⊢ (⊤
→ ;15 ∈
ℕ) |
26 | 25 | nnred 11731 |
. . 3
⊢ (⊤
→ ;15 ∈
ℝ) |
27 | | 0red 10722 |
. . . . 5
⊢ (⊤
→ 0 ∈ ℝ) |
28 | 6 | rehalfcld 11963 |
. . . . . 6
⊢ (⊤
→ (3 / 2) ∈ ℝ) |
29 | 6, 2, 8, 4 | divgt0d 11653 |
. . . . . 6
⊢ (⊤
→ 0 < (3 / 2)) |
30 | | 3lexlogpow2ineq1 39686 |
. . . . . . . 8
⊢ ((3 / 2)
< (2 logb 3) ∧ (2 logb 3) < (5 /
3)) |
31 | 30 | simpli 487 |
. . . . . . 7
⊢ (3 / 2)
< (2 logb 3) |
32 | 31 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (3 / 2) < (2 logb 3)) |
33 | 27, 28, 14, 29, 32 | lttrd 10879 |
. . . . 5
⊢ (⊤
→ 0 < (2 logb 3)) |
34 | 27, 14, 33 | ltled 10866 |
. . . 4
⊢ (⊤
→ 0 ≤ (2 logb 3)) |
35 | 30 | simpri 489 |
. . . . . 6
⊢ (2
logb 3) < (5 / 3) |
36 | 35 | a1i 11 |
. . . . 5
⊢ (⊤
→ (2 logb 3) < (5 / 3)) |
37 | 14, 20, 36 | ltled 10866 |
. . . 4
⊢ (⊤
→ (2 logb 3) ≤ (5 / 3)) |
38 | 14, 20, 16, 34, 37 | leexp1ad 39599 |
. . 3
⊢ (⊤
→ ((2 logb 3)↑5) ≤ ((5 / 3)↑5)) |
39 | | df-5 11782 |
. . . . . . 7
⊢ 5 = (4 +
1) |
40 | 39 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 5 = (4 + 1)) |
41 | 40 | oveq2d 7186 |
. . . . 5
⊢ (⊤
→ ((5 / 3)↑5) = ((5 / 3)↑(4 + 1))) |
42 | 20 | recnd 10747 |
. . . . . 6
⊢ (⊤
→ (5 / 3) ∈ ℂ) |
43 | | 4nn0 11995 |
. . . . . . 7
⊢ 4 ∈
ℕ0 |
44 | 43 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 4 ∈ ℕ0) |
45 | 42, 44 | expp1d 13603 |
. . . . 5
⊢ (⊤
→ ((5 / 3)↑(4 + 1)) = (((5 / 3)↑4) · (5 /
3))) |
46 | 41, 45 | eqtrd 2773 |
. . . 4
⊢ (⊤
→ ((5 / 3)↑5) = (((5 / 3)↑4) · (5 / 3))) |
47 | | 6nn0 11997 |
. . . . . . . . . . . 12
⊢ 6 ∈
ℕ0 |
48 | | 2nn0 11993 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
49 | 47, 48 | deccl 12194 |
. . . . . . . . . . 11
⊢ ;62 ∈
ℕ0 |
50 | | 7nn0 11998 |
. . . . . . . . . . . 12
⊢ 7 ∈
ℕ0 |
51 | 50, 48 | deccl 12194 |
. . . . . . . . . . 11
⊢ ;72 ∈
ℕ0 |
52 | | 9nn0 12000 |
. . . . . . . . . . 11
⊢ 9 ∈
ℕ0 |
53 | | 9re 11815 |
. . . . . . . . . . . . . 14
⊢ 9 ∈
ℝ |
54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 9 ∈ ℝ) |
55 | | 5lt9 11918 |
. . . . . . . . . . . . . 14
⊢ 5 <
9 |
56 | 55 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 5 < 9) |
57 | 18, 54, 56 | ltled 10866 |
. . . . . . . . . . . 12
⊢ (⊤
→ 5 ≤ 9) |
58 | 57 | mptru 1549 |
. . . . . . . . . . 11
⊢ 5 ≤
9 |
59 | | 2lt10 12317 |
. . . . . . . . . . . 12
⊢ 2 <
;10 |
60 | | 6lt7 11902 |
. . . . . . . . . . . 12
⊢ 6 <
7 |
61 | 47, 50, 48, 48, 59, 60 | decltc 12208 |
. . . . . . . . . . 11
⊢ ;62 < ;72 |
62 | 49, 51, 15, 52, 58, 61 | decleh 12214 |
. . . . . . . . . 10
⊢ ;;625 ≤ ;;729 |
63 | 62 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ ;;625 ≤ ;;729) |
64 | | 8nn0 11999 |
. . . . . . . . . . . 12
⊢ 8 ∈
ℕ0 |
65 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ;81 = ;81 |
66 | | 0nn0 11991 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
67 | | 9cn 11816 |
. . . . . . . . . . . . . 14
⊢ 9 ∈
ℂ |
68 | | 8cn 11813 |
. . . . . . . . . . . . . 14
⊢ 8 ∈
ℂ |
69 | | 9t8e72 12307 |
. . . . . . . . . . . . . 14
⊢ (9
· 8) = ;72 |
70 | 67, 68, 69 | mulcomli 10728 |
. . . . . . . . . . . . 13
⊢ (8
· 9) = ;72 |
71 | | 2cn 11791 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℂ |
72 | 71 | addid1i 10905 |
. . . . . . . . . . . . 13
⊢ (2 + 0) =
2 |
73 | 50, 48, 66, 70, 72 | decaddi 12239 |
. . . . . . . . . . . 12
⊢ ((8
· 9) + 0) = ;72 |
74 | | ax-1cn 10673 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
75 | 67 | mulid1i 10723 |
. . . . . . . . . . . . . 14
⊢ (9
· 1) = 9 |
76 | 52 | dec0h 12201 |
. . . . . . . . . . . . . . 15
⊢ 9 = ;09 |
77 | 76 | eqcomi 2747 |
. . . . . . . . . . . . . 14
⊢ ;09 = 9 |
78 | 75, 77 | eqtr4i 2764 |
. . . . . . . . . . . . 13
⊢ (9
· 1) = ;09 |
79 | 67, 74, 78 | mulcomli 10728 |
. . . . . . . . . . . 12
⊢ (1
· 9) = ;09 |
80 | 52, 64, 22, 65, 52, 66, 73, 79 | decmul1c 12244 |
. . . . . . . . . . 11
⊢ (;81 · 9) = ;;729 |
81 | 80 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (;81 · 9) = ;;729) |
82 | 81 | eqcomd 2744 |
. . . . . . . . 9
⊢ (⊤
→ ;;729 = (;81 · 9)) |
83 | 63, 82 | breqtrd 5056 |
. . . . . . . 8
⊢ (⊤
→ ;;625 ≤ (;81 · 9)) |
84 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ 4 =
4 |
85 | | 2p2e4 11851 |
. . . . . . . . . . . . 13
⊢ (2 + 2) =
4 |
86 | 84, 85 | eqtr4i 2764 |
. . . . . . . . . . . 12
⊢ 4 = (2 +
2) |
87 | 86 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 4 = (2 + 2)) |
88 | 87 | oveq2d 7186 |
. . . . . . . . . 10
⊢ (⊤
→ (5↑4) = (5↑(2 + 2))) |
89 | 23 | nncni 11726 |
. . . . . . . . . . . 12
⊢ 5 ∈
ℂ |
90 | 89 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 5 ∈ ℂ) |
91 | 48 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ 2 ∈ ℕ0) |
92 | 90, 91, 91 | expaddd 13604 |
. . . . . . . . . 10
⊢ (⊤
→ (5↑(2 + 2)) = ((5↑2) · (5↑2))) |
93 | 89 | sqvali 13635 |
. . . . . . . . . . . . 13
⊢
(5↑2) = (5 · 5) |
94 | | 5t5e25 12282 |
. . . . . . . . . . . . 13
⊢ (5
· 5) = ;25 |
95 | 93, 94 | eqtri 2761 |
. . . . . . . . . . . 12
⊢
(5↑2) = ;25 |
96 | 95 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ (5↑2) = ;25) |
97 | 96, 96 | oveq12d 7188 |
. . . . . . . . . 10
⊢ (⊤
→ ((5↑2) · (5↑2)) = (;25 · ;25)) |
98 | 88, 92, 97 | 3eqtrd 2777 |
. . . . . . . . 9
⊢ (⊤
→ (5↑4) = (;25 ·
;25)) |
99 | 48, 15 | deccl 12194 |
. . . . . . . . . . 11
⊢ ;25 ∈
ℕ0 |
100 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ;25 = ;25 |
101 | 22, 48 | deccl 12194 |
. . . . . . . . . . 11
⊢ ;12 ∈
ℕ0 |
102 | 48 | dec0h 12201 |
. . . . . . . . . . . 12
⊢ 2 = ;02 |
103 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ;12 = ;12 |
104 | 99 | nn0cni 11988 |
. . . . . . . . . . . . . . 15
⊢ ;25 ∈ ℂ |
105 | 104 | mul02i 10907 |
. . . . . . . . . . . . . 14
⊢ (0
· ;25) = 0 |
106 | | 5p1e6 11863 |
. . . . . . . . . . . . . . 15
⊢ (5 + 1) =
6 |
107 | 89, 74, 106 | addcomli 10910 |
. . . . . . . . . . . . . 14
⊢ (1 + 5) =
6 |
108 | 105, 107 | oveq12i 7182 |
. . . . . . . . . . . . 13
⊢ ((0
· ;25) + (1 + 5)) = (0 +
6) |
109 | | 6cn 11807 |
. . . . . . . . . . . . . 14
⊢ 6 ∈
ℂ |
110 | 109 | addid2i 10906 |
. . . . . . . . . . . . 13
⊢ (0 + 6) =
6 |
111 | 108, 110 | eqtri 2761 |
. . . . . . . . . . . 12
⊢ ((0
· ;25) + (1 + 5)) =
6 |
112 | | 2t2e4 11880 |
. . . . . . . . . . . . . . 15
⊢ (2
· 2) = 4 |
113 | | 0p1e1 11838 |
. . . . . . . . . . . . . . 15
⊢ (0 + 1) =
1 |
114 | 112, 113 | oveq12i 7182 |
. . . . . . . . . . . . . 14
⊢ ((2
· 2) + (0 + 1)) = (4 + 1) |
115 | | 4p1e5 11862 |
. . . . . . . . . . . . . 14
⊢ (4 + 1) =
5 |
116 | 114, 115 | eqtri 2761 |
. . . . . . . . . . . . 13
⊢ ((2
· 2) + (0 + 1)) = 5 |
117 | | 5t2e10 12279 |
. . . . . . . . . . . . . . 15
⊢ (5
· 2) = ;10 |
118 | 89, 71, 117 | mulcomli 10728 |
. . . . . . . . . . . . . 14
⊢ (2
· 5) = ;10 |
119 | 71 | addid2i 10906 |
. . . . . . . . . . . . . 14
⊢ (0 + 2) =
2 |
120 | 22, 66, 48, 118, 119 | decaddi 12239 |
. . . . . . . . . . . . 13
⊢ ((2
· 5) + 2) = ;12 |
121 | 48, 15, 66, 48, 100, 102, 48, 48, 22, 116, 120 | decma2c 12232 |
. . . . . . . . . . . 12
⊢ ((2
· ;25) + 2) = ;52 |
122 | 66, 48, 22, 48, 102, 103, 99, 48, 15, 111, 121 | decmac 12231 |
. . . . . . . . . . 11
⊢ ((2
· ;25) + ;12) = ;62 |
123 | 22, 66, 48, 117, 119 | decaddi 12239 |
. . . . . . . . . . . 12
⊢ ((5
· 2) + 2) = ;12 |
124 | 15, 48, 15, 100, 15, 48, 123, 94 | decmul2c 12245 |
. . . . . . . . . . 11
⊢ (5
· ;25) = ;;125 |
125 | 99, 48, 15, 100, 15, 101, 122, 124 | decmul1c 12244 |
. . . . . . . . . 10
⊢ (;25 · ;25) = ;;625 |
126 | 125 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (;25 · ;25) = ;;625) |
127 | 98, 126 | eqtr2d 2774 |
. . . . . . . 8
⊢ (⊤
→ ;;625 = (5↑4)) |
128 | 87 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ (⊤
→ (3↑4) = (3↑(2 + 2))) |
129 | | 3cn 11797 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℂ |
130 | 129 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 3 ∈ ℂ) |
131 | 130, 91, 91 | expaddd 13604 |
. . . . . . . . . . 11
⊢ (⊤
→ (3↑(2 + 2)) = ((3↑2) · (3↑2))) |
132 | 129 | sqvali 13635 |
. . . . . . . . . . . . . . 15
⊢
(3↑2) = (3 · 3) |
133 | | 3t3e9 11883 |
. . . . . . . . . . . . . . 15
⊢ (3
· 3) = 9 |
134 | 132, 133 | eqtri 2761 |
. . . . . . . . . . . . . 14
⊢
(3↑2) = 9 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ (3↑2) = 9) |
136 | 135, 135 | oveq12d 7188 |
. . . . . . . . . . . 12
⊢ (⊤
→ ((3↑2) · (3↑2)) = (9 · 9)) |
137 | | 9t9e81 12308 |
. . . . . . . . . . . . 13
⊢ (9
· 9) = ;81 |
138 | 137 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ (9 · 9) = ;81) |
139 | 136, 138 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (⊤
→ ((3↑2) · (3↑2)) = ;81) |
140 | 128, 131,
139 | 3eqtrd 2777 |
. . . . . . . . . 10
⊢ (⊤
→ (3↑4) = ;81) |
141 | 140 | eqcomd 2744 |
. . . . . . . . 9
⊢ (⊤
→ ;81 =
(3↑4)) |
142 | 141 | oveq1d 7185 |
. . . . . . . 8
⊢ (⊤
→ (;81 · 9) =
((3↑4) · 9)) |
143 | 83, 127, 142 | 3brtr3d 5061 |
. . . . . . 7
⊢ (⊤
→ (5↑4) ≤ ((3↑4) · 9)) |
144 | 18, 44 | reexpcld 13619 |
. . . . . . . 8
⊢ (⊤
→ (5↑4) ∈ ℝ) |
145 | | 3rp 12478 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ+ |
146 | 145 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 3 ∈ ℝ+) |
147 | | 4z 12097 |
. . . . . . . . . 10
⊢ 4 ∈
ℤ |
148 | 147 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 4 ∈ ℤ) |
149 | 146, 148 | rpexpcld 13700 |
. . . . . . . 8
⊢ (⊤
→ (3↑4) ∈ ℝ+) |
150 | 144, 54, 149 | ledivmuld 12567 |
. . . . . . 7
⊢ (⊤
→ (((5↑4) / (3↑4)) ≤ 9 ↔ (5↑4) ≤ ((3↑4)
· 9))) |
151 | 143, 150 | mpbird 260 |
. . . . . 6
⊢ (⊤
→ ((5↑4) / (3↑4)) ≤ 9) |
152 | 18 | recnd 10747 |
. . . . . . . 8
⊢ (⊤
→ 5 ∈ ℂ) |
153 | 152, 130,
19, 44 | expdivd 13616 |
. . . . . . 7
⊢ (⊤
→ ((5 / 3)↑4) = ((5↑4) / (3↑4))) |
154 | 153 | eqcomd 2744 |
. . . . . 6
⊢ (⊤
→ ((5↑4) / (3↑4)) = ((5 / 3)↑4)) |
155 | 26 | recnd 10747 |
. . . . . . . 8
⊢ (⊤
→ ;15 ∈
ℂ) |
156 | 23 | nngt0i 11755 |
. . . . . . . . . . 11
⊢ 0 <
5 |
157 | 156 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ 0 < 5) |
158 | 27, 157 | ltned 10854 |
. . . . . . . . 9
⊢ (⊤
→ 0 ≠ 5) |
159 | 158 | necomd 2989 |
. . . . . . . 8
⊢ (⊤
→ 5 ≠ 0) |
160 | 155, 152,
130, 159, 19 | divdiv2d 11526 |
. . . . . . 7
⊢ (⊤
→ (;15 / (5 / 3)) = ((;15 · 3) / 5)) |
161 | | 5cn 11804 |
. . . . . . . . . . 11
⊢ 5 ∈
ℂ |
162 | | 9t5e45 12304 |
. . . . . . . . . . 11
⊢ (9
· 5) = ;45 |
163 | 67, 161, 162 | mulcomli 10728 |
. . . . . . . . . 10
⊢ (5
· 9) = ;45 |
164 | 163 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ (5 · 9) = ;45) |
165 | | 3nn0 11994 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℕ0 |
166 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ ;15 = ;15 |
167 | 129 | mulid2i 10724 |
. . . . . . . . . . . . . 14
⊢ (1
· 3) = 3 |
168 | 167 | oveq1i 7180 |
. . . . . . . . . . . . 13
⊢ ((1
· 3) + 1) = (3 + 1) |
169 | | 3p1e4 11861 |
. . . . . . . . . . . . 13
⊢ (3 + 1) =
4 |
170 | 168, 169 | eqtri 2761 |
. . . . . . . . . . . 12
⊢ ((1
· 3) + 1) = 4 |
171 | | 5t3e15 12280 |
. . . . . . . . . . . 12
⊢ (5
· 3) = ;15 |
172 | 165, 22, 15, 166, 15, 22, 170, 171 | decmul1c 12244 |
. . . . . . . . . . 11
⊢ (;15 · 3) = ;45 |
173 | 172 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ (;15 · 3) = ;45) |
174 | 173 | eqcomd 2744 |
. . . . . . . . 9
⊢ (⊤
→ ;45 = (;15 · 3)) |
175 | 164, 174 | eqtrd 2773 |
. . . . . . . 8
⊢ (⊤
→ (5 · 9) = (;15
· 3)) |
176 | 155, 130 | mulcld 10739 |
. . . . . . . . 9
⊢ (⊤
→ (;15 · 3) ∈
ℂ) |
177 | 67 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ 9 ∈ ℂ) |
178 | 176, 152,
177, 159 | divmuld 11516 |
. . . . . . . 8
⊢ (⊤
→ (((;15 · 3) / 5) = 9
↔ (5 · 9) = (;15
· 3))) |
179 | 175, 178 | mpbird 260 |
. . . . . . 7
⊢ (⊤
→ ((;15 · 3) / 5) =
9) |
180 | 160, 179 | eqtr2d 2774 |
. . . . . 6
⊢ (⊤
→ 9 = (;15 / (5 /
3))) |
181 | 151, 154,
180 | 3brtr3d 5061 |
. . . . 5
⊢ (⊤
→ ((5 / 3)↑4) ≤ (;15
/ (5 / 3))) |
182 | 20, 44 | reexpcld 13619 |
. . . . . 6
⊢ (⊤
→ ((5 / 3)↑4) ∈ ℝ) |
183 | 18, 157 | elrpd 12511 |
. . . . . . 7
⊢ (⊤
→ 5 ∈ ℝ+) |
184 | 183, 146 | rpdivcld 12531 |
. . . . . 6
⊢ (⊤
→ (5 / 3) ∈ ℝ+) |
185 | 182, 26, 184 | lemuldivd 12563 |
. . . . 5
⊢ (⊤
→ ((((5 / 3)↑4) · (5 / 3)) ≤ ;15 ↔ ((5 / 3)↑4) ≤ (;15 / (5 / 3)))) |
186 | 181, 185 | mpbird 260 |
. . . 4
⊢ (⊤
→ (((5 / 3)↑4) · (5 / 3)) ≤ ;15) |
187 | 46, 186 | eqbrtrd 5052 |
. . 3
⊢ (⊤
→ ((5 / 3)↑5) ≤ ;15) |
188 | 17, 21, 26, 38, 187 | letrd 10875 |
. 2
⊢ (⊤
→ ((2 logb 3)↑5) ≤ ;15) |
189 | 188 | mptru 1549 |
1
⊢ ((2
logb 3)↑5) ≤ ;15 |