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 < log 2 3 log 2 3 < 5 3

Proof

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