Step |
Hyp |
Ref |
Expression |
1 |
|
log2le1 |
⊢ ( log ‘ 2 ) < 1 |
2 |
|
2rp |
⊢ 2 ∈ ℝ+ |
3 |
|
relogcl |
⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ ) |
4 |
2 3
|
ax-mp |
⊢ ( log ‘ 2 ) ∈ ℝ |
5 |
|
1re |
⊢ 1 ∈ ℝ |
6 |
4 5
|
posdifi |
⊢ ( ( log ‘ 2 ) < 1 ↔ 0 < ( 1 − ( log ‘ 2 ) ) ) |
7 |
1 6
|
mpbi |
⊢ 0 < ( 1 − ( log ‘ 2 ) ) |
8 |
|
emcl |
⊢ γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) |
9 |
5 4
|
resubcli |
⊢ ( 1 − ( log ‘ 2 ) ) ∈ ℝ |
10 |
9 5
|
elicc2i |
⊢ ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) ↔ ( γ ∈ ℝ ∧ ( 1 − ( log ‘ 2 ) ) ≤ γ ∧ γ ≤ 1 ) ) |
11 |
10
|
simp2bi |
⊢ ( γ ∈ ( ( 1 − ( log ‘ 2 ) ) [,] 1 ) → ( 1 − ( log ‘ 2 ) ) ≤ γ ) |
12 |
8 11
|
ax-mp |
⊢ ( 1 − ( log ‘ 2 ) ) ≤ γ |
13 |
|
0re |
⊢ 0 ∈ ℝ |
14 |
|
emre |
⊢ γ ∈ ℝ |
15 |
13 9 14
|
ltletri |
⊢ ( ( 0 < ( 1 − ( log ‘ 2 ) ) ∧ ( 1 − ( log ‘ 2 ) ) ≤ γ ) → 0 < γ ) |
16 |
7 12 15
|
mp2an |
⊢ 0 < γ |