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 ) < ( ; ; 2 5 3 / ; ; 3 6 5 )
2 2nn0 
 |-  2 e. NN0
3 3nn0 
 |-  3 e. NN0
4 5nn0 
 |-  5 e. NN0
5 6nn0 
 |-  6 e. NN0
6 2lt3 
 |-  2 < 3
7 5lt10 
 |-  5 < ; 1 0
8 3lt10 
 |-  3 < ; 1 0
9 2 3 4 5 3 4 6 7 8 3decltc 
 |-  ; ; 2 5 3 < ; ; 3 6 5
10 2 4 deccl 
 |-  ; 2 5 e. NN0
11 10 3 deccl 
 |-  ; ; 2 5 3 e. NN0
12 11 nn0rei 
 |-  ; ; 2 5 3 e. RR
13 3 5 deccl 
 |-  ; 3 6 e. NN0
14 13 4 deccl 
 |-  ; ; 3 6 5 e. NN0
15 14 nn0rei 
 |-  ; ; 3 6 5 e. RR
16 6nn 
 |-  6 e. NN
17 3 16 decnncl 
 |-  ; 3 6 e. NN
18 0nn0 
 |-  0 e. NN0
19 10pos 
 |-  0 < ; 1 0
20 17 4 18 19 declti 
 |-  0 < ; ; 3 6 5
21 12 15 15 20 ltdiv1ii 
 |-  ( ; ; 2 5 3 < ; ; 3 6 5 <-> ( ; ; 2 5 3 / ; ; 3 6 5 ) < ( ; ; 3 6 5 / ; ; 3 6 5 ) )
22 9 21 mpbi 
 |-  ( ; ; 2 5 3 / ; ; 3 6 5 ) < ( ; ; 3 6 5 / ; ; 3 6 5 )
23 15 recni 
 |-  ; ; 3 6 5 e. CC
24 0re 
 |-  0 e. RR
25 24 20 gtneii 
 |-  ; ; 3 6 5 =/= 0
26 23 25 dividi 
 |-  ( ; ; 3 6 5 / ; ; 3 6 5 ) = 1
27 22 26 breqtri 
 |-  ( ; ; 2 5 3 / ; ; 3 6 5 ) < 1
28 2rp 
 |-  2 e. RR+
29 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
30 28 29 ax-mp 
 |-  ( log ` 2 ) e. RR
31 12 15 25 redivcli 
 |-  ( ; ; 2 5 3 / ; ; 3 6 5 ) e. RR
32 1re 
 |-  1 e. RR
33 30 31 32 lttri 
 |-  ( ( ( log ` 2 ) < ( ; ; 2 5 3 / ; ; 3 6 5 ) /\ ( ; ; 2 5 3 / ; ; 3 6 5 ) < 1 ) -> ( log ` 2 ) < 1 )
34 1 27 33 mp2an 
 |-  ( log ` 2 ) < 1