Theorem 3lexlogpow2ineq2

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

	Ref	Expression
Assertion	3lexlogpow2ineq2	|- ( 2 < ( ( 2 logb 3 ) ^ 2 ) /\ ( ( 2 logb 3 ) ^ 2 ) < 3 )

Proof

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