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