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