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 ⊢ ⊤
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 ↔ ( 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 ⊢ ( ⊤ → ( 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 ⊢ ( ⊤ → 8 = ( 2 ↑ 3 ) )
21 20 oveq2d ⊢ ( ⊤ → ( 2 logb 8 ) = ( 2 logb ( 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 ⊢ ( ⊤ → ( 2 logb ( 2 ↑ 3 ) ) = 3 )
32 21 31 eqtrd ⊢ ( ⊤ → ( 2 logb 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 ⊢ ( ⊤ → ( 2 logb 9 ) = ( 2 logb ( 3 ↑ 2 ) ) )
38 16 32 37 3brtr3d ⊢ ( ⊤ → 3 < ( 2 logb ( 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 ⊢ ( ⊤ → ( 2 logb ( 3 ↑ 2 ) ) = ( 2 · ( 2 logb 3 ) ) )
55 43 46 40 51 28 relogbcld ⊢ ( ⊤ → ( 2 logb 3 ) ∈ ℝ )
56 55 recnd ⊢ ( ⊤ → ( 2 logb 3 ) ∈ ℂ )
57 44 56 mulcomd ⊢ ( ⊤ → ( 2 · ( 2 logb 3 ) ) = ( ( 2 logb 3 ) · 2 ) )
58 54 57 eqtrd ⊢ ( ⊤ → ( 2 logb ( 3 ↑ 2 ) ) = ( ( 2 logb 3 ) · 2 ) )
59 38 49 58 3brtr3d ⊢ ( ⊤ → ( ( 3 / 2 ) · 2 ) < ( ( 2 logb 3 ) · 2 ) )
60 40 rehalfcld ⊢ ( ⊤ → ( 3 / 2 ) ∈ ℝ )
61 60 55 23 ltmul1d ⊢ ( ⊤ → ( ( 3 / 2 ) < ( 2 logb 3 ) ↔ ( ( 3 / 2 ) · 2 ) < ( ( 2 logb 3 ) · 2 ) ) )
62 59 61 mpbird ⊢ ( ⊤ → ( 3 / 2 ) < ( 2 logb 3 ) )
63 2nn0 ⊢ 2 ∈ ℕ0
64 3nn0 ⊢ 3 ∈ ℕ0
65 7nn0 ⊢ 7 ∈ ℕ0
66 7lt10 ⊢ 7 < 1 0
67 2lt3 ⊢ 2 < 3
68 63 64 65 63 66 67 decltc ⊢ 2 7 < 3 2
69 7nn ⊢ 7 ∈ ℕ
70 63 69 decnncl ⊢ 2 7 ∈ ℕ
71 nnrp ⊢ ( 2 7 ∈ ℕ → 2 7 ∈ ℝ+ )
72 70 71 ax-mp ⊢ 2 7 ∈ ℝ+
73 2nn ⊢ 2 ∈ ℕ
74 64 73 decnncl ⊢ 3 2 ∈ ℕ
75 nnrp ⊢ ( 3 2 ∈ ℕ → 3 2 ∈ ℝ+ )
76 74 75 ax-mp ⊢ 3 2 ∈ ℝ+
77 5 72 76 3pm3.2i ⊢ ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 2 7 ∈ ℝ+ ∧ 3 2 ∈ ℝ+ )
78 logblt ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 2 7 ∈ ℝ+ ∧ 3 2 ∈ ℝ+ ) → ( 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 ⊢ ( ⊤ → ( 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 ⊢ ( ⊤ → 3 2 = ( 2 ↑ 5 ) )
86 85 oveq2d ⊢ ( ⊤ → ( 2 logb 3 2 ) = ( 2 logb ( 2 ↑ 5 ) ) )
87 81 86 breqtrd ⊢ ( ⊤ → ( 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 ⊢ ( ⊤ → 2 7 = ( 3 ↑ 3 ) )
92 91 oveq2d ⊢ ( ⊤ → ( 2 logb 2 7 ) = ( 2 logb ( 3 ↑ 3 ) ) )
93 23 28 52 30 relogbzexpd ⊢ ( ⊤ → ( 2 logb ( 3 ↑ 3 ) ) = ( 3 · ( 2 logb 3 ) ) )
94 92 93 eqtrd ⊢ ( ⊤ → ( 2 logb 2 7 ) = ( 3 · ( 2 logb 3 ) ) )
95 41 56 mulcomd ⊢ ( ⊤ → ( 3 · ( 2 logb 3 ) ) = ( ( 2 logb 3 ) · 3 ) )
96 94 95 eqtrd ⊢ ( ⊤ → ( 2 logb 2 7 ) = ( ( 2 logb 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 ⊢ ( ⊤ → ( 2 logb ( 2 ↑ 5 ) ) = 5 )
106 105 eqcomd ⊢ ( ⊤ → 5 = ( 2 logb ( 2 ↑ 5 ) ) )
107 101 106 eqtrd ⊢ ( ⊤ → ( ( 5 / 3 ) · 3 ) = ( 2 logb ( 2 ↑ 5 ) ) )
108 107 eqcomd ⊢ ( ⊤ → ( 2 logb ( 2 ↑ 5 ) ) = ( ( 5 / 3 ) · 3 ) )
109 87 96 108 3brtr3d ⊢ ( ⊤ → ( ( 2 logb 3 ) · 3 ) < ( ( 5 / 3 ) · 3 ) )
110 98 40 100 redivcld ⊢ ( ⊤ → ( 5 / 3 ) ∈ ℝ )
111 55 110 52 ltmul1d ⊢ ( ⊤ → ( ( 2 logb 3 ) < ( 5 / 3 ) ↔ ( ( 2 logb 3 ) · 3 ) < ( ( 5 / 3 ) · 3 ) ) )
112 109 111 mpbird ⊢ ( ⊤ → ( 2 logb 3 ) < ( 5 / 3 ) )
113 62 112 jca ⊢ ( ⊤ → ( ( 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 ) )