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 ) ) |
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 ) ) |