Theorem 3lexlogpow5ineq5

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

	Ref	Expression
Assertion	3lexlogpow5ineq5	$$⊢{{\log }_{2}3}^5\le 15$$

Proof

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