cxploglim

Description: The logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 18-Sep-2014)

		Ref	Expression
	Assertion	cxploglim	$⊢ A \in ℝ^{+} \to (n \in ℝ^{+} ⟼ \frac{\log n}{n^{A}}) \underset{ℝ}{⇝} 0$

Proof

Step	Hyp	Ref	Expression
1		rpre	$⊢ A \in ℝ^{+} \to A \in ℝ$
2		reefcl	$⊢ A \in ℝ \to e^{A} \in ℝ$
3	1 2	syl	$⊢ A \in ℝ^{+} \to e^{A} \in ℝ$
4		efgt1	$⊢ A \in ℝ^{+} \to 1 < e^{A}$
5		cxp2limlem	$⊢ (e^{A} \in ℝ \land 1 < e^{A}) \to (m \in ℝ^{+} ⟼ \frac{m}{{e^{A}}^{m}}) \underset{ℝ}{⇝} 0$
6	3 4 5	syl2anc	$⊢ A \in ℝ^{+} \to (m \in ℝ^{+} ⟼ \frac{m}{{e^{A}}^{m}}) \underset{ℝ}{⇝} 0$
7		reefcl	$⊢ z \in ℝ \to e^{z} \in ℝ$
8	7	adantl	$⊢ (A \in ℝ^{+} \land z \in ℝ) \to e^{z} \in ℝ$
9		1re	$⊢ 1 \in ℝ$
10		ifcl	$⊢ (e^{z} \in ℝ \land 1 \in ℝ) \to if (1 \leq e^{z}, e^{z}, 1) \in ℝ$
11	8 9 10	sylancl	$⊢ (A \in ℝ^{+} \land z \in ℝ) \to if (1 \leq e^{z}, e^{z}, 1) \in ℝ$
12		rpre	$⊢ n \in ℝ^{+} \to n \in ℝ$
13		maxlt	$⊢ (1 \in ℝ \land e^{z} \in ℝ \land n \in ℝ) \to (if (1 \leq e^{z}, e^{z}, 1) < n \leftrightarrow (1 < n \land e^{z} < n))$
14	9 8 12 13	mp3an3an	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land n \in ℝ^{+}) \to (if (1 \leq e^{z}, e^{z}, 1) < n \leftrightarrow (1 < n \land e^{z} < n))$
15		simprrr	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to e^{z} < n$
16		reeflog	$⊢ n \in ℝ^{+} \to e^{\log n} = n$
17	16	ad2antrl	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to e^{\log n} = n$
18	15 17	breqtrrd	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to e^{z} < e^{\log n}$
19		simplr	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to z \in ℝ$
20	12	ad2antrl	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to n \in ℝ$
21		simprrl	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to 1 < n$
22	20 21	rplogcld	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to \log n \in ℝ^{+}$
23	22	rpred	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to \log n \in ℝ$
24		eflt	$⊢ (z \in ℝ \land \log n \in ℝ) \to (z < \log n \leftrightarrow e^{z} < e^{\log n})$
25	19 23 24	syl2anc	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to (z < \log n \leftrightarrow e^{z} < e^{\log n})$
26	18 25	mpbird	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to z < \log n$
27		breq2	$⊢ m = \log n \to (z < m \leftrightarrow z < \log n)$
28		id	$⊢ m = \log n \to m = \log n$
29		oveq2	$⊢ m = \log n \to {e^{A}}^{m} = {e^{A}}^{\log n}$
30	28 29	oveq12d	$⊢ m = \log n \to \frac{m}{{e^{A}}^{m}} = \frac{\log n}{{e^{A}}^{\log n}}$
31	30	fveq2d	$⊢ m = \log n \to \|\frac{m}{{e^{A}}^{m}}\| = \|\frac{\log n}{{e^{A}}^{\log n}}\|$
32	31	breq1d	$⊢ m = \log n \to (\|\frac{m}{{e^{A}}^{m}}\| < x \leftrightarrow \|\frac{\log n}{{e^{A}}^{\log n}}\| < x)$
33	27 32	imbi12d	$⊢ m = \log n \to ((z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \leftrightarrow (z < \log n \to \|\frac{\log n}{{e^{A}}^{\log n}}\| < x))$
34	33	rspcv	$⊢ \log n \in ℝ^{+} \to (\forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to (z < \log n \to \|\frac{\log n}{{e^{A}}^{\log n}}\| < x))$
35	22 34	syl	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to (\forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to (z < \log n \to \|\frac{\log n}{{e^{A}}^{\log n}}\| < x))$
36	26 35	mpid	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to (\forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to \|\frac{\log n}{{e^{A}}^{\log n}}\| < x)$
37	1	ad2antrr	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to A \in ℝ$
38	37	relogefd	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to \log e^{A} = A$
39	38	oveq2d	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to \log n \log e^{A} = \log n A$
40	22	rpcnd	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to \log n \in ℂ$
41		rpcn	$⊢ A \in ℝ^{+} \to A \in ℂ$
42	41	ad2antrr	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to A \in ℂ$
43	40 42	mulcomd	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to \log n A = A \log n$
44	39 43	eqtrd	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to \log n \log e^{A} = A \log n$
45	44	fveq2d	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to e^{\log n \log e^{A}} = e^{A \log n}$
46	3	ad2antrr	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to e^{A} \in ℝ$
47	46	recnd	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to e^{A} \in ℂ$
48		efne0	$⊢ A \in ℂ \to e^{A} \neq 0$
49	42 48	syl	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to e^{A} \neq 0$
50	47 49 40	cxpefd	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to {e^{A}}^{\log n} = e^{\log n \log e^{A}}$
51		rpcn	$⊢ n \in ℝ^{+} \to n \in ℂ$
52	51	ad2antrl	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to n \in ℂ$
53		rpne0	$⊢ n \in ℝ^{+} \to n \neq 0$
54	53	ad2antrl	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to n \neq 0$
55	52 54 42	cxpefd	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to n^{A} = e^{A \log n}$
56	45 50 55	3eqtr4d	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to {e^{A}}^{\log n} = n^{A}$
57	56	oveq2d	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to \frac{\log n}{{e^{A}}^{\log n}} = \frac{\log n}{n^{A}}$
58	57	fveq2d	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to \|\frac{\log n}{{e^{A}}^{\log n}}\| = \|\frac{\log n}{n^{A}}\|$
59	58	breq1d	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to (\|\frac{\log n}{{e^{A}}^{\log n}}\| < x \leftrightarrow \|\frac{\log n}{n^{A}}\| < x)$
60	36 59	sylibd	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land (n \in ℝ^{+} \land (1 < n \land e^{z} < n))) \to (\forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to \|\frac{\log n}{n^{A}}\| < x)$
61	60	expr	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land n \in ℝ^{+}) \to ((1 < n \land e^{z} < n) \to (\forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to \|\frac{\log n}{n^{A}}\| < x))$
62	14 61	sylbid	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land n \in ℝ^{+}) \to (if (1 \leq e^{z}, e^{z}, 1) < n \to (\forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to \|\frac{\log n}{n^{A}}\| < x))$
63	62	com23	$⊢ ((A \in ℝ^{+} \land z \in ℝ) \land n \in ℝ^{+}) \to (\forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to (if (1 \leq e^{z}, e^{z}, 1) < n \to \|\frac{\log n}{n^{A}}\| < x))$
64	63	ralrimdva	$⊢ (A \in ℝ^{+} \land z \in ℝ) \to (\forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to \forall n \in ℝ^{+} (if (1 \leq e^{z}, e^{z}, 1) < n \to \|\frac{\log n}{n^{A}}\| < x))$
65		breq1	$⊢ y = if (1 \leq e^{z}, e^{z}, 1) \to (y < n \leftrightarrow if (1 \leq e^{z}, e^{z}, 1) < n)$
66	65	rspceaimv	$⊢ (if (1 \leq e^{z}, e^{z}, 1) \in ℝ \land \forall n \in ℝ^{+} (if (1 \leq e^{z}, e^{z}, 1) < n \to \|\frac{\log n}{n^{A}}\| < x)) \to \exists y \in ℝ \forall n \in ℝ^{+} (y < n \to \|\frac{\log n}{n^{A}}\| < x)$
67	11 64 66	syl6an	$⊢ (A \in ℝ^{+} \land z \in ℝ) \to (\forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to \exists y \in ℝ \forall n \in ℝ^{+} (y < n \to \|\frac{\log n}{n^{A}}\| < x))$
68	67	rexlimdva	$⊢ A \in ℝ^{+} \to (\exists z \in ℝ \forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to \exists y \in ℝ \forall n \in ℝ^{+} (y < n \to \|\frac{\log n}{n^{A}}\| < x))$
69	68	ralimdv	$⊢ A \in ℝ^{+} \to (\forall x \in ℝ^{+} \exists z \in ℝ \forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x) \to \forall x \in ℝ^{+} \exists y \in ℝ \forall n \in ℝ^{+} (y < n \to \|\frac{\log n}{n^{A}}\| < x))$
70		simpr	$⊢ (A \in ℝ^{+} \land m \in ℝ^{+}) \to m \in ℝ^{+}$
71	1	adantr	$⊢ (A \in ℝ^{+} \land m \in ℝ^{+}) \to A \in ℝ$
72	71	rpefcld	$⊢ (A \in ℝ^{+} \land m \in ℝ^{+}) \to e^{A} \in ℝ^{+}$
73		rpre	$⊢ m \in ℝ^{+} \to m \in ℝ$
74	73	adantl	$⊢ (A \in ℝ^{+} \land m \in ℝ^{+}) \to m \in ℝ$
75	72 74	rpcxpcld	$⊢ (A \in ℝ^{+} \land m \in ℝ^{+}) \to {e^{A}}^{m} \in ℝ^{+}$
76	70 75	rpdivcld	$⊢ (A \in ℝ^{+} \land m \in ℝ^{+}) \to \frac{m}{{e^{A}}^{m}} \in ℝ^{+}$
77	76	rpcnd	$⊢ (A \in ℝ^{+} \land m \in ℝ^{+}) \to \frac{m}{{e^{A}}^{m}} \in ℂ$
78	77	ralrimiva	$⊢ A \in ℝ^{+} \to \forall m \in ℝ^{+} \frac{m}{{e^{A}}^{m}} \in ℂ$
79		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
80	79	a1i	$⊢ A \in ℝ^{+} \to ℝ^{+} \subseteq ℝ$
81	78 80	rlim0lt	$⊢ A \in ℝ^{+} \to ((m \in ℝ^{+} ⟼ \frac{m}{{e^{A}}^{m}}) \underset{ℝ}{⇝} 0 \leftrightarrow \forall x \in ℝ^{+} \exists z \in ℝ \forall m \in ℝ^{+} (z < m \to \|\frac{m}{{e^{A}}^{m}}\| < x))$
82		relogcl	$⊢ n \in ℝ^{+} \to \log n \in ℝ$
83	82	adantl	$⊢ (A \in ℝ^{+} \land n \in ℝ^{+}) \to \log n \in ℝ$
84		simpr	$⊢ (A \in ℝ^{+} \land n \in ℝ^{+}) \to n \in ℝ^{+}$
85	1	adantr	$⊢ (A \in ℝ^{+} \land n \in ℝ^{+}) \to A \in ℝ$
86	84 85	rpcxpcld	$⊢ (A \in ℝ^{+} \land n \in ℝ^{+}) \to n^{A} \in ℝ^{+}$
87	83 86	rerpdivcld	$⊢ (A \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{\log n}{n^{A}} \in ℝ$
88	87	recnd	$⊢ (A \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{\log n}{n^{A}} \in ℂ$
89	88	ralrimiva	$⊢ A \in ℝ^{+} \to \forall n \in ℝ^{+} \frac{\log n}{n^{A}} \in ℂ$
90	89 80	rlim0lt	$⊢ A \in ℝ^{+} \to ((n \in ℝ^{+} ⟼ \frac{\log n}{n^{A}}) \underset{ℝ}{⇝} 0 \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℝ \forall n \in ℝ^{+} (y < n \to \|\frac{\log n}{n^{A}}\| < x))$
91	69 81 90	3imtr4d	$⊢ A \in ℝ^{+} \to ((m \in ℝ^{+} ⟼ \frac{m}{{e^{A}}^{m}}) \underset{ℝ}{⇝} 0 \to (n \in ℝ^{+} ⟼ \frac{\log n}{n^{A}}) \underset{ℝ}{⇝} 0)$
92	6 91	mpd	$⊢ A \in ℝ^{+} \to (n \in ℝ^{+} ⟼ \frac{\log n}{n^{A}}) \underset{ℝ}{⇝} 0$

Metamath Proof Explorer

Theorem cxploglim

Proof