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