Metamath Proof Explorer

Theorem 3lexlogpow5ineq5

Description: Result for bound in AKS inequality lemma. (Contributed by metakunt, 21-Aug-2024)

Ref Expression
Assertion 3lexlogpow5ineq5 ( ( 2 logb 3 ) ↑ 5 ) ≤ 1 5

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 1 a1i ⊢ ( ⊤ → 2 ∈ ℝ )
3 2pos ⊢ 0 < 2
4 3 a1i ⊢ ( ⊤ → 0 < 2 )
5 3re ⊢ 3 ∈ ℝ
6 5 a1i ⊢ ( ⊤ → 3 ∈ ℝ )
7 3pos ⊢ 0 < 3
8 7 a1i ⊢ ( ⊤ → 0 < 3 )
9 1red ⊢ ( ⊤ → 1 ∈ ℝ )
10 1lt2 ⊢ 1 < 2
11 10 a1i ⊢ ( ⊤ → 1 < 2 )
12 9 11 ltned ⊢ ( ⊤ → 1 ≠ 2 )
13 12 necomd ⊢ ( ⊤ → 2 ≠ 1 )
14 2 4 6 8 13 relogbcld ⊢ ( ⊤ → ( 2 logb 3 ) ∈ ℝ )
15 5nn0 ⊢ 5 ∈ ℕ0
16 15 a1i ⊢ ( ⊤ → 5 ∈ ℕ0 )
17 14 16 reexpcld ⊢ ( ⊤ → ( ( 2 logb 3 ) ↑ 5 ) ∈ ℝ )
18 16 nn0red ⊢ ( ⊤ → 5 ∈ ℝ )
19 8 gt0ne0d ⊢ ( ⊤ → 3 ≠ 0 )
20 18 6 19 redivcld ⊢ ( ⊤ → ( 5 / 3 ) ∈ ℝ )
21 20 16 reexpcld ⊢ ( ⊤ → ( ( 5 / 3 ) ↑ 5 ) ∈ ℝ )
22 1nn0 ⊢ 1 ∈ ℕ0
23 5nn ⊢ 5 ∈ ℕ
24 22 23 decnncl ⊢ 1 5 ∈ ℕ
25 24 a1i ⊢ ( ⊤ → 1 5 ∈ ℕ )
26 25 nnred ⊢ ( ⊤ → 1 5 ∈ ℝ )
27 0red ⊢ ( ⊤ → 0 ∈ ℝ )
28 6 rehalfcld ⊢ ( ⊤ → ( 3 / 2 ) ∈ ℝ )
29 6 2 8 4 divgt0d ⊢ ( ⊤ → 0 < ( 3 / 2 ) )
30 3lexlogpow2ineq1 ⊢ ( ( 3 / 2 ) < ( 2 logb 3 ) ∧ ( 2 logb 3 ) < ( 5 / 3 ) )
31 30 simpli ⊢ ( 3 / 2 ) < ( 2 logb 3 )
32 31 a1i ⊢ ( ⊤ → ( 3 / 2 ) < ( 2 logb 3 ) )
33 27 28 14 29 32 lttrd ⊢ ( ⊤ → 0 < ( 2 logb 3 ) )
34 27 14 33 ltled ⊢ ( ⊤ → 0 ≤ ( 2 logb 3 ) )
35 30 simpri ⊢ ( 2 logb 3 ) < ( 5 / 3 )
36 35 a1i ⊢ ( ⊤ → ( 2 logb 3 ) < ( 5 / 3 ) )
37 14 20 36 ltled ⊢ ( ⊤ → ( 2 logb 3 ) ≤ ( 5 / 3 ) )
38 14 20 16 34 37 leexp1ad ⊢ ( ⊤ → ( ( 2 logb 3 ) ↑ 5 ) ≤ ( ( 5 / 3 ) ↑ 5 ) )
39 df-5 ⊢ 5 = ( 4 + 1 )
40 39 a1i ⊢ ( ⊤ → 5 = ( 4 + 1 ) )
41 40 oveq2d ⊢ ( ⊤ → ( ( 5 / 3 ) ↑ 5 ) = ( ( 5 / 3 ) ↑ ( 4 + 1 ) ) )
42 20 recnd ⊢ ( ⊤ → ( 5 / 3 ) ∈ ℂ )
43 4nn0 ⊢ 4 ∈ ℕ0
44 43 a1i ⊢ ( ⊤ → 4 ∈ ℕ0 )
45 42 44 expp1d ⊢ ( ⊤ → ( ( 5 / 3 ) ↑ ( 4 + 1 ) ) = ( ( ( 5 / 3 ) ↑ 4 ) · ( 5 / 3 ) ) )
46 41 45 eqtrd ⊢ ( ⊤ → ( ( 5 / 3 ) ↑ 5 ) = ( ( ( 5 / 3 ) ↑ 4 ) · ( 5 / 3 ) ) )
47 6nn0 ⊢ 6 ∈ ℕ0
48 2nn0 ⊢ 2 ∈ ℕ0
49 47 48 deccl ⊢ 6 2 ∈ ℕ0
50 7nn0 ⊢ 7 ∈ ℕ0
51 50 48 deccl ⊢ 7 2 ∈ ℕ0
52 9nn0 ⊢ 9 ∈ ℕ0
53 9re ⊢ 9 ∈ ℝ
54 53 a1i ⊢ ( ⊤ → 9 ∈ ℝ )
55 5lt9 ⊢ 5 < 9
56 55 a1i ⊢ ( ⊤ → 5 < 9 )
57 18 54 56 ltled ⊢ ( ⊤ → 5 ≤ 9 )
58 57 mptru ⊢ 5 ≤ 9
59 2lt10 ⊢ 2 < 1 0
60 6lt7 ⊢ 6 < 7
61 47 50 48 48 59 60 decltc ⊢ 6 2 < 7 2
62 49 51 15 52 58 61 decleh ⊢ 6 2 5 ≤ 7 2 9
63 62 a1i ⊢ ( ⊤ → 6 2 5 ≤ 7 2 9 )
64 8nn0 ⊢ 8 ∈ ℕ0
65 eqid ⊢ 8 1 = 8 1
66 0nn0 ⊢ 0 ∈ ℕ0
67 9cn ⊢ 9 ∈ ℂ
68 8cn ⊢ 8 ∈ ℂ
69 9t8e72 ⊢ ( 9 · 8 ) = 7 2
70 67 68 69 mulcomli ⊢ ( 8 · 9 ) = 7 2
71 2cn ⊢ 2 ∈ ℂ
72 71 addridi ⊢ ( 2 + 0 ) = 2
73 50 48 66 70 72 decaddi ⊢ ( ( 8 · 9 ) + 0 ) = 7 2
74 ax-1cn ⊢ 1 ∈ ℂ
75 67 mulridi ⊢ ( 9 · 1 ) = 9
76 52 dec0h ⊢ 9 = 0 9
77 76 eqcomi ⊢ 0 9 = 9
78 75 77 eqtr4i ⊢ ( 9 · 1 ) = 0 9
79 67 74 78 mulcomli ⊢ ( 1 · 9 ) = 0 9
80 52 64 22 65 52 66 73 79 decmul1c ⊢ ( 8 1 · 9 ) = 7 2 9
81 80 a1i ⊢ ( ⊤ → ( 8 1 · 9 ) = 7 2 9 )
82 81 eqcomd ⊢ ( ⊤ → 7 2 9 = ( 8 1 · 9 ) )
83 63 82 breqtrd ⊢ ( ⊤ → 6 2 5 ≤ ( 8 1 · 9 ) )
84 eqid ⊢ 4 = 4
85 2p2e4 ⊢ ( 2 + 2 ) = 4
86 84 85 eqtr4i ⊢ 4 = ( 2 + 2 )
87 86 a1i ⊢ ( ⊤ → 4 = ( 2 + 2 ) )
88 87 oveq2d ⊢ ( ⊤ → ( 5 ↑ 4 ) = ( 5 ↑ ( 2 + 2 ) ) )
89 23 nncni ⊢ 5 ∈ ℂ
90 89 a1i ⊢ ( ⊤ → 5 ∈ ℂ )
91 48 a1i ⊢ ( ⊤ → 2 ∈ ℕ0 )
92 90 91 91 expaddd ⊢ ( ⊤ → ( 5 ↑ ( 2 + 2 ) ) = ( ( 5 ↑ 2 ) · ( 5 ↑ 2 ) ) )
93 89 sqvali ⊢ ( 5 ↑ 2 ) = ( 5 · 5 )
94 5t5e25 ⊢ ( 5 · 5 ) = 2 5
95 93 94 eqtri ⊢ ( 5 ↑ 2 ) = 2 5
96 95 a1i ⊢ ( ⊤ → ( 5 ↑ 2 ) = 2 5 )
97 96 96 oveq12d ⊢ ( ⊤ → ( ( 5 ↑ 2 ) · ( 5 ↑ 2 ) ) = ( 2 5 · 2 5 ) )
98 88 92 97 3eqtrd ⊢ ( ⊤ → ( 5 ↑ 4 ) = ( 2 5 · 2 5 ) )
99 48 15 deccl ⊢ 2 5 ∈ ℕ0
100 eqid ⊢ 2 5 = 2 5
101 22 48 deccl ⊢ 1 2 ∈ ℕ0
102 48 dec0h ⊢ 2 = 0 2
103 eqid ⊢ 1 2 = 1 2
104 99 nn0cni ⊢ 2 5 ∈ ℂ
105 104 mul02i ⊢ ( 0 · 2 5 ) = 0
106 5p1e6 ⊢ ( 5 + 1 ) = 6
107 89 74 106 addcomli ⊢ ( 1 + 5 ) = 6
108 105 107 oveq12i ⊢ ( ( 0 · 2 5 ) + ( 1 + 5 ) ) = ( 0 + 6 )
109 6cn ⊢ 6 ∈ ℂ
110 109 addlidi ⊢ ( 0 + 6 ) = 6
111 108 110 eqtri ⊢ ( ( 0 · 2 5 ) + ( 1 + 5 ) ) = 6
112 2t2e4 ⊢ ( 2 · 2 ) = 4
113 0p1e1 ⊢ ( 0 + 1 ) = 1
114 112 113 oveq12i ⊢ ( ( 2 · 2 ) + ( 0 + 1 ) ) = ( 4 + 1 )
115 4p1e5 ⊢ ( 4 + 1 ) = 5
116 114 115 eqtri ⊢ ( ( 2 · 2 ) + ( 0 + 1 ) ) = 5
117 5t2e10 ⊢ ( 5 · 2 ) = 1 0
118 89 71 117 mulcomli ⊢ ( 2 · 5 ) = 1 0
119 71 addlidi ⊢ ( 0 + 2 ) = 2
120 22 66 48 118 119 decaddi ⊢ ( ( 2 · 5 ) + 2 ) = 1 2
121 48 15 66 48 100 102 48 48 22 116 120 decma2c ⊢ ( ( 2 · 2 5 ) + 2 ) = 5 2
122 66 48 22 48 102 103 99 48 15 111 121 decmac ⊢ ( ( 2 · 2 5 ) + 1 2 ) = 6 2
123 22 66 48 117 119 decaddi ⊢ ( ( 5 · 2 ) + 2 ) = 1 2
124 15 48 15 100 15 48 123 94 decmul2c ⊢ ( 5 · 2 5 ) = 1 2 5
125 99 48 15 100 15 101 122 124 decmul1c ⊢ ( 2 5 · 2 5 ) = 6 2 5
126 125 a1i ⊢ ( ⊤ → ( 2 5 · 2 5 ) = 6 2 5 )
127 98 126 eqtr2d ⊢ ( ⊤ → 6 2 5 = ( 5 ↑ 4 ) )
128 87 oveq2d ⊢ ( ⊤ → ( 3 ↑ 4 ) = ( 3 ↑ ( 2 + 2 ) ) )
129 3cn ⊢ 3 ∈ ℂ
130 129 a1i ⊢ ( ⊤ → 3 ∈ ℂ )
131 130 91 91 expaddd ⊢ ( ⊤ → ( 3 ↑ ( 2 + 2 ) ) = ( ( 3 ↑ 2 ) · ( 3 ↑ 2 ) ) )
132 129 sqvali ⊢ ( 3 ↑ 2 ) = ( 3 · 3 )
133 3t3e9 ⊢ ( 3 · 3 ) = 9
134 132 133 eqtri ⊢ ( 3 ↑ 2 ) = 9
135 134 a1i ⊢ ( ⊤ → ( 3 ↑ 2 ) = 9 )
136 135 135 oveq12d ⊢ ( ⊤ → ( ( 3 ↑ 2 ) · ( 3 ↑ 2 ) ) = ( 9 · 9 ) )
137 9t9e81 ⊢ ( 9 · 9 ) = 8 1
138 137 a1i ⊢ ( ⊤ → ( 9 · 9 ) = 8 1 )
139 136 138 eqtrd ⊢ ( ⊤ → ( ( 3 ↑ 2 ) · ( 3 ↑ 2 ) ) = 8 1 )
140 128 131 139 3eqtrd ⊢ ( ⊤ → ( 3 ↑ 4 ) = 8 1 )
141 140 eqcomd ⊢ ( ⊤ → 8 1 = ( 3 ↑ 4 ) )
142 141 oveq1d ⊢ ( ⊤ → ( 8 1 · 9 ) = ( ( 3 ↑ 4 ) · 9 ) )
143 83 127 142 3brtr3d ⊢ ( ⊤ → ( 5 ↑ 4 ) ≤ ( ( 3 ↑ 4 ) · 9 ) )
144 18 44 reexpcld ⊢ ( ⊤ → ( 5 ↑ 4 ) ∈ ℝ )
145 3rp ⊢ 3 ∈ ℝ+
146 145 a1i ⊢ ( ⊤ → 3 ∈ ℝ+ )
147 4z ⊢ 4 ∈ ℤ
148 147 a1i ⊢ ( ⊤ → 4 ∈ ℤ )
149 146 148 rpexpcld ⊢ ( ⊤ → ( 3 ↑ 4 ) ∈ ℝ+ )
150 144 54 149 ledivmuld ⊢ ( ⊤ → ( ( ( 5 ↑ 4 ) / ( 3 ↑ 4 ) ) ≤ 9 ↔ ( 5 ↑ 4 ) ≤ ( ( 3 ↑ 4 ) · 9 ) ) )
151 143 150 mpbird ⊢ ( ⊤ → ( ( 5 ↑ 4 ) / ( 3 ↑ 4 ) ) ≤ 9 )
152 18 recnd ⊢ ( ⊤ → 5 ∈ ℂ )
153 152 130 19 44 expdivd ⊢ ( ⊤ → ( ( 5 / 3 ) ↑ 4 ) = ( ( 5 ↑ 4 ) / ( 3 ↑ 4 ) ) )
154 153 eqcomd ⊢ ( ⊤ → ( ( 5 ↑ 4 ) / ( 3 ↑ 4 ) ) = ( ( 5 / 3 ) ↑ 4 ) )
155 26 recnd ⊢ ( ⊤ → 1 5 ∈ ℂ )
156 23 nngt0i ⊢ 0 < 5
157 156 a1i ⊢ ( ⊤ → 0 < 5 )
158 27 157 ltned ⊢ ( ⊤ → 0 ≠ 5 )
159 158 necomd ⊢ ( ⊤ → 5 ≠ 0 )
160 155 152 130 159 19 divdiv2d ⊢ ( ⊤ → ( 1 5 / ( 5 / 3 ) ) = ( ( 1 5 · 3 ) / 5 ) )
161 5cn ⊢ 5 ∈ ℂ
162 9t5e45 ⊢ ( 9 · 5 ) = 4 5
163 67 161 162 mulcomli ⊢ ( 5 · 9 ) = 4 5
164 163 a1i ⊢ ( ⊤ → ( 5 · 9 ) = 4 5 )
165 3nn0 ⊢ 3 ∈ ℕ0
166 eqid ⊢ 1 5 = 1 5
167 129 mullidi ⊢ ( 1 · 3 ) = 3
168 167 oveq1i ⊢ ( ( 1 · 3 ) + 1 ) = ( 3 + 1 )
169 3p1e4 ⊢ ( 3 + 1 ) = 4
170 168 169 eqtri ⊢ ( ( 1 · 3 ) + 1 ) = 4
171 5t3e15 ⊢ ( 5 · 3 ) = 1 5
172 165 22 15 166 15 22 170 171 decmul1c ⊢ ( 1 5 · 3 ) = 4 5
173 172 a1i ⊢ ( ⊤ → ( 1 5 · 3 ) = 4 5 )
174 173 eqcomd ⊢ ( ⊤ → 4 5 = ( 1 5 · 3 ) )
175 164 174 eqtrd ⊢ ( ⊤ → ( 5 · 9 ) = ( 1 5 · 3 ) )
176 155 130 mulcld ⊢ ( ⊤ → ( 1 5 · 3 ) ∈ ℂ )
177 67 a1i ⊢ ( ⊤ → 9 ∈ ℂ )
178 176 152 177 159 divmuld ⊢ ( ⊤ → ( ( ( 1 5 · 3 ) / 5 ) = 9 ↔ ( 5 · 9 ) = ( 1 5 · 3 ) ) )
179 175 178 mpbird ⊢ ( ⊤ → ( ( 1 5 · 3 ) / 5 ) = 9 )
180 160 179 eqtr2d ⊢ ( ⊤ → 9 = ( 1 5 / ( 5 / 3 ) ) )
181 151 154 180 3brtr3d ⊢ ( ⊤ → ( ( 5 / 3 ) ↑ 4 ) ≤ ( 1 5 / ( 5 / 3 ) ) )
182 20 44 reexpcld ⊢ ( ⊤ → ( ( 5 / 3 ) ↑ 4 ) ∈ ℝ )
183 18 157 elrpd ⊢ ( ⊤ → 5 ∈ ℝ+ )
184 183 146 rpdivcld ⊢ ( ⊤ → ( 5 / 3 ) ∈ ℝ+ )
185 182 26 184 lemuldivd ⊢ ( ⊤ → ( ( ( ( 5 / 3 ) ↑ 4 ) · ( 5 / 3 ) ) ≤ 1 5 ↔ ( ( 5 / 3 ) ↑ 4 ) ≤ ( 1 5 / ( 5 / 3 ) ) ) )
186 181 185 mpbird ⊢ ( ⊤ → ( ( ( 5 / 3 ) ↑ 4 ) · ( 5 / 3 ) ) ≤ 1 5 )
187 46 186 eqbrtrd ⊢ ( ⊤ → ( ( 5 / 3 ) ↑ 5 ) ≤ 1 5 )
188 17 21 26 38 187 letrd ⊢ ( ⊤ → ( ( 2 logb 3 ) ↑ 5 ) ≤ 1 5 )
189 188 mptru ⊢ ( ( 2 logb 3 ) ↑ 5 ) ≤ 1 5