Metamath Proof Explorer

Theorem 3lexlogpow2ineq1

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

Ref Expression
Assertion 3lexlogpow2ineq1 
|- ( ( 3 / 2 ) < ( 2 logb 3 ) /\ ( 2 logb 3 ) < ( 5 / 3 ) )

Proof

Step Hyp Ref Expression
1 tru 
 |-  T.
2 8lt9 
 |-  8 < 9
3 2z 
 |-  2 e. ZZ
4 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
5 3 4 ax-mp 
 |-  2 e. ( ZZ>= ` 2 )
6 8nn 
 |-  8 e. NN
7 nnrp 
 |-  ( 8 e. NN -> 8 e. RR+ )
8 6 7 ax-mp 
 |-  8 e. RR+
9 9nn 
 |-  9 e. NN
10 nnrp 
 |-  ( 9 e. NN -> 9 e. RR+ )
11 9 10 ax-mp 
 |-  9 e. RR+
12 5 8 11 3pm3.2i 
 |-  ( 2 e. ( ZZ>= ` 2 ) /\ 8 e. RR+ /\ 9 e. RR+ )
13 logblt 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ 8 e. RR+ /\ 9 e. RR+ ) -> ( 8 < 9 <-> ( 2 logb 8 ) < ( 2 logb 9 ) ) )
14 12 13 ax-mp 
 |-  ( 8 < 9 <-> ( 2 logb 8 ) < ( 2 logb 9 ) )
15 2 14 mpbi 
 |-  ( 2 logb 8 ) < ( 2 logb 9 )
16 15 a1i 
 |-  ( T. -> ( 2 logb 8 ) < ( 2 logb 9 ) )
17 eqid 
 |-  8 = 8
18 cu2 
 |-  ( 2 ^ 3 ) = 8
19 17 18 eqtr4i 
 |-  8 = ( 2 ^ 3 )
20 19 a1i 
 |-  ( T. -> 8 = ( 2 ^ 3 ) )
21 20 oveq2d 
 |-  ( T. -> ( 2 logb 8 ) = ( 2 logb ( 2 ^ 3 ) ) )
22 2rp 
 |-  2 e. RR+
23 22 a1i 
 |-  ( T. -> 2 e. RR+ )
24 1red 
 |-  ( T. -> 1 e. RR )
25 1lt2 
 |-  1 < 2
26 25 a1i 
 |-  ( T. -> 1 < 2 )
27 24 26 ltned 
 |-  ( T. -> 1 =/= 2 )
28 27 necomd 
 |-  ( T. -> 2 =/= 1 )
29 3z 
 |-  3 e. ZZ
30 29 a1i 
 |-  ( T. -> 3 e. ZZ )
31 23 28 30 relogbexpd 
 |-  ( T. -> ( 2 logb ( 2 ^ 3 ) ) = 3 )
32 21 31 eqtrd 
 |-  ( T. -> ( 2 logb 8 ) = 3 )
33 eqid 
 |-  9 = 9
34 sq3 
 |-  ( 3 ^ 2 ) = 9
35 33 34 eqtr4i 
 |-  9 = ( 3 ^ 2 )
36 35 a1i 
 |-  ( T. -> 9 = ( 3 ^ 2 ) )
37 36 oveq2d 
 |-  ( T. -> ( 2 logb 9 ) = ( 2 logb ( 3 ^ 2 ) ) )
38 16 32 37 3brtr3d 
 |-  ( T. -> 3 < ( 2 logb ( 3 ^ 2 ) ) )
39 3re 
 |-  3 e. RR
40 39 a1i 
 |-  ( T. -> 3 e. RR )
41 40 recnd 
 |-  ( T. -> 3 e. CC )
42 2re 
 |-  2 e. RR
43 42 a1i 
 |-  ( T. -> 2 e. RR )
44 43 recnd 
 |-  ( T. -> 2 e. CC )
45 2pos 
 |-  0 < 2
46 45 a1i 
 |-  ( T. -> 0 < 2 )
