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