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