cxp2lim

Description: Any power grows slower than any exponential with base greater than 1 . (Contributed by Mario Carneiro, 18-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		elicopnf	$⊢ 1 \in ℝ \to (n \in [1, +∞) \leftrightarrow (n \in ℝ \land 1 \leq n))$
3	1 2	ax-mp	$⊢ n \in [1, +∞) \leftrightarrow (n \in ℝ \land 1 \leq n)$
4	3	simplbi	$⊢ n \in [1, +∞) \to n \in ℝ$
5		0red	$⊢ n \in [1, +∞) \to 0 \in ℝ$
6		1red	$⊢ n \in [1, +∞) \to 1 \in ℝ$
7		0lt1	$⊢ 0 < 1$
8	7	a1i	$⊢ n \in [1, +∞) \to 0 < 1$
9	3	simprbi	$⊢ n \in [1, +∞) \to 1 \leq n$
10	5 6 4 8 9	ltletrd	$⊢ n \in [1, +∞) \to 0 < n$
11	4 10	elrpd	$⊢ n \in [1, +∞) \to n \in ℝ^{+}$
12	11	ssriv	$⊢ [1, +∞) \subseteq ℝ^{+}$
13		resmpt	$⊢ [1, +∞) \subseteq ℝ^{+} \to {(n \in ℝ^{+} ⟼ \frac{n^{A}}{B^{n}}) ↾}_{[1, +∞)} = (n \in [1, +∞) ⟼ \frac{n^{A}}{B^{n}})$
14	12 13	ax-mp	$⊢ {(n \in ℝ^{+} ⟼ \frac{n^{A}}{B^{n}}) ↾}_{[1, +∞)} = (n \in [1, +∞) ⟼ \frac{n^{A}}{B^{n}})$
15		0red	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 0 \in ℝ$
16	12	a1i	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to [1, +∞) \subseteq ℝ^{+}$
17		rpre	$⊢ n \in ℝ^{+} \to n \in ℝ$
18	17	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to n \in ℝ$
19		rpge0	$⊢ n \in ℝ^{+} \to 0 \leq n$
20	19	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to 0 \leq n$
21		simpl2	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to B \in ℝ$
22		0red	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to 0 \in ℝ$
23		1red	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to 1 \in ℝ$
24	7	a1i	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to 0 < 1$
25		simpl3	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to 1 < B$
26	22 23 21 24 25	lttrd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to 0 < B$
27	21 26	elrpd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to B \in ℝ^{+}$
28	27 18	rpcxpcld	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to B^{n} \in ℝ^{+}$
29		simp1	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to A \in ℝ$
30		ifcl	$⊢ (A \in ℝ \land 1 \in ℝ) \to if (1 \leq A, A, 1) \in ℝ$
31	29 1 30	sylancl	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to if (1 \leq A, A, 1) \in ℝ$
32		1red	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 1 \in ℝ$
33	7	a1i	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 0 < 1$
34		max1	$⊢ (1 \in ℝ \land A \in ℝ) \to 1 \leq if (1 \leq A, A, 1)$
35	1 29 34	sylancr	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 1 \leq if (1 \leq A, A, 1)$
36	15 32 31 33 35	ltletrd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 0 < if (1 \leq A, A, 1)$
37	31 36	elrpd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to if (1 \leq A, A, 1) \in ℝ^{+}$
38	37	rprecred	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to \frac{1}{if (1 \leq A, A, 1)} \in ℝ$
39	38	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to \frac{1}{if (1 \leq A, A, 1)} \in ℝ$
40	28 39	rpcxpcld	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to {(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}} \in ℝ^{+}$
41	31	recnd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to if (1 \leq A, A, 1) \in ℂ$
42	41	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to if (1 \leq A, A, 1) \in ℂ$
43	18 20 40 42	divcxpd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to {(\frac{n}{{(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}}})}^{if (1 \leq A, A, 1)} = \frac{n^{if (1 \leq A, A, 1)}}{{({B^{n}}^{\frac{1}{if (1 \leq A, A, 1)}})}^{if (1 \leq A, A, 1)}}$
44	37	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to if (1 \leq A, A, 1) \in ℝ^{+}$
45	44	rpne0d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to if (1 \leq A, A, 1) \neq 0$
46	42 45	recid2d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to (\frac{1}{if (1 \leq A, A, 1)}) if (1 \leq A, A, 1) = 1$
47	46	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to {(B^{n})}^{(\frac{1}{if (1 \leq A, A, 1)}) if (1 \leq A, A, 1)} = {(B^{n})}^{1}$
48	28 39 42	cxpmuld	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to {(B^{n})}^{(\frac{1}{if (1 \leq A, A, 1)}) if (1 \leq A, A, 1)} = {({B^{n}}^{\frac{1}{if (1 \leq A, A, 1)}})}^{if (1 \leq A, A, 1)}$
49	28	rpcnd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to B^{n} \in ℂ$
50	49	cxp1d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to {(B^{n})}^{1} = B^{n}$
51	47 48 50	3eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to {({B^{n}}^{\frac{1}{if (1 \leq A, A, 1)}})}^{if (1 \leq A, A, 1)} = B^{n}$
52	51	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to \frac{n^{if (1 \leq A, A, 1)}}{{({B^{n}}^{\frac{1}{if (1 \leq A, A, 1)}})}^{if (1 \leq A, A, 1)}} = \frac{n^{if (1 \leq A, A, 1)}}{B^{n}}$
53	43 52	eqtrd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to {(\frac{n}{{(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}}})}^{if (1 \leq A, A, 1)} = \frac{n^{if (1 \leq A, A, 1)}}{B^{n}}$
54	53	mpteq2dva	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in ℝ^{+} ⟼ {(\frac{n}{{(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}}})}^{if (1 \leq A, A, 1)}) = (n \in ℝ^{+} ⟼ \frac{n^{if (1 \leq A, A, 1)}}{B^{n}})$
55		ovexd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to \frac{n}{{(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}}} \in V$
56	18	recnd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to n \in ℂ$
57	38	recnd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to \frac{1}{if (1 \leq A, A, 1)} \in ℂ$
58	57	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to \frac{1}{if (1 \leq A, A, 1)} \in ℂ$
59	56 58	mulcomd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to n (\frac{1}{if (1 \leq A, A, 1)}) = (\frac{1}{if (1 \leq A, A, 1)}) n$
60	59	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to B^{n (\frac{1}{if (1 \leq A, A, 1)})} = B^{(\frac{1}{if (1 \leq A, A, 1)}) n}$
61	27 18 58	cxpmuld	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to B^{n (\frac{1}{if (1 \leq A, A, 1)})} = {(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}}$
62	27 39 56	cxpmuld	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to B^{(\frac{1}{if (1 \leq A, A, 1)}) n} = {(B^{\frac{1}{if (1 \leq A, A, 1)}})}^{n}$
63	60 61 62	3eqtr3d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to {(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}} = {(B^{\frac{1}{if (1 \leq A, A, 1)}})}^{n}$
64	63	oveq2d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to \frac{n}{{(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}}} = \frac{n}{{(B^{\frac{1}{if (1 \leq A, A, 1)}})}^{n}}$
65	64	mpteq2dva	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in ℝ^{+} ⟼ \frac{n}{{(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}}}) = (n \in ℝ^{+} ⟼ \frac{n}{{(B^{\frac{1}{if (1 \leq A, A, 1)}})}^{n}})$
66		simp2	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to B \in ℝ$
67		simp3	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 1 < B$
68	15 32 66 33 67	lttrd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 0 < B$
69	66 68	elrpd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to B \in ℝ^{+}$
70	69 38	rpcxpcld	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to B^{\frac{1}{if (1 \leq A, A, 1)}} \in ℝ^{+}$
71	70	rpred	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to B^{\frac{1}{if (1 \leq A, A, 1)}} \in ℝ$
72	57	1cxpd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 1^{\frac{1}{if (1 \leq A, A, 1)}} = 1$
73		0le1	$⊢ 0 \leq 1$
74	73	a1i	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 0 \leq 1$
75	69	rpge0d	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 0 \leq B$
76	37	rpreccld	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to \frac{1}{if (1 \leq A, A, 1)} \in ℝ^{+}$
77	32 74 66 75 76	cxplt2d	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (1 < B \leftrightarrow 1^{\frac{1}{if (1 \leq A, A, 1)}} < B^{\frac{1}{if (1 \leq A, A, 1)}})$
78	67 77	mpbid	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 1^{\frac{1}{if (1 \leq A, A, 1)}} < B^{\frac{1}{if (1 \leq A, A, 1)}}$
79	72 78	eqbrtrrd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 1 < B^{\frac{1}{if (1 \leq A, A, 1)}}$
80		cxp2limlem	$⊢ (B^{\frac{1}{if (1 \leq A, A, 1)}} \in ℝ \land 1 < B^{\frac{1}{if (1 \leq A, A, 1)}}) \to (n \in ℝ^{+} ⟼ \frac{n}{{(B^{\frac{1}{if (1 \leq A, A, 1)}})}^{n}}) \underset{ℝ}{⇝} 0$
81	71 79 80	syl2anc	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in ℝ^{+} ⟼ \frac{n}{{(B^{\frac{1}{if (1 \leq A, A, 1)}})}^{n}}) \underset{ℝ}{⇝} 0$
82	65 81	eqbrtrd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in ℝ^{+} ⟼ \frac{n}{{(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}}}) \underset{ℝ}{⇝} 0$
83	55 82 37	rlimcxp	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in ℝ^{+} ⟼ {(\frac{n}{{(B^{n})}^{\frac{1}{if (1 \leq A, A, 1)}}})}^{if (1 \leq A, A, 1)}) \underset{ℝ}{⇝} 0$
84	54 83	eqbrtrrd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in ℝ^{+} ⟼ \frac{n^{if (1 \leq A, A, 1)}}{B^{n}}) \underset{ℝ}{⇝} 0$
85	16 84	rlimres2	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in [1, +∞) ⟼ \frac{n^{if (1 \leq A, A, 1)}}{B^{n}}) \underset{ℝ}{⇝} 0$
86		simpr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to n \in ℝ^{+}$
87	31	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to if (1 \leq A, A, 1) \in ℝ$
88	86 87	rpcxpcld	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to n^{if (1 \leq A, A, 1)} \in ℝ^{+}$
89	88 28	rpdivcld	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to \frac{n^{if (1 \leq A, A, 1)}}{B^{n}} \in ℝ^{+}$
90	89	rpred	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to \frac{n^{if (1 \leq A, A, 1)}}{B^{n}} \in ℝ$
91	11 90	sylan2	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to \frac{n^{if (1 \leq A, A, 1)}}{B^{n}} \in ℝ$
92		simpl1	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to A \in ℝ$
93	86 92	rpcxpcld	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to n^{A} \in ℝ^{+}$
94	93 28	rpdivcld	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to \frac{n^{A}}{B^{n}} \in ℝ^{+}$
95	11 94	sylan2	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to \frac{n^{A}}{B^{n}} \in ℝ^{+}$
96	95	rpred	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to \frac{n^{A}}{B^{n}} \in ℝ$
97	11 93	sylan2	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to n^{A} \in ℝ^{+}$
98	97	rpred	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to n^{A} \in ℝ$
99	11 88	sylan2	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to n^{if (1 \leq A, A, 1)} \in ℝ^{+}$
100	99	rpred	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to n^{if (1 \leq A, A, 1)} \in ℝ$
101	11 28	sylan2	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to B^{n} \in ℝ^{+}$
102	4	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to n \in ℝ$
103	9	adantl	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to 1 \leq n$
104		simpl1	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to A \in ℝ$
105	31	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to if (1 \leq A, A, 1) \in ℝ$
106		max2	$⊢ (1 \in ℝ \land A \in ℝ) \to A \leq if (1 \leq A, A, 1)$
107	1 104 106	sylancr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to A \leq if (1 \leq A, A, 1)$
108	102 103 104 105 107	cxplead	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to n^{A} \leq n^{if (1 \leq A, A, 1)}$
109	98 100 101 108	lediv1dd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to \frac{n^{A}}{B^{n}} \leq \frac{n^{if (1 \leq A, A, 1)}}{B^{n}}$
110	109	adantrr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in [1, +∞) \land 0 \leq n)) \to \frac{n^{A}}{B^{n}} \leq \frac{n^{if (1 \leq A, A, 1)}}{B^{n}}$
111	95	rpge0d	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in [1, +∞)) \to 0 \leq \frac{n^{A}}{B^{n}}$
112	111	adantrr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in [1, +∞) \land 0 \leq n)) \to 0 \leq \frac{n^{A}}{B^{n}}$
113	15 15 85 91 96 110 112	rlimsqz2	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in [1, +∞) ⟼ \frac{n^{A}}{B^{n}}) \underset{ℝ}{⇝} 0$
114	14 113	eqbrtrid	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to ({(n \in ℝ^{+} ⟼ \frac{n^{A}}{B^{n}}) ↾}_{[1, +∞)}) \underset{ℝ}{⇝} 0$
115	94	rpcnd	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land n \in ℝ^{+}) \to \frac{n^{A}}{B^{n}} \in ℂ$
116	115	fmpttd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in ℝ^{+} ⟼ \frac{n^{A}}{B^{n}}) : ℝ^{+} ⟶ ℂ$
117		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
118	117	a1i	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to ℝ^{+} \subseteq ℝ$
119	116 118 32	rlimresb	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to ((n \in ℝ^{+} ⟼ \frac{n^{A}}{B^{n}}) \underset{ℝ}{⇝} 0 \leftrightarrow ({(n \in ℝ^{+} ⟼ \frac{n^{A}}{B^{n}}) ↾}_{[1, +∞)}) \underset{ℝ}{⇝} 0)$
120	114 119	mpbird	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (n \in ℝ^{+} ⟼ \frac{n^{A}}{B^{n}}) \underset{ℝ}{⇝} 0$

Metamath Proof Explorer

Theorem cxp2lim

Proof