3lexlogpow2ineq2

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

		Ref	Expression
	Assertion	3lexlogpow2ineq2	$⊢ (2 < {\log_{2} 3}^{2} \land {\log_{2} 3}^{2} < 3)$

Proof

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

Metamath Proof Explorer

Theorem 3lexlogpow2ineq2

Proof