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<\frac{253}{365}$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3		3nn0	$$⊢3\in {\mathbb{N}}_0$$
4		5nn0	$$⊢5\in {\mathbb{N}}_0$$
5		6nn0	$$⊢6\in {\mathbb{N}}_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\in {\mathbb{N}}_0$$
11	10 3	deccl	$$⊢253\in {\mathbb{N}}_0$$
12	11	nn0rei	$$⊢253\in ℝ$$
13	3 5	deccl	$$⊢36\in {\mathbb{N}}_0$$
14	13 4	deccl	$$⊢365\in {\mathbb{N}}_0$$
15	14	nn0rei	$$⊢365\in ℝ$$
16		6nn	$$⊢6\in \mathbb{N}$$
17	3 16	decnncl	$$⊢36\in \mathbb{N}$$
18		0nn0	$$⊢0\in {\mathbb{N}}_0$$
19		10pos	$$⊢0<10$$
20	17 4 18 19	declti	$$⊢0<365$$
21	12 15 15 20	ltdiv1ii	$$⊢253<365\leftrightarrow \frac{253}{365}<\frac{365}{365}$$
22	9 21	mpbi	$$⊢\frac{253}{365}<\frac{365}{365}$$
23	15	recni	$$⊢365\in ℂ$$
24		0re	$$⊢0\in ℝ$$
25	24 20	gtneii	$$⊢365\ne 0$$
26	23 25	dividi	$$⊢\frac{365}{365}=1$$
27	22 26	breqtri	$$⊢\frac{253}{365}<1$$
28		2rp	$$⊢2\in {ℝ}^{+}$$
29		relogcl	$$⊢2\in {ℝ}^{+}\to \log 2\in ℝ$$
30	28 29	ax-mp	$$⊢\log 2\in ℝ$$
31	12 15 25	redivcli	$$⊢\frac{253}{365}\in ℝ$$
32		1re	$$⊢1\in ℝ$$
33	30 31 32	lttri	$$⊢\left(\log 2<\frac{253}{365}\wedge \frac{253}{365}<1\right)\to \log 2<1$$
34	1 27 33	mp2an	$$⊢\log 2<1$$