47 46 gt0ne0d 
 |-  ( T. -> 2 =/= 0 )
48 41 44 47 divcan1d 
 |-  ( T. -> ( ( 3 / 2 ) x. 2 ) = 3 )
49 48 eqcomd 
 |-  ( T. -> 3 = ( ( 3 / 2 ) x. 2 ) )
50 3pos 
 |-  0 < 3
51 50 a1i 
 |-  ( T. -> 0 < 3 )
52 40 51 elrpd 
 |-  ( T. -> 3 e. RR+ )
53 3 a1i 
 |-  ( T. -> 2 e. ZZ )
54 23 28 52 53 relogbzexpd 
 |-  ( T. -> ( 2 logb ( 3 ^ 2 ) ) = ( 2 x. ( 2 logb 3 ) ) )
55 43 46 40 51 28 relogbcld 
 |-  ( T. -> ( 2 logb 3 ) e. RR )
56 55 recnd 
 |-  ( T. -> ( 2 logb 3 ) e. CC )
57 44 56 mulcomd 
 |-  ( T. -> ( 2 x. ( 2 logb 3 ) ) = ( ( 2 logb 3 ) x. 2 ) )
58 54 57 eqtrd 
 |-  ( T. -> ( 2 logb ( 3 ^ 2 ) ) = ( ( 2 logb 3 ) x. 2 ) )
59 38 49 58 3brtr3d 
 |-  ( T. -> ( ( 3 / 2 ) x. 2 ) < ( ( 2 logb 3 ) x. 2 ) )
60 40 rehalfcld 
 |-  ( T. -> ( 3 / 2 ) e. RR )
61 60 55 23 ltmul1d 
 |-  ( T. -> ( ( 3 / 2 ) < ( 2 logb 3 ) <-> ( ( 3 / 2 ) x. 2 ) < ( ( 2 logb 3 ) x. 2 ) ) )
62 59 61 mpbird 
 |-  ( T. -> ( 3 / 2 ) < ( 2 logb 3 ) )
63 2nn0 
 |-  2 e. NN0
64 3nn0 
 |-  3 e. NN0
65 7nn0 
 |-  7 e. NN0
66 7lt10 
 |-  7 < ; 1 0
67 2lt3 
 |-  2 < 3
68 63 64 65 63 66 67 decltc 
 |-  ; 2 7 < ; 3 2
69 7nn 
 |-  7 e. NN
70 63 69 decnncl 
 |-  ; 2 7 e. NN
71 nnrp 
 |-  ( ; 2 7 e. NN -> ; 2 7 e. RR+ )
72 70 71 ax-mp 
 |-  ; 2 7 e. RR+
73 2nn 
 |-  2 e. NN
74 64 73 decnncl 
 |-  ; 3 2 e. NN
75 nnrp 
 |-  ( ; 3 2 e. NN -> ; 3 2 e. RR+ )
76 74 75 ax-mp 
 |-  ; 3 2 e. RR+
