Metamath Proof Explorer

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