This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ¬ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 elioore ⊢ ( 𝑦 ∈ ( 1 (,) +∞ ) → 𝑦 ∈ ℝ )
2 1 adantl ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → 𝑦 ∈ ℝ )
3 1rp ⊢ 1 ∈ ℝ+
4 3 a1i ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
5 1red ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
6 eliooord ⊢ ( 𝑦 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑦 ∧ 𝑦 < +∞ ) )
7 6 adantl ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑦 ∧ 𝑦 < +∞ ) )
8 7 simpld ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑦 )
9 5 2 8 ltled ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑦 )
10 2 4 9 rpgecld ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → 𝑦 ∈ ℝ+ )
11 10 ex ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → ( 𝑦 ∈ ( 1 (,) +∞ ) → 𝑦 ∈ ℝ+ ) )
12 11 ssrdv ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → ( 1 (,) +∞ ) ⊆ ℝ+ )
13 fveq2 ⊢ ( 𝑥 = 𝑦 → ( log ‘ 𝑥 ) = ( log ‘ 𝑦 ) )
14 13 cbvmptv ⊢ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) = ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) )
15 14 eleq1i ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ↔ ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) ∈ 𝑂(1) )
16 15 biimpi ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → ( 𝑦 ∈ ℝ+ ↦ ( log ‘ 𝑦 ) ) ∈ 𝑂(1) )
17 12 16 o1res2 ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → ( 𝑦 ∈ ( 1 (,) +∞ ) ↦ ( log ‘ 𝑦 ) ) ∈ 𝑂(1) )
18 1red ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → 1 ∈ ℝ )
19 18 rexrd ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → 1 ∈ ℝ* )
20 18 renepnfd ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → 1 ≠ +∞ )
21 ioopnfsup ⊢ ( ( 1 ∈ ℝ* ∧ 1 ≠ +∞ ) → sup ( ( 1 (,) +∞ ) , ℝ* , < ) = +∞ )
22 19 20 21 syl2anc ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → sup ( ( 1 (,) +∞ ) , ℝ* , < ) = +∞ )
23 divlogrlim ⊢ ( 𝑦 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑦 ) ) ) ⇝𝑟 0
24 23 a1i ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → ( 𝑦 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑦 ) ) ) ⇝𝑟 0 )
25 2 8 rplogcld ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑦 ) ∈ ℝ+ )
26 25 rpcnd ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑦 ) ∈ ℂ )
27 25 rpne0d ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) ∧ 𝑦 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑦 ) ≠ 0 )
28 22 24 26 27 rlimno1 ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1) → ¬ ( 𝑦 ∈ ( 1 (,) +∞ ) ↦ ( log ‘ 𝑦 ) ) ∈ 𝑂(1) )
29 17 28 pm2.65i ⊢ ¬ ( 𝑥 ∈ ℝ+ ↦ ( log ‘ 𝑥 ) ) ∈ 𝑂(1)