77 5 72 76 3pm3.2i 
 |-  ( 2 e. ( ZZ>= ` 2 ) /\ ; 2 7 e. RR+ /\ ; 3 2 e. RR+ )
78 logblt 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ ; 2 7 e. RR+ /\ ; 3 2 e. RR+ ) -> ( ; 2 7 < ; 3 2 <-> ( 2 logb ; 2 7 ) < ( 2 logb ; 3 2 ) ) )
79 77 78 ax-mp 
 |-  ( ; 2 7 < ; 3 2 <-> ( 2 logb ; 2 7 ) < ( 2 logb ; 3 2 ) )
80 68 79 mpbi 
 |-  ( 2 logb ; 2 7 ) < ( 2 logb ; 3 2 )
81 80 a1i 
 |-  ( T. -> ( 2 logb ; 2 7 ) < ( 2 logb ; 3 2 ) )
82 eqid 
 |-  ; 3 2 = ; 3 2
83 2exp5 
 |-  ( 2 ^ 5 ) = ; 3 2
84 82 83 eqtr4i 
 |-  ; 3 2 = ( 2 ^ 5 )
85 84 a1i 
 |-  ( T. -> ; 3 2 = ( 2 ^ 5 ) )
86 85 oveq2d 
 |-  ( T. -> ( 2 logb ; 3 2 ) = ( 2 logb ( 2 ^ 5 ) ) )
87 81 86 breqtrd 
 |-  ( T. -> ( 2 logb ; 2 7 ) < ( 2 logb ( 2 ^ 5 ) ) )
88 eqid 
 |-  ; 2 7 = ; 2 7
89 3exp3 
 |-  ( 3 ^ 3 ) = ; 2 7
90 88 89 eqtr4i 
 |-  ; 2 7 = ( 3 ^ 3 )
91 90 a1i 
 |-  ( T. -> ; 2 7 = ( 3 ^ 3 ) )
92 91 oveq2d 
 |-  ( T. -> ( 2 logb ; 2 7 ) = ( 2 logb ( 3 ^ 3 ) ) )
93 23 28 52 30 relogbzexpd 
 |-  ( T. -> ( 2 logb ( 3 ^ 3 ) ) = ( 3 x. ( 2 logb 3 ) ) )
94 92 93 eqtrd 
 |-  ( T. -> ( 2 logb ; 2 7 ) = ( 3 x. ( 2 logb 3 ) ) )
95 41 56 mulcomd 
 |-  ( T. -> ( 3 x. ( 2 logb 3 ) ) = ( ( 2 logb 3 ) x. 3 ) )
96 94 95 eqtrd 
 |-  ( T. -> ( 2 logb ; 2 7 ) = ( ( 2 logb 3 ) x. 3 ) )
97 5re 
 |-  5 e. RR
98 97 a1i 
 |-  ( T. -> 5 e. RR )
99 98 recnd 
 |-  ( T. -> 5 e. CC )
100 51 gt0ne0d 
 |-  ( T. -> 3 =/= 0 )
101 99 41 100 divcan1d 
 |-  ( T. -> ( ( 5 / 3 ) x. 3 ) = 5 )
102 5nn 
 |-  5 e. NN
103 102 a1i 
 |-  ( T. -> 5 e. NN )
104 103 nnzd 
 |-  ( T. -> 5 e. ZZ )
105 23 28 104 relogbexpd 
 |-  ( T. -> ( 2 logb ( 2 ^ 5 ) ) = 5 )
106 105 eqcomd 
 |-  ( T. -> 5 = ( 2 logb ( 2 ^ 5 ) ) )
107 101 106 eqtrd 
 |-  ( T. -> ( ( 5 / 3 ) x. 3 ) = ( 2 logb ( 2 ^ 5 ) ) )
108 107 eqcomd 
 |-  ( T. -> ( 2 logb ( 2 ^ 5 ) ) = ( ( 5 / 3 ) x. 3 ) )
109 87 96 108 3brtr3d 
 |-  ( T. -> ( ( 2 logb 3 ) x. 3 ) < ( ( 5 / 3 ) x. 3 ) )
110 98 40 100 redivcld 
 |-  ( T. -> ( 5 / 3 ) e. RR )
111 55 110 52 ltmul1d 
 |-  ( T. -> ( ( 2 logb 3 ) < ( 5 / 3 ) <-> ( ( 2 logb 3 ) x. 3 ) < ( ( 5 / 3 ) x. 3 ) ) )
112 109 111 mpbird 
 |-  ( T. -> ( 2 logb 3 ) < ( 5 / 3 ) )
113 62 112 jca 
 |-  ( T. -> ( ( 3 / 2 ) < ( 2 logb 3 ) /\ ( 2 logb 3 ) < ( 5 / 3 ) ) )
114 1 113 ax-mp 
 |-  ( ( 3 / 2 ) < ( 2 logb 3 ) /\ ( 2 logb 3 ) < ( 5 / 3 ) )