Theorem 3lexlogpow2ineq1

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

	Ref	Expression
Assertion	3lexlogpow2ineq1	$$⊢\left(\frac{3}{2}<{\log }_{2}3\wedge {\log }_{2}3<\frac{5}{3}\right)$$

Proof

Step	Hyp	Ref	Expression
1		tru	$$⊢\top$$
2		8lt9	$$⊢8<9$$
3		2z	$$⊢2\in \mathbb{Z}$$
4		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
5	3 4	ax-mp	$$⊢2\in {\mathbb{Z}}_{\ge 2}$$
6		8nn	$$⊢8\in \mathbb{N}$$
7		nnrp	$$⊢8\in \mathbb{N}\to 8\in {ℝ}^{+}$$
8	6 7	ax-mp	$$⊢8\in {ℝ}^{+}$$
9		9nn	$$⊢9\in \mathbb{N}$$
10		nnrp	$$⊢9\in \mathbb{N}\to 9\in {ℝ}^{+}$$
11	9 10	ax-mp	$$⊢9\in {ℝ}^{+}$$
12	5 8 11	3pm3.2i	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge 8\in {ℝ}^{+}\wedge 9\in {ℝ}^{+}\right)$$
13		logblt	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge 8\in {ℝ}^{+}\wedge 9\in {ℝ}^{+}\right)\to \left(8<9\leftrightarrow {\log }_{2}8<{\log }_{2}9\right)$$
14	12 13	ax-mp	$$⊢8<9\leftrightarrow {\log }_{2}8<{\log }_{2}9$$
15	2 14	mpbi	$$⊢{\log }_{2}8<{\log }_{2}9$$
16	15	a1i	$$⊢\top \to {\log }_{2}8<{\log }_{2}9$$
17		eqid	$$⊢8=8$$
18		cu2	$$⊢2^3=8$$
19	17 18	eqtr4i	$$⊢8=2^3$$
20	19	a1i	$$⊢\top \to 8=2^3$$
21	20	oveq2d	$$⊢\top \to {\log }_{2}8={\log }_2{2}^3$$
22		2rp	$$⊢2\in {ℝ}^{+}$$
23	22	a1i	$$⊢\top \to 2\in {ℝ}^{+}$$
24		1red	$$⊢\top \to 1\in ℝ$$
25		1lt2	$$⊢1<2$$
26	25	a1i	$$⊢\top \to 1<2$$
27	24 26	ltned	$$⊢\top \to 1\ne 2$$
28	27	necomd	$$⊢\top \to 2\ne 1$$
29		3z	$$⊢3\in \mathbb{Z}$$
30	29	a1i	$$⊢\top \to 3\in \mathbb{Z}$$
31	23 28 30	relogbexpd	$$⊢\top \to {\log }_2{2}^3=3$$
32	21 31	eqtrd	$$⊢\top \to {\log }_{2}8=3$$
33		eqid	$$⊢9=9$$
34		sq3	$$⊢3^2=9$$
35	33 34	eqtr4i	$$⊢9=3^2$$
36	35	a1i	$$⊢\top \to 9=3^2$$
37	36	oveq2d	$$⊢\top \to {\log }_{2}9={\log }_2{3}^2$$
38	16 32 37	3brtr3d	$$⊢\top \to 3<{\log }_2{3}^2$$
39		3re	$$⊢3\in ℝ$$
40	39	a1i	$$⊢\top \to 3\in ℝ$$
41	40	recnd	$$⊢\top \to 3\in ℂ$$
42		2re	$$⊢2\in ℝ$$
43	42	a1i	$$⊢\top \to 2\in ℝ$$
44	43	recnd	$$⊢\top \to 2\in ℂ$$
45		2pos	$$⊢0<2$$
46	45	a1i	$$⊢\top \to 0<2$$
47	46	gt0ne0d	$$⊢\top \to 2\ne 0$$
48	41 44 47	divcan1d	$$⊢\top \to \left(\frac{3}{2}\right)\cdot 2=3$$
49	48	eqcomd	$$⊢\top \to 3=\left(\frac{3}{2}\right)\cdot 2$$
50		3pos	$$⊢0<3$$
51	50	a1i	$$⊢\top \to 0<3$$
52	40 51	elrpd	$$⊢\top \to 3\in {ℝ}^{+}$$
53	3	a1i	$$⊢\top \to 2\in \mathbb{Z}$$
54	23 28 52 53	relogbzexpd	$$⊢\top \to {\log }_2{3}^2=2{\log }_{2}3$$
55	43 46 40 51 28	relogbcld	$$⊢\top \to {\log }_{2}3\in ℝ$$
56	55	recnd	$$⊢\top \to {\log }_{2}3\in ℂ$$
57	44 56	mulcomd	$$⊢\top \to 2{\log }_{2}3={\log }_{2}3\cdot 2$$
58	54 57	eqtrd	$$⊢\top \to {\log }_2{3}^2={\log }_{2}3\cdot 2$$
59	38 49 58	3brtr3d	$$⊢\top \to \left(\frac{3}{2}\right)\cdot 2<{\log }_{2}3\cdot 2$$
60	40	rehalfcld	$$⊢\top \to \frac{3}{2}\in ℝ$$
61	60 55 23	ltmul1d	$$⊢\top \to \left(\frac{3}{2}<{\log }_{2}3\leftrightarrow \left(\frac{3}{2}\right)\cdot 2<{\log }_{2}3\cdot 2\right)$$
62	59 61	mpbird	$$⊢\top \to \frac{3}{2}<{\log }_{2}3$$
63		2nn0	$$⊢2\in {\mathbb{N}}_0$$
64		3nn0	$$⊢3\in {\mathbb{N}}_0$$
65		7nn0	$$⊢7\in {\mathbb{N}}_0$$
66		7lt10	$$⊢7<10$$
67		2lt3	$$⊢2<3$$
68	63 64 65 63 66 67	decltc	$$⊢27<32$$
69		7nn	$$⊢7\in \mathbb{N}$$
70	63 69	decnncl	$$⊢27\in \mathbb{N}$$
71		nnrp	$$⊢27\in \mathbb{N}\to 27\in {ℝ}^{+}$$
72	70 71	ax-mp	$$⊢27\in {ℝ}^{+}$$
73		2nn	$$⊢2\in \mathbb{N}$$
74	64 73	decnncl	$$⊢32\in \mathbb{N}$$
75		nnrp	$$⊢32\in \mathbb{N}\to 32\in {ℝ}^{+}$$
76	74 75	ax-mp	$$⊢32\in {ℝ}^{+}$$
77	5 72 76	3pm3.2i	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge 27\in {ℝ}^{+}\wedge 32\in {ℝ}^{+}\right)$$
78		logblt	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge 27\in {ℝ}^{+}\wedge 32\in {ℝ}^{+}\right)\to \left(27<32\leftrightarrow {\log }_{2}27<{\log }_{2}32\right)$$
79	77 78	ax-mp	$$⊢27<32\leftrightarrow {\log }_{2}27<{\log }_{2}32$$
80	68 79	mpbi	$$⊢{\log }_{2}27<{\log }_{2}32$$
81	80	a1i	$$⊢\top \to {\log }_{2}27<{\log }_{2}32$$
82		eqid	$$⊢32=32$$
83		2exp5	$$⊢2^5=32$$
84	82 83	eqtr4i	$$⊢32=2^5$$
85	84	a1i	$$⊢\top \to 32=2^5$$
86	85	oveq2d	$$⊢\top \to {\log }_{2}32={\log }_2{2}^5$$
87	81 86	breqtrd	$$⊢\top \to {\log }_{2}27<{\log }_2{2}^5$$
88		eqid	$$⊢27=27$$
89		3exp3	$$⊢3^3=27$$
90	88 89	eqtr4i	$$⊢27=3^3$$
91	90	a1i	$$⊢\top \to 27=3^3$$
92	91	oveq2d	$$⊢\top \to {\log }_{2}27={\log }_2{3}^3$$
93	23 28 52 30	relogbzexpd	$$⊢\top \to {\log }_2{3}^3=3{\log }_{2}3$$
94	92 93	eqtrd	$$⊢\top \to {\log }_{2}27=3{\log }_{2}3$$
95	41 56	mulcomd	$$⊢\top \to 3{\log }_{2}3={\log }_{2}3\cdot 3$$
96	94 95	eqtrd	$$⊢\top \to {\log }_{2}27={\log }_{2}3\cdot 3$$
97		5re	$$⊢5\in ℝ$$
98	97	a1i	$$⊢\top \to 5\in ℝ$$
99	98	recnd	$$⊢\top \to 5\in ℂ$$
100	51	gt0ne0d	$$⊢\top \to 3\ne 0$$
101	99 41 100	divcan1d	$$⊢\top \to \left(\frac{5}{3}\right)\cdot 3=5$$
102		5nn	$$⊢5\in \mathbb{N}$$
103	102	a1i	$$⊢\top \to 5\in \mathbb{N}$$
104	103	nnzd	$$⊢\top \to 5\in \mathbb{Z}$$
105	23 28 104	relogbexpd	$$⊢\top \to {\log }_2{2}^5=5$$
106	105	eqcomd	$$⊢\top \to 5={\log }_2{2}^5$$
107	101 106	eqtrd	$$⊢\top \to \left(\frac{5}{3}\right)\cdot 3={\log }_2{2}^5$$
108	107	eqcomd	$$⊢\top \to {\log }_2{2}^5=\left(\frac{5}{3}\right)\cdot 3$$
109	87 96 108	3brtr3d	$$⊢\top \to {\log }_{2}3\cdot 3<\left(\frac{5}{3}\right)\cdot 3$$
110	98 40 100	redivcld	$$⊢\top \to \frac{5}{3}\in ℝ$$
111	55 110 52	ltmul1d	$$⊢\top \to \left({\log }_{2}3<\frac{5}{3}\leftrightarrow {\log }_{2}3\cdot 3<\left(\frac{5}{3}\right)\cdot 3\right)$$
112	109 111	mpbird	$$⊢\top \to {\log }_{2}3<\frac{5}{3}$$
113	62 112	jca	$$⊢\top \to \left(\frac{3}{2}<{\log }_{2}3\wedge {\log }_{2}3<\frac{5}{3}\right)$$
114	1 113	ax-mp	$$⊢\left(\frac{3}{2}<{\log }_{2}3\wedge {\log }_{2}3<\frac{5}{3}\right)$$