Theorem explecnv

Description: A sequence of terms converges to zero when it is less than powers of a number A whose absolute value is smaller than 1. (Contributed by NM, 19-Jul-2008) (Revised by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Hypotheses	explecnv.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	explecnv.2	$$⊢\phi \to F\in V$$
	explecnv.3	$$⊢\phi \to M\in \mathbb{Z}$$
	explecnv.5	$$⊢\phi \to A\in ℝ$$
	explecnv.4	$$⊢\phi \to \left|A\right|<1$$
	explecnv.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
	explecnv.7	$$⊢\left(\phi \wedge k\in Z\right)\to \left|F\left(k\right)\right|\le A^k$$
Assertion	explecnv	$$⊢\phi \to F⇝0$$

Proof

Step	Hyp	Ref	Expression
1		explecnv.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		explecnv.2	$$⊢\phi \to F\in V$$
3		explecnv.3	$$⊢\phi \to M\in \mathbb{Z}$$
4		explecnv.5	$$⊢\phi \to A\in ℝ$$
5		explecnv.4	$$⊢\phi \to \left|A\right|<1$$
6		explecnv.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
7		explecnv.7	$$⊢\left(\phi \wedge k\in Z\right)\to \left|F\left(k\right)\right|\le A^k$$
8		eqid	$$⊢{\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}={\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}$$
9		0z	$$⊢0\in \mathbb{Z}$$
10		ifcl	$$⊢\left(0\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to if\left(M\le 0,0,M\right)\in \mathbb{Z}$$
11	9 3 10	sylancr	$$⊢\phi \to if\left(M\le 0,0,M\right)\in \mathbb{Z}$$
12	4	recnd	$$⊢\phi \to A\in ℂ$$
13	12 5	expcnv	$$⊢\phi \to \left(n\in {\mathbb{N}}_0⟼A^n\right)⇝0$$
14	1	fvexi	$$⊢Z\in \mathrm{V}$$
15	14	mptex	$$⊢\left(n\in Z⟼\left|F\left(n\right)\right|\right)\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to \left(n\in Z⟼\left|F\left(n\right)\right|\right)\in \mathrm{V}$$
17		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
18	1 17	ineq12i	$$⊢Z\cap {\mathbb{N}}_0={\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge 0}$$
19		uzin	$$⊢\left(M\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge 0}={\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}$$
20	3 9 19	sylancl	$$⊢\phi \to {\mathbb{Z}}_{\ge M}\cap {\mathbb{Z}}_{\ge 0}={\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}$$
21	18 20	syl5req	$$⊢\phi \to {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}=Z\cap {\mathbb{N}}_0$$
22	21	eleq2d	$$⊢\phi \to \left(k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\leftrightarrow k\in \left(Z\cap {\mathbb{N}}_0\right)\right)$$
23	22	biimpa	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to k\in \left(Z\cap {\mathbb{N}}_0\right)$$
24	23	elin2d	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to k\in {\mathbb{N}}_0$$
25		oveq2	$$⊢n=k\to A^n=A^k$$
26		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼A^n\right)=\left(n\in {\mathbb{N}}_0⟼A^n\right)$$
27		ovex	$$⊢A^k\in \mathrm{V}$$
28	25 26 27	fvmpt	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=A^k$$
29	24 28	syl	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)=A^k$$
30	4	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to A\in ℝ$$
31	30 24	reexpcld	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to A^k\in ℝ$$
32	29 31	eqeltrd	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)\in ℝ$$
33	23	elin1d	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to k\in Z$$
34		2fveq3	$$⊢n=k\to \left|F\left(n\right)\right|=\left|F\left(k\right)\right|$$
35		eqid	$$⊢\left(n\in Z⟼\left|F\left(n\right)\right|\right)=\left(n\in Z⟼\left|F\left(n\right)\right|\right)$$
36		fvex	$$⊢\left|F\left(k\right)\right|\in \mathrm{V}$$
37	34 35 36	fvmpt	$$⊢k\in Z\to \left(n\in Z⟼\left|F\left(n\right)\right|\right)\left(k\right)=\left|F\left(k\right)\right|$$
38	33 37	syl	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to \left(n\in Z⟼\left|F\left(n\right)\right|\right)\left(k\right)=\left|F\left(k\right)\right|$$
39	33 6	syldan	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to F\left(k\right)\in ℂ$$
40	39	abscld	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to \left|F\left(k\right)\right|\in ℝ$$
41	38 40	eqeltrd	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to \left(n\in Z⟼\left|F\left(n\right)\right|\right)\left(k\right)\in ℝ$$
42	33 7	syldan	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to \left|F\left(k\right)\right|\le A^k$$
43	42 38 29	3brtr4d	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to \left(n\in Z⟼\left|F\left(n\right)\right|\right)\left(k\right)\le \left(n\in {\mathbb{N}}_0⟼A^n\right)\left(k\right)$$
44	39	absge0d	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to 0\le \left|F\left(k\right)\right|$$
45	44 38	breqtrrd	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge if\left(M\le 0,0,M\right)}\right)\to 0\le \left(n\in Z⟼\left|F\left(n\right)\right|\right)\left(k\right)$$
46	8 11 13 16 32 41 43 45	climsqz2	$$⊢\phi \to \left(n\in Z⟼\left|F\left(n\right)\right|\right)⇝0$$
47	37	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to \left(n\in Z⟼\left|F\left(n\right)\right|\right)\left(k\right)=\left|F\left(k\right)\right|$$
48	1 3 2 16 6 47	climabs0	$$⊢\phi \to \left(F⇝0\leftrightarrow \left(n\in Z⟼\left|F\left(n\right)\right|\right)⇝0\right)$$
49	46 48	mpbird	$$⊢\phi \to F⇝0$$