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

Metamath Proof Explorer

Theorem divlogrlim

Description: The inverse logarithm function converges to zero. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion divlogrlim ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0

Proof

Step Hyp Ref Expression
1 elioore ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
2 eliooord ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
3 2 simpld ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 1 < 𝑥 )
4 1 3 rplogcld ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
5 4 rprecred ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 / ( log ‘ 𝑥 ) ) ∈ ℝ )
6 5 recnd ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 / ( log ‘ 𝑥 ) ) ∈ ℂ )
7 6 rgen ⊢ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ( 1 / ( log ‘ 𝑥 ) ) ∈ ℂ
8 7 a1i ⊢ ( ⊤ → ∀ 𝑥 ∈ ( 1 (,) +∞ ) ( 1 / ( log ‘ 𝑥 ) ) ∈ ℂ )
9 ioossre ⊢ ( 1 (,) +∞ ) ⊆ ℝ
10 9 a1i ⊢ ( ⊤ → ( 1 (,) +∞ ) ⊆ ℝ )
11 8 10 rlim0lt ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ( 𝑐 < 𝑥 → ( abs ‘ ( 1 / ( log ‘ 𝑥 ) ) ) < 𝑦 ) ) )
12 11 mptru ⊢ ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ( 𝑐 < 𝑥 → ( abs ‘ ( 1 / ( log ‘ 𝑥 ) ) ) < 𝑦 ) )
13 id ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ+ )
14 13 rprecred ⊢ ( 𝑦 ∈ ℝ+ → ( 1 / 𝑦 ) ∈ ℝ )
15 14 reefcld ⊢ ( 𝑦 ∈ ℝ+ → ( exp ‘ ( 1 / 𝑦 ) ) ∈ ℝ )
16 5 ad2antlr ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( 1 / ( log ‘ 𝑥 ) ) ∈ ℝ )
17 1 ad2antlr ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → 𝑥 ∈ ℝ )
18 3 ad2antlr ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → 1 < 𝑥 )
19 17 18 rplogcld ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
20 19 rpreccld ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( 1 / ( log ‘ 𝑥 ) ) ∈ ℝ+ )
21 20 rpge0d ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → 0 ≤ ( 1 / ( log ‘ 𝑥 ) ) )
22 16 21 absidd ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( abs ‘ ( 1 / ( log ‘ 𝑥 ) ) ) = ( 1 / ( log ‘ 𝑥 ) ) )
23 simpll ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → 𝑦 ∈ ℝ+ )
24 4 ad2antlr ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
25 simpr ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 )
26 1rp ⊢ 1 ∈ ℝ+
27 26 a1i ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → 1 ∈ ℝ+ )
28 27 rpred ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → 1 ∈ ℝ )
29 28 17 18 ltled ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → 1 ≤ 𝑥 )
30 17 27 29 rpgecld ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → 𝑥 ∈ ℝ+ )
31 30 reeflogd ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( exp ‘ ( log ‘ 𝑥 ) ) = 𝑥 )
32 25 31 breqtrrd ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( exp ‘ ( 1 / 𝑦 ) ) < ( exp ‘ ( log ‘ 𝑥 ) ) )
33 23 rprecred ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( 1 / 𝑦 ) ∈ ℝ )
34 24 rpred ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( log ‘ 𝑥 ) ∈ ℝ )
35 eflt ⊢ ( ( ( 1 / 𝑦 ) ∈ ℝ ∧ ( log ‘ 𝑥 ) ∈ ℝ ) → ( ( 1 / 𝑦 ) < ( log ‘ 𝑥 ) ↔ ( exp ‘ ( 1 / 𝑦 ) ) < ( exp ‘ ( log ‘ 𝑥 ) ) ) )
36 33 34 35 syl2anc ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( ( 1 / 𝑦 ) < ( log ‘ 𝑥 ) ↔ ( exp ‘ ( 1 / 𝑦 ) ) < ( exp ‘ ( log ‘ 𝑥 ) ) ) )
37 32 36 mpbird ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( 1 / 𝑦 ) < ( log ‘ 𝑥 ) )
38 23 24 37 ltrec1d ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( 1 / ( log ‘ 𝑥 ) ) < 𝑦 )
39 22 38 eqbrtrd ⊢ ( ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) → ( abs ‘ ( 1 / ( log ‘ 𝑥 ) ) ) < 𝑦 )
40 39 ex ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 → ( abs ‘ ( 1 / ( log ‘ 𝑥 ) ) ) < 𝑦 ) )
41 40 ralrimiva ⊢ ( 𝑦 ∈ ℝ+ → ∀ 𝑥 ∈ ( 1 (,) +∞ ) ( ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 → ( abs ‘ ( 1 / ( log ‘ 𝑥 ) ) ) < 𝑦 ) )
42 breq1 ⊢ ( 𝑐 = ( exp ‘ ( 1 / 𝑦 ) ) → ( 𝑐 < 𝑥 ↔ ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 ) )
43 42 rspceaimv ⊢ ( ( ( exp ‘ ( 1 / 𝑦 ) ) ∈ ℝ ∧ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ( ( exp ‘ ( 1 / 𝑦 ) ) < 𝑥 → ( abs ‘ ( 1 / ( log ‘ 𝑥 ) ) ) < 𝑦 ) ) → ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ( 𝑐 < 𝑥 → ( abs ‘ ( 1 / ( log ‘ 𝑥 ) ) ) < 𝑦 ) )
44 15 41 43 syl2anc ⊢ ( 𝑦 ∈ ℝ+ → ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ ( 1 (,) +∞ ) ( 𝑐 < 𝑥 → ( abs ‘ ( 1 / ( log ‘ 𝑥 ) ) ) < 𝑦 ) )
45 12 44 mprgbir ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0