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 ∈ ℕ0
3		3nn0	⊢ 3 ∈ ℕ0
4		5nn0	⊢ 5 ∈ ℕ0
5		6nn0	⊢ 6 ∈ ℕ0
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 ∈ ℕ0
11	10 3	deccl	⊢ ; ; 2 5 3 ∈ ℕ0
12	11	nn0rei	⊢ ; ; 2 5 3 ∈ ℝ
13	3 5	deccl	⊢ ; 3 6 ∈ ℕ0
14	13 4	deccl	⊢ ; ; 3 6 5 ∈ ℕ0
15	14	nn0rei	⊢ ; ; 3 6 5 ∈ ℝ
16		6nn	⊢ 6 ∈ ℕ
17	3 16	decnncl	⊢ ; 3 6 ∈ ℕ
18		0nn0	⊢ 0 ∈ ℕ0
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 ∈ ℂ
24		0re	⊢ 0 ∈ ℝ
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 ∈ ℝ+
29		relogcl	⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
30	28 29	ax-mp	⊢ ( log ‘ 2 ) ∈ ℝ
31	12 15 25	redivcli	⊢ ( ; ; 2 5 3 / ; ; 3 6 5 ) ∈ ℝ
32		1re	⊢ 1 ∈ ℝ
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