Metamath Proof Explorer


Theorem 3lexlogpow5ineq2

Description: Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024)

Ref Expression
Hypotheses 3lexlogpow5ineq2.1 ( 𝜑𝑋 ∈ ℝ )
3lexlogpow5ineq2.2 ( 𝜑 → 3 ≤ 𝑋 )
Assertion 3lexlogpow5ineq2 ( 𝜑 → ( ( 1 1 / 7 ) ↑ 5 ) ≤ ( ( 2 logb 𝑋 ) ↑ 5 ) )

Proof

Step Hyp Ref Expression
1 3lexlogpow5ineq2.1 ( 𝜑𝑋 ∈ ℝ )
2 3lexlogpow5ineq2.2 ( 𝜑 → 3 ≤ 𝑋 )
3 1nn0 1 ∈ ℕ0
4 1nn 1 ∈ ℕ
5 3 4 decnncl 1 1 ∈ ℕ
6 5 a1i ( 𝜑 1 1 ∈ ℕ )
7 6 nnred ( 𝜑 1 1 ∈ ℝ )
8 7re 7 ∈ ℝ
9 8 a1i ( 𝜑 → 7 ∈ ℝ )
10 0red ( 𝜑 → 0 ∈ ℝ )
11 7pos 0 < 7
12 11 a1i ( 𝜑 → 0 < 7 )
13 10 12 ltned ( 𝜑 → 0 ≠ 7 )
14 13 necomd ( 𝜑 → 7 ≠ 0 )
15 7 9 14 redivcld ( 𝜑 → ( 1 1 / 7 ) ∈ ℝ )
16 2re 2 ∈ ℝ
17 16 a1i ( 𝜑 → 2 ∈ ℝ )
18 2pos 0 < 2
19 18 a1i ( 𝜑 → 0 < 2 )
20 3re 3 ∈ ℝ
21 20 a1i ( 𝜑 → 3 ∈ ℝ )
22 3pos 0 < 3
23 22 a1i ( 𝜑 → 0 < 3 )
24 10 21 1 23 2 ltletrd ( 𝜑 → 0 < 𝑋 )
25 1red ( 𝜑 → 1 ∈ ℝ )
26 1lt2 1 < 2
27 26 a1i ( 𝜑 → 1 < 2 )
28 25 27 ltned ( 𝜑 → 1 ≠ 2 )
29 28 necomd ( 𝜑 → 2 ≠ 1 )
30 17 19 1 24 29 relogbcld ( 𝜑 → ( 2 logb 𝑋 ) ∈ ℝ )
31 5nn0 5 ∈ ℕ0
32 31 a1i ( 𝜑 → 5 ∈ ℕ0 )
33 7nn 7 ∈ ℕ
34 33 a1i ( 𝜑 → 7 ∈ ℕ )
35 34 nnrpd ( 𝜑 → 7 ∈ ℝ+ )
36 0nn0 0 ∈ ℕ0
37 tru
38 0red ( ⊤ → 0 ∈ ℝ )
39 9re 9 ∈ ℝ
40 39 a1i ( ⊤ → 9 ∈ ℝ )
41 9pos 0 < 9
42 41 a1i ( ⊤ → 0 < 9 )
43 38 40 42 ltled ( ⊤ → 0 ≤ 9 )
44 37 43 ax-mp 0 ≤ 9
45 4 3 36 44 declei 0 ≤ 1 1
46 45 a1i ( 𝜑 → 0 ≤ 1 1 )
47 7 35 46 divge0d ( 𝜑 → 0 ≤ ( 1 1 / 7 ) )
48 17 19 21 23 29 relogbcld ( 𝜑 → ( 2 logb 3 ) ∈ ℝ )
49 2exp11 ( 2 ↑ 1 1 ) = 2 0 4 8
50 49 eqcomi 2 0 4 8 = ( 2 ↑ 1 1 )
51 50 a1i ( 𝜑 2 0 4 8 = ( 2 ↑ 1 1 ) )
52 51 oveq2d ( 𝜑 → ( 2 logb 2 0 4 8 ) = ( 2 logb ( 2 ↑ 1 1 ) ) )
53 17 19 elrpd ( 𝜑 → 2 ∈ ℝ+ )
54 6 nnzd ( 𝜑 1 1 ∈ ℤ )
55 53 29 54 relogbexpd ( 𝜑 → ( 2 logb ( 2 ↑ 1 1 ) ) = 1 1 )
56 52 55 eqtrd ( 𝜑 → ( 2 logb 2 0 4 8 ) = 1 1 )
57 56 eqcomd ( 𝜑 1 1 = ( 2 logb 2 0 4 8 ) )
58 2z 2 ∈ ℤ
59 58 a1i ( 𝜑 → 2 ∈ ℤ )
60 17 leidd ( 𝜑 → 2 ≤ 2 )
61 2nn0 2 ∈ ℕ0
62 61 36 deccl 2 0 ∈ ℕ0
63 4nn0 4 ∈ ℕ0
64 62 63 deccl 2 0 4 ∈ ℕ0
65 8nn 8 ∈ ℕ
66 64 65 decnncl 2 0 4 8 ∈ ℕ
67 66 a1i ( 𝜑 2 0 4 8 ∈ ℕ )
68 67 nnred ( 𝜑 2 0 4 8 ∈ ℝ )
69 4nn 4 ∈ ℕ
70 62 69 decnncl 2 0 4 ∈ ℕ
71 8nn0 8 ∈ ℕ0
72 70 71 36 44 decltdi 0 < 2 0 4 8
73 72 a1i ( 𝜑 → 0 < 2 0 4 8 )
74 61 3 deccl 2 1 ∈ ℕ0
75 74 71 deccl 2 1 8 ∈ ℕ0
76 75 33 decnncl 2 1 8 7 ∈ ℕ
77 76 a1i ( 𝜑 2 1 8 7 ∈ ℕ )
78 77 nnred ( 𝜑 2 1 8 7 ∈ ℝ )
79 74 65 decnncl 2 1 8 ∈ ℕ
80 7nn0 7 ∈ ℕ0
81 79 80 36 44 decltdi 0 < 2 1 8 7
82 81 a1i ( 𝜑 → 0 < 2 1 8 7 )
83 8re 8 ∈ ℝ
84 83 3 nn0addge1i 8 ≤ ( 8 + 1 )
85 8p1e9 ( 8 + 1 ) = 9
86 84 85 breqtri 8 ≤ 9
87 4lt10 4 < 1 0
88 0lt1 0 < 1
89 61 36 4 88 declt 2 0 < 2 1
90 62 74 63 71 87 89 decltc 2 0 4 < 2 1 8
91 64 75 71 80 86 90 decleh 2 0 4 8 ≤ 2 1 8 7
92 91 a1i ( 𝜑 2 0 4 8 ≤ 2 1 8 7 )
93 59 60 68 73 78 82 92 logblebd ( 𝜑 → ( 2 logb 2 0 4 8 ) ≤ ( 2 logb 2 1 8 7 ) )
94 57 93 eqbrtrd ( 𝜑 1 1 ≤ ( 2 logb 2 1 8 7 ) )
95 7 recnd ( 𝜑 1 1 ∈ ℂ )
96 9 recnd ( 𝜑 → 7 ∈ ℂ )
97 95 96 14 divcan1d ( 𝜑 → ( ( 1 1 / 7 ) · 7 ) = 1 1 )
98 97 eqcomd ( 𝜑 1 1 = ( ( 1 1 / 7 ) · 7 ) )
99 3exp7 ( 3 ↑ 7 ) = 2 1 8 7
100 99 eqcomi 2 1 8 7 = ( 3 ↑ 7 )
101 100 a1i ( 𝜑 2 1 8 7 = ( 3 ↑ 7 ) )
102 101 oveq2d ( 𝜑 → ( 2 logb 2 1 8 7 ) = ( 2 logb ( 3 ↑ 7 ) ) )
103 21 23 elrpd ( 𝜑 → 3 ∈ ℝ+ )
104 34 nnzd ( 𝜑 → 7 ∈ ℤ )
105 53 29 103 104 relogbzexpd ( 𝜑 → ( 2 logb ( 3 ↑ 7 ) ) = ( 7 · ( 2 logb 3 ) ) )
106 102 105 eqtrd ( 𝜑 → ( 2 logb 2 1 8 7 ) = ( 7 · ( 2 logb 3 ) ) )
107 48 recnd ( 𝜑 → ( 2 logb 3 ) ∈ ℂ )
108 96 107 mulcomd ( 𝜑 → ( 7 · ( 2 logb 3 ) ) = ( ( 2 logb 3 ) · 7 ) )
109 106 108 eqtrd ( 𝜑 → ( 2 logb 2 1 8 7 ) = ( ( 2 logb 3 ) · 7 ) )
110 94 98 109 3brtr3d ( 𝜑 → ( ( 1 1 / 7 ) · 7 ) ≤ ( ( 2 logb 3 ) · 7 ) )
111 15 48 35 lemul1d ( 𝜑 → ( ( 1 1 / 7 ) ≤ ( 2 logb 3 ) ↔ ( ( 1 1 / 7 ) · 7 ) ≤ ( ( 2 logb 3 ) · 7 ) ) )
112 110 111 mpbird ( 𝜑 → ( 1 1 / 7 ) ≤ ( 2 logb 3 ) )
113 59 60 21 23 1 24 2 logblebd ( 𝜑 → ( 2 logb 3 ) ≤ ( 2 logb 𝑋 ) )
114 15 48 30 112 113 letrd ( 𝜑 → ( 1 1 / 7 ) ≤ ( 2 logb 𝑋 ) )
115 15 30 32 47 114 leexp1ad ( 𝜑 → ( ( 1 1 / 7 ) ↑ 5 ) ≤ ( ( 2 logb 𝑋 ) ↑ 5 ) )