This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem log2le1

Description: log 2 is less than 1 . This is just a weaker form of log2ub when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion log2le1 ⊢ log ⁡ 2 < 1

Proof

Step Hyp Ref Expression
1 log2ub ⊢ log ⁡ 2 < 253 365
2 2nn0 ⊢ 2 ∈ ℕ 0
3 3nn0 ⊢ 3 ∈ ℕ 0
4 5nn0 ⊢ 5 ∈ ℕ 0
5 6nn0 ⊢ 6 ∈ ℕ 0
6 2lt3 ⊢ 2 < 3
7 5lt10 ⊢ 5 < 10
8 3lt10 ⊢ 3 < 10
9 2 3 4 5 3 4 6 7 8 3decltc ⊢ 253 < 365
10 2 4 deccl ⊢ 25 ∈ ℕ 0
11 10 3 deccl ⊢ 253 ∈ ℕ 0
12 11 nn0rei ⊢ 253 ∈ ℝ
13 3 5 deccl ⊢ 36 ∈ ℕ 0
14 13 4 deccl ⊢ 365 ∈ ℕ 0
15 14 nn0rei ⊢ 365 ∈ ℝ
16 6nn ⊢ 6 ∈ ℕ
17 3 16 decnncl ⊢ 36 ∈ ℕ
18 0nn0 ⊢ 0 ∈ ℕ 0
19 10pos ⊢ 0 < 10
20 17 4 18 19 declti ⊢ 0 < 365
21 12 15 15 20 ltdiv1ii ⊢ 253 < 365 ↔ 253 365 < 365 365
22 9 21 mpbi ⊢ 253 365 < 365 365
23 15 recni ⊢ 365 ∈ ℂ
24 0re ⊢ 0 ∈ ℝ
25 24 20 gtneii ⊢ 365 ≠ 0
26 23 25 dividi ⊢ 365 365 = 1
27 22 26 breqtri ⊢ 253 365 < 1
28 2rp ⊢ 2 ∈ ℝ +
29 relogcl ⊢ 2 ∈ ℝ + → log ⁡ 2 ∈ ℝ
30 28 29 ax-mp ⊢ log ⁡ 2 ∈ ℝ
31 12 15 25 redivcli ⊢ 253 365 ∈ ℝ
32 1re ⊢ 1 ∈ ℝ
33 30 31 32 lttri ⊢ log ⁡ 2 < 253 365 ∧ 253 365 < 1 → log ⁡ 2 < 1
34 1 27 33 mp2an ⊢ log ⁡ 2 < 1