cxp2limlem

Description: A linear factor grows slower than any exponential with base greater than 1 . (Contributed by Mario Carneiro, 15-Sep-2014)

		Ref	Expression
	Assertion	cxp2limlem	$⊢ (A \in ℝ \land 1 < A) \to (n \in ℝ^{+} ⟼ \frac{n}{A^{n}}) \underset{ℝ}{⇝} 0$

Proof

Step	Hyp	Ref	Expression
1		0red	$⊢ (A \in ℝ \land 1 < A) \to 0 \in ℝ$
2		2rp	$⊢ 2 \in ℝ^{+}$
3		rplogcl	$⊢ (A \in ℝ \land 1 < A) \to \log A \in ℝ^{+}$
4		2z	$⊢ 2 \in ℤ$
5		rpexpcl	$⊢ (\log A \in ℝ^{+} \land 2 \in ℤ) \to {\log A}^{2} \in ℝ^{+}$
6	3 4 5	sylancl	$⊢ (A \in ℝ \land 1 < A) \to {\log A}^{2} \in ℝ^{+}$
7		rpdivcl	$⊢ (2 \in ℝ^{+} \land {\log A}^{2} \in ℝ^{+}) \to \frac{2}{{\log A}^{2}} \in ℝ^{+}$
8	2 6 7	sylancr	$⊢ (A \in ℝ \land 1 < A) \to \frac{2}{{\log A}^{2}} \in ℝ^{+}$
9	8	rpcnd	$⊢ (A \in ℝ \land 1 < A) \to \frac{2}{{\log A}^{2}} \in ℂ$
10		divrcnv	$⊢ \frac{2}{{\log A}^{2}} \in ℂ \to (n \in ℝ^{+} ⟼ \frac{\frac{2}{{\log A}^{2}}}{n}) \underset{ℝ}{⇝} 0$
11	9 10	syl	$⊢ (A \in ℝ \land 1 < A) \to (n \in ℝ^{+} ⟼ \frac{\frac{2}{{\log A}^{2}}}{n}) \underset{ℝ}{⇝} 0$
12	8	rpred	$⊢ (A \in ℝ \land 1 < A) \to \frac{2}{{\log A}^{2}} \in ℝ$
13		rerpdivcl	$⊢ (\frac{2}{{\log A}^{2}} \in ℝ \land n \in ℝ^{+}) \to \frac{\frac{2}{{\log A}^{2}}}{n} \in ℝ$
14	12 13	sylan	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{\frac{2}{{\log A}^{2}}}{n} \in ℝ$
15		simpr	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n \in ℝ^{+}$
16		simpl	$⊢ (A \in ℝ \land 1 < A) \to A \in ℝ$
17		1red	$⊢ (A \in ℝ \land 1 < A) \to 1 \in ℝ$
18		0lt1	$⊢ 0 < 1$
19	18	a1i	$⊢ (A \in ℝ \land 1 < A) \to 0 < 1$
20		simpr	$⊢ (A \in ℝ \land 1 < A) \to 1 < A$
21	1 17 16 19 20	lttrd	$⊢ (A \in ℝ \land 1 < A) \to 0 < A$
22	16 21	elrpd	$⊢ (A \in ℝ \land 1 < A) \to A \in ℝ^{+}$
23		rpre	$⊢ n \in ℝ^{+} \to n \in ℝ$
24		rpcxpcl	$⊢ (A \in ℝ^{+} \land n \in ℝ) \to A^{n} \in ℝ^{+}$
25	22 23 24	syl2an	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to A^{n} \in ℝ^{+}$
26	15 25	rpdivcld	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n}{A^{n}} \in ℝ^{+}$
27	26	rpred	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n}{A^{n}} \in ℝ$
28	3	adantr	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \log A \in ℝ^{+}$
29	15 28	rpmulcld	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n \log A \in ℝ^{+}$
30	29	rpred	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n \log A \in ℝ$
31	30	resqcld	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to {n \log A}^{2} \in ℝ$
32	31	rehalfcld	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{{n \log A}^{2}}{2} \in ℝ$
33		1rp	$⊢ 1 \in ℝ^{+}$
34		rpaddcl	$⊢ (1 \in ℝ^{+} \land n \log A \in ℝ^{+}) \to 1 + n \log A \in ℝ^{+}$
35	33 29 34	sylancr	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to 1 + n \log A \in ℝ^{+}$
36	35	rpred	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to 1 + n \log A \in ℝ$
37	36 32	readdcld	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to 1 + n \log A + (\frac{{n \log A}^{2}}{2}) \in ℝ$
38	30	reefcld	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to e^{n \log A} \in ℝ$
39	32 35	ltaddrp2d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{{n \log A}^{2}}{2} < 1 + n \log A + (\frac{{n \log A}^{2}}{2})$
40		efgt1p2	$⊢ n \log A \in ℝ^{+} \to 1 + n \log A + (\frac{{n \log A}^{2}}{2}) < e^{n \log A}$
41	29 40	syl	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to 1 + n \log A + (\frac{{n \log A}^{2}}{2}) < e^{n \log A}$
42	32 37 38 39 41	lttrd	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{{n \log A}^{2}}{2} < e^{n \log A}$
43	23	adantl	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n \in ℝ$
44	43	recnd	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n \in ℂ$
45	44	sqcld	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n^{2} \in ℂ$
46		2cnd	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to 2 \in ℂ$
47	6	adantr	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to {\log A}^{2} \in ℝ^{+}$
48	47	rpcnd	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to {\log A}^{2} \in ℂ$
49		2ne0	$⊢ 2 \neq 0$
50	49	a1i	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to 2 \neq 0$
51	47	rpne0d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to {\log A}^{2} \neq 0$
52	45 46 48 50 51	divdiv2d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n^{2}}{\frac{2}{{\log A}^{2}}} = \frac{n^{2} {\log A}^{2}}{2}$
53	3	rpcnd	$⊢ (A \in ℝ \land 1 < A) \to \log A \in ℂ$
54	53	adantr	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \log A \in ℂ$
55	44 54	sqmuld	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to {n \log A}^{2} = n^{2} {\log A}^{2}$
56	55	oveq1d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{{n \log A}^{2}}{2} = \frac{n^{2} {\log A}^{2}}{2}$
57	52 56	eqtr4d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n^{2}}{\frac{2}{{\log A}^{2}}} = \frac{{n \log A}^{2}}{2}$
58	16	recnd	$⊢ (A \in ℝ \land 1 < A) \to A \in ℂ$
59	58	adantr	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to A \in ℂ$
60	22	adantr	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to A \in ℝ^{+}$
61	60	rpne0d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to A \neq 0$
62	59 61 44	cxpefd	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to A^{n} = e^{n \log A}$
63	42 57 62	3brtr4d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n^{2}}{\frac{2}{{\log A}^{2}}} < A^{n}$
64		rpexpcl	$⊢ (n \in ℝ^{+} \land 2 \in ℤ) \to n^{2} \in ℝ^{+}$
65	15 4 64	sylancl	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n^{2} \in ℝ^{+}$
66	8	adantr	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{2}{{\log A}^{2}} \in ℝ^{+}$
67	65 66	rpdivcld	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n^{2}}{\frac{2}{{\log A}^{2}}} \in ℝ^{+}$
68	67 25 15	ltdiv2d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to (\frac{n^{2}}{\frac{2}{{\log A}^{2}}} < A^{n} \leftrightarrow \frac{n}{A^{n}} < \frac{n}{\frac{n^{2}}{\frac{2}{{\log A}^{2}}}})$
69	63 68	mpbid	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n}{A^{n}} < \frac{n}{\frac{n^{2}}{\frac{2}{{\log A}^{2}}}}$
70	9	adantr	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{2}{{\log A}^{2}} \in ℂ$
71	65	rpne0d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n^{2} \neq 0$
72	66	rpne0d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{2}{{\log A}^{2}} \neq 0$
73	44 45 70 71 72	divdiv2d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n}{\frac{n^{2}}{\frac{2}{{\log A}^{2}}}} = \frac{n (\frac{2}{{\log A}^{2}})}{n^{2}}$
74	44	sqvald	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n^{2} = n n$
75	74	oveq2d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n (\frac{2}{{\log A}^{2}})}{n^{2}} = \frac{n (\frac{2}{{\log A}^{2}})}{n n}$
76		rpne0	$⊢ n \in ℝ^{+} \to n \neq 0$
77	76	adantl	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to n \neq 0$
78	70 44 44 77 77	divcan5d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n (\frac{2}{{\log A}^{2}})}{n n} = \frac{\frac{2}{{\log A}^{2}}}{n}$
79	73 75 78	3eqtrd	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n}{\frac{n^{2}}{\frac{2}{{\log A}^{2}}}} = \frac{\frac{2}{{\log A}^{2}}}{n}$
80	69 79	breqtrd	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n}{A^{n}} < \frac{\frac{2}{{\log A}^{2}}}{n}$
81	27 14 80	ltled	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to \frac{n}{A^{n}} \leq \frac{\frac{2}{{\log A}^{2}}}{n}$
82	81	adantrr	$⊢ ((A \in ℝ \land 1 < A) \land (n \in ℝ^{+} \land 0 \leq n)) \to \frac{n}{A^{n}} \leq \frac{\frac{2}{{\log A}^{2}}}{n}$
83	26	rpge0d	$⊢ ((A \in ℝ \land 1 < A) \land n \in ℝ^{+}) \to 0 \leq \frac{n}{A^{n}}$
84	83	adantrr	$⊢ ((A \in ℝ \land 1 < A) \land (n \in ℝ^{+} \land 0 \leq n)) \to 0 \leq \frac{n}{A^{n}}$
85	1 1 11 14 27 82 84	rlimsqz2	$⊢ (A \in ℝ \land 1 < A) \to (n \in ℝ^{+} ⟼ \frac{n}{A^{n}}) \underset{ℝ}{⇝} 0$

Metamath Proof Explorer

Theorem cxp2limlem

Proof