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