Theorem 3lexlogpow2ineq2

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

	Ref	Expression
Assertion	3lexlogpow2ineq2	$$⊢\left(2<{{\log }_{2}3}^2\wedge {{\log }_{2}3}^2<3\right)$$

Proof

Step	Hyp	Ref	Expression
1		tru	$$⊢\top$$
2		2re	$$⊢2\in ℝ$$
3	2	a1i	$$⊢\top \to 2\in ℝ$$
4		3re	$$⊢3\in ℝ$$
5	4	a1i	$$⊢\top \to 3\in ℝ$$
6	5	rehalfcld	$$⊢\top \to \frac{3}{2}\in ℝ$$
7	6	resqcld	$$⊢\top \to {\left(\frac{3}{2}\right)}^2\in ℝ$$
8		2pos	$$⊢0<2$$
9	8	a1i	$$⊢\top \to 0<2$$
10		3pos	$$⊢0<3$$
11	10	a1i	$$⊢\top \to 0<3$$
12		1red	$$⊢\top \to 1\in ℝ$$
13		1lt2	$$⊢1<2$$
14	13	a1i	$$⊢\top \to 1<2$$
15	12 14	ltned	$$⊢\top \to 1\ne 2$$
16	15	necomd	$$⊢\top \to 2\ne 1$$
17	3 9 5 11 16	relogbcld	$$⊢\top \to {\log }_{2}3\in ℝ$$
18	17	resqcld	$$⊢\top \to {{\log }_{2}3}^2\in ℝ$$
19		2cnd	$$⊢\top \to 2\in ℂ$$
20		4cn	$$⊢4\in ℂ$$
21	20	a1i	$$⊢\top \to 4\in ℂ$$
22		0red	$$⊢\top \to 0\in ℝ$$
23		4pos	$$⊢0<4$$
24	23	a1i	$$⊢\top \to 0<4$$
25	22 24	ltned	$$⊢\top \to 0\ne 4$$
26	25	necomd	$$⊢\top \to 4\ne 0$$
27	19 21 26	divcan4d	$$⊢\top \to \frac{2\cdot 4}{4}=2$$
28	27	eqcomd	$$⊢\top \to 2=\frac{2\cdot 4}{4}$$
29		4re	$$⊢4\in ℝ$$
30	29	a1i	$$⊢\top \to 4\in ℝ$$
31	3 30	remulcld	$$⊢\top \to 2\cdot 4\in ℝ$$
32		9re	$$⊢9\in ℝ$$
33	32	a1i	$$⊢\top \to 9\in ℝ$$
34	30 24	elrpd	$$⊢\top \to 4\in {ℝ}^{+}$$
35		2cn	$$⊢2\in ℂ$$
36		4t2e8	$$⊢4\cdot 2=8$$
37	20 35 36	mulcomli	$$⊢2\cdot 4=8$$
38	37	a1i	$$⊢\top \to 2\cdot 4=8$$
39		8lt9	$$⊢8<9$$
40	39	a1i	$$⊢\top \to 8<9$$
41	38 40	eqbrtrd	$$⊢\top \to 2\cdot 4<9$$
42	31 33 34 41	ltdiv1dd	$$⊢\top \to \frac{2\cdot 4}{4}<\frac{9}{4}$$
43	28 42	eqbrtrd	$$⊢\top \to 2<\frac{9}{4}$$
44		eqid	$$⊢9=9$$
45		3t3e9	$$⊢3\cdot 3=9$$
46	44 45	eqtr4i	$$⊢9=3\cdot 3$$
47	46	a1i	$$⊢\top \to 9=3\cdot 3$$
48		eqid	$$⊢4=4$$
49		2t2e4	$$⊢2\cdot 2=4$$
50	48 49	eqtr4i	$$⊢4=2\cdot 2$$
51	50	a1i	$$⊢\top \to 4=2\cdot 2$$
52	47 51	oveq12d	$$⊢\top \to \frac{9}{4}=\frac{3\cdot 3}{2\cdot 2}$$
53	5	recnd	$$⊢\top \to 3\in ℂ$$
54	3	recnd	$$⊢\top \to 2\in ℂ$$
55	9	gt0ne0d	$$⊢\top \to 2\ne 0$$
56	53 54 53 54 55 55	divmuldivd	$$⊢\top \to \left(\frac{3}{2}\right)\left(\frac{3}{2}\right)=\frac{3\cdot 3}{2\cdot 2}$$
57	56	eqcomd	$$⊢\top \to \frac{3\cdot 3}{2\cdot 2}=\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)$$
58	52 57	eqtrd	$$⊢\top \to \frac{9}{4}=\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)$$
59	6	recnd	$$⊢\top \to \frac{3}{2}\in ℂ$$
60		sqval	$$⊢\frac{3}{2}\in ℂ\to {\left(\frac{3}{2}\right)}^2=\left(\frac{3}{2}\right)\left(\frac{3}{2}\right)$$
61	60	eqcomd	$$⊢\frac{3}{2}\in ℂ\to \left(\frac{3}{2}\right)\left(\frac{3}{2}\right)={\left(\frac{3}{2}\right)}^2$$
62	59 61	syl	$$⊢\top \to \left(\frac{3}{2}\right)\left(\frac{3}{2}\right)={\left(\frac{3}{2}\right)}^2$$
63	58 62	eqtrd	$$⊢\top \to \frac{9}{4}={\left(\frac{3}{2}\right)}^2$$
64	43 63	breqtrd	$$⊢\top \to 2<{\left(\frac{3}{2}\right)}^2$$
65		3lexlogpow2ineq1	$$⊢\left(\frac{3}{2}<{\log }_{2}3\wedge {\log }_{2}3<\frac{5}{3}\right)$$
66	65	a1i	$$⊢\top \to \left(\frac{3}{2}<{\log }_{2}3\wedge {\log }_{2}3<\frac{5}{3}\right)$$
67	66	simpld	$$⊢\top \to \frac{3}{2}<{\log }_{2}3$$
68		2nn	$$⊢2\in \mathbb{N}$$
69	68	a1i	$$⊢\top \to 2\in \mathbb{N}$$
70		3rp	$$⊢3\in {ℝ}^{+}$$
71	70	a1i	$$⊢\top \to 3\in {ℝ}^{+}$$
72	71	rphalfcld	$$⊢\top \to \frac{3}{2}\in {ℝ}^{+}$$
73	5 3 11 9	divgt0d	$$⊢\top \to 0<\frac{3}{2}$$
74	22 6 17 73 67	lttrd	$$⊢\top \to 0<{\log }_{2}3$$
75	17 74	elrpd	$$⊢\top \to {\log }_{2}3\in {ℝ}^{+}$$
76		rpexpmord	$$⊢\left(2\in \mathbb{N}\wedge \frac{3}{2}\in {ℝ}^{+}\wedge {\log }_{2}3\in {ℝ}^{+}\right)\to \left(\frac{3}{2}<{\log }_{2}3\leftrightarrow {\left(\frac{3}{2}\right)}^2<{{\log }_{2}3}^2\right)$$
77	69 72 75 76	syl3anc	$$⊢\top \to \left(\frac{3}{2}<{\log }_{2}3\leftrightarrow {\left(\frac{3}{2}\right)}^2<{{\log }_{2}3}^2\right)$$
78	67 77	mpbid	$$⊢\top \to {\left(\frac{3}{2}\right)}^2<{{\log }_{2}3}^2$$
79	3 7 18 64 78	lttrd	$$⊢\top \to 2<{{\log }_{2}3}^2$$
80		5re	$$⊢5\in ℝ$$
81	80	a1i	$$⊢\top \to 5\in ℝ$$
82	22 11	gtned	$$⊢\top \to 3\ne 0$$
83	81 5 82	redivcld	$$⊢\top \to \frac{5}{3}\in ℝ$$
84	69	nnnn0d	$$⊢\top \to 2\in {\mathbb{N}}_0$$
85	83 84	reexpcld	$$⊢\top \to {\left(\frac{5}{3}\right)}^2\in ℝ$$
86	66	simprd	$$⊢\top \to {\log }_{2}3<\frac{5}{3}$$
87		5nn	$$⊢5\in \mathbb{N}$$
88	87	a1i	$$⊢\top \to 5\in \mathbb{N}$$
89	88	nnrpd	$$⊢\top \to 5\in {ℝ}^{+}$$
90	89 71	rpdivcld	$$⊢\top \to \frac{5}{3}\in {ℝ}^{+}$$
91		rpexpmord	$$⊢\left(2\in \mathbb{N}\wedge {\log }_{2}3\in {ℝ}^{+}\wedge \frac{5}{3}\in {ℝ}^{+}\right)\to \left({\log }_{2}3<\frac{5}{3}\leftrightarrow {{\log }_{2}3}^2<{\left(\frac{5}{3}\right)}^2\right)$$
92	69 75 90 91	syl3anc	$$⊢\top \to \left({\log }_{2}3<\frac{5}{3}\leftrightarrow {{\log }_{2}3}^2<{\left(\frac{5}{3}\right)}^2\right)$$
93	86 92	mpbid	$$⊢\top \to {{\log }_{2}3}^2<{\left(\frac{5}{3}\right)}^2$$
94	83	recnd	$$⊢\top \to \frac{5}{3}\in ℂ$$
95	94	sqvald	$$⊢\top \to {\left(\frac{5}{3}\right)}^2=\left(\frac{5}{3}\right)\left(\frac{5}{3}\right)$$
96	81	recnd	$$⊢\top \to 5\in ℂ$$
97	96 53 96 53 82 82	divmuldivd	$$⊢\top \to \left(\frac{5}{3}\right)\left(\frac{5}{3}\right)=\frac{5\cdot 5}{3\cdot 3}$$
98		5t5e25	$$⊢5\cdot 5=25$$
99	98	a1i	$$⊢\top \to 5\cdot 5=25$$
100	45	a1i	$$⊢\top \to 3\cdot 3=9$$
101	99 100	oveq12d	$$⊢\top \to \frac{5\cdot 5}{3\cdot 3}=\frac{25}{9}$$
102		2nn0	$$⊢2\in {\mathbb{N}}_0$$
103		5nn0	$$⊢5\in {\mathbb{N}}_0$$
104		7nn	$$⊢7\in \mathbb{N}$$
105		5lt7	$$⊢5<7$$
106	102 103 104 105	declt	$$⊢25<27$$
107		9cn	$$⊢9\in ℂ$$
108		3cn	$$⊢3\in ℂ$$
109		9t3e27	$$⊢9\cdot 3=27$$
110	107 108 109	mulcomli	$$⊢3\cdot 9=27$$
111	106 110	breqtrri	$$⊢25<3\cdot 9$$
112	111	a1i	$$⊢\top \to 25<3\cdot 9$$
113	102 87	decnncl	$$⊢25\in \mathbb{N}$$
114	113	a1i	$$⊢\top \to 25\in \mathbb{N}$$
115	114	nnred	$$⊢\top \to 25\in ℝ$$
116		9nn	$$⊢9\in \mathbb{N}$$
117	116	a1i	$$⊢\top \to 9\in \mathbb{N}$$
118	117	nnrpd	$$⊢\top \to 9\in {ℝ}^{+}$$
119	115 5 118	ltdivmul2d	$$⊢\top \to \left(\frac{25}{9}<3\leftrightarrow 25<3\cdot 9\right)$$
120	112 119	mpbird	$$⊢\top \to \frac{25}{9}<3$$
121	101 120	eqbrtrd	$$⊢\top \to \frac{5\cdot 5}{3\cdot 3}<3$$
122	97 121	eqbrtrd	$$⊢\top \to \left(\frac{5}{3}\right)\left(\frac{5}{3}\right)<3$$
123	95 122	eqbrtrd	$$⊢\top \to {\left(\frac{5}{3}\right)}^2<3$$
124	18 85 5 93 123	lttrd	$$⊢\top \to {{\log }_{2}3}^2<3$$
125	79 124	jca	$$⊢\top \to \left(2<{{\log }_{2}3}^2\wedge {{\log }_{2}3}^2<3\right)$$
126	1 125	ax-mp	$$⊢\left(2<{{\log }_{2}3}^2\wedge {{\log }_{2}3}^2<3\right)$$