divlogrlim

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

		Ref	Expression
	Assertion	divlogrlim	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0$

Proof

Step	Hyp	Ref	Expression
1		elioore	$⊢ x \in (1, +∞) \to x \in ℝ$
2		eliooord	$⊢ x \in (1, +∞) \to (1 < x \land x < +∞)$
3	2	simpld	$⊢ x \in (1, +∞) \to 1 < x$
4	1 3	rplogcld	$⊢ x \in (1, +∞) \to \log x \in ℝ^{+}$
5	4	rprecred	$⊢ x \in (1, +∞) \to \frac{1}{\log x} \in ℝ$
6	5	recnd	$⊢ x \in (1, +∞) \to \frac{1}{\log x} \in ℂ$
7	6	rgen	$⊢ \forall x \in (1, +∞) \frac{1}{\log x} \in ℂ$
8	7	a1i	$⊢ ⊤ \to \forall x \in (1, +∞) \frac{1}{\log x} \in ℂ$
9		ioossre	$⊢ (1, +∞) \subseteq ℝ$
10	9	a1i	$⊢ ⊤ \to (1, +∞) \subseteq ℝ$
11	8 10	rlim0lt	$⊢ ⊤ \to ((x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0 \leftrightarrow \forall y \in ℝ^{+} \exists c \in ℝ \forall x \in (1, +∞) (c < x \to \|\frac{1}{\log x}\| < y))$
12	11	mptru	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0 \leftrightarrow \forall y \in ℝ^{+} \exists c \in ℝ \forall x \in (1, +∞) (c < x \to \|\frac{1}{\log x}\| < y)$
13		id	$⊢ y \in ℝ^{+} \to y \in ℝ^{+}$
14	13	rprecred	$⊢ y \in ℝ^{+} \to \frac{1}{y} \in ℝ$
15	14	reefcld	$⊢ y \in ℝ^{+} \to e^{\frac{1}{y}} \in ℝ$
16	5	ad2antlr	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \frac{1}{\log x} \in ℝ$
17	1	ad2antlr	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to x \in ℝ$
18	3	ad2antlr	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to 1 < x$
19	17 18	rplogcld	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \log x \in ℝ^{+}$
20	19	rpreccld	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \frac{1}{\log x} \in ℝ^{+}$
21	20	rpge0d	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to 0 \leq \frac{1}{\log x}$
22	16 21	absidd	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \|\frac{1}{\log x}\| = \frac{1}{\log x}$
23		simpll	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to y \in ℝ^{+}$
24	4	ad2antlr	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \log x \in ℝ^{+}$
25		simpr	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to e^{\frac{1}{y}} < x$
26		1rp	$⊢ 1 \in ℝ^{+}$
27	26	a1i	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to 1 \in ℝ^{+}$
28	27	rpred	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to 1 \in ℝ$
29	28 17 18	ltled	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to 1 \leq x$
30	17 27 29	rpgecld	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to x \in ℝ^{+}$
31	30	reeflogd	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to e^{\log x} = x$
32	25 31	breqtrrd	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to e^{\frac{1}{y}} < e^{\log x}$
33	23	rprecred	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \frac{1}{y} \in ℝ$
34	24	rpred	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \log x \in ℝ$
35		eflt	$⊢ (\frac{1}{y} \in ℝ \land \log x \in ℝ) \to (\frac{1}{y} < \log x \leftrightarrow e^{\frac{1}{y}} < e^{\log x})$
36	33 34 35	syl2anc	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to (\frac{1}{y} < \log x \leftrightarrow e^{\frac{1}{y}} < e^{\log x})$
37	32 36	mpbird	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \frac{1}{y} < \log x$
38	23 24 37	ltrec1d	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \frac{1}{\log x} < y$
39	22 38	eqbrtrd	$⊢ ((y \in ℝ^{+} \land x \in (1, +∞)) \land e^{\frac{1}{y}} < x) \to \|\frac{1}{\log x}\| < y$
40	39	ex	$⊢ (y \in ℝ^{+} \land x \in (1, +∞)) \to (e^{\frac{1}{y}} < x \to \|\frac{1}{\log x}\| < y)$
41	40	ralrimiva	$⊢ y \in ℝ^{+} \to \forall x \in (1, +∞) (e^{\frac{1}{y}} < x \to \|\frac{1}{\log x}\| < y)$
42		breq1	$⊢ c = e^{\frac{1}{y}} \to (c < x \leftrightarrow e^{\frac{1}{y}} < x)$
43	42	rspceaimv	$⊢ (e^{\frac{1}{y}} \in ℝ \land \forall x \in (1, +∞) (e^{\frac{1}{y}} < x \to \|\frac{1}{\log x}\| < y)) \to \exists c \in ℝ \forall x \in (1, +∞) (c < x \to \|\frac{1}{\log x}\| < y)$
44	15 41 43	syl2anc	$⊢ y \in ℝ^{+} \to \exists c \in ℝ \forall x \in (1, +∞) (c < x \to \|\frac{1}{\log x}\| < y)$
45	12 44	mprgbir	$⊢ (x \in (1, +∞) ⟼ \frac{1}{\log x}) \underset{ℝ}{⇝} 0$

Metamath Proof Explorer

Theorem divlogrlim

Proof