logno1

Description: The logarithm function is not eventually bounded. (Contributed by Mario Carneiro, 30-Apr-2016) (Proof shortened by Mario Carneiro, 30-May-2016)

		Ref	Expression
	Assertion	logno1	$⊢ \neg (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		elioore	$⊢ y \in (1, +∞) \to y \in ℝ$
2	1	adantl	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to y \in ℝ$
3		1rp	$⊢ 1 \in ℝ^{+}$
4	3	a1i	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to 1 \in ℝ^{+}$
5		1red	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to 1 \in ℝ$
6		eliooord	$⊢ y \in (1, +∞) \to (1 < y \land y < +∞)$
7	6	adantl	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to (1 < y \land y < +∞)$
8	7	simpld	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to 1 < y$
9	5 2 8	ltled	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to 1 \leq y$
10	2 4 9	rpgecld	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to y \in ℝ^{+}$
11	10	ex	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to (y \in (1, +∞) \to y \in ℝ^{+})$
12	11	ssrdv	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to (1, +∞) \subseteq ℝ^{+}$
13		fveq2	$⊢ x = y \to \log x = \log y$
14	13	cbvmptv	$⊢ (x \in ℝ^{+} ⟼ \log x) = (y \in ℝ^{+} ⟼ \log y)$
15	14	eleq1i	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \leftrightarrow (y \in ℝ^{+} ⟼ \log y) \in 𝑂 (1)$
16	15	biimpi	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to (y \in ℝ^{+} ⟼ \log y) \in 𝑂 (1)$
17	12 16	o1res2	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to (y \in (1, +∞) ⟼ \log y) \in 𝑂 (1)$
18		1red	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to 1 \in ℝ$
19	18	rexrd	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to 1 \in ℝ^{*}$
20	18	renepnfd	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to 1 \neq +∞$
21		ioopnfsup	$⊢ (1 \in ℝ^{} \land 1 \neq +∞) \to sup ((1, +∞) ℝ^{} <) = +∞$
22	19 20 21	syl2anc	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to sup ((1, +∞) ℝ^{*} <) = +∞$
23		divlogrlim	$⊢ (y \in (1, +∞) ⟼ \frac{1}{\log y}) \underset{ℝ}{⇝} 0$
24	23	a1i	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to (y \in (1, +∞) ⟼ \frac{1}{\log y}) \underset{ℝ}{⇝} 0$
25	2 8	rplogcld	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to \log y \in ℝ^{+}$
26	25	rpcnd	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to \log y \in ℂ$
27	25	rpne0d	$⊢ ((x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \land y \in (1, +∞)) \to \log y \neq 0$
28	22 24 26 27	rlimno1	$⊢ (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1) \to \neg (y \in (1, +∞) ⟼ \log y) \in 𝑂 (1)$
29	17 28	pm2.65i	$⊢ \neg (x \in ℝ^{+} ⟼ \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem logno1

Proof