expcnv

Description: A sequence of powers of a complex number A with absolute value less than 1 converges to zero. (Contributed by NM, 8-May-2006) (Proof shortened by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Hypotheses	expcnv.1	$⊢ φ \to A \in ℂ$
	expcnv.2	$⊢ φ \to \|A\| < 1$
Assertion	expcnv	$⊢ φ \to (n \in ℕ_{0} ⟼ A^{n}) ⇝ 0$

Proof

Step	Hyp	Ref	Expression
1		expcnv.1	$⊢ φ \to A \in ℂ$
2		expcnv.2	$⊢ φ \to \|A\| < 1$
3		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
4		1zzd	$⊢ (φ \land A = 0) \to 1 \in ℤ$
5		nn0ex	$⊢ ℕ_{0} \in V$
6	5	mptex	$⊢ (n \in ℕ_{0} ⟼ A^{n}) \in V$
7	6	a1i	$⊢ (φ \land A = 0) \to (n \in ℕ_{0} ⟼ A^{n}) \in V$
8		0cnd	$⊢ (φ \land A = 0) \to 0 \in ℂ$
9		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
10		oveq2	$⊢ n = k \to A^{n} = A^{k}$
11		eqid	$⊢ (n \in ℕ_{0} ⟼ A^{n}) = (n \in ℕ_{0} ⟼ A^{n})$
12		ovex	$⊢ A^{k} \in V$
13	10 11 12	fvmpt	$⊢ k \in ℕ_{0} \to (n \in ℕ_{0} ⟼ A^{n}) (k) = A^{k}$
14	9 13	syl	$⊢ k \in ℕ \to (n \in ℕ_{0} ⟼ A^{n}) (k) = A^{k}$
15		simpr	$⊢ (φ \land A = 0) \to A = 0$
16	15	oveq1d	$⊢ (φ \land A = 0) \to A^{k} = 0^{k}$
17	14 16	sylan9eqr	$⊢ ((φ \land A = 0) \land k \in ℕ) \to (n \in ℕ_{0} ⟼ A^{n}) (k) = 0^{k}$
18		0exp	$⊢ k \in ℕ \to 0^{k} = 0$
19	18	adantl	$⊢ ((φ \land A = 0) \land k \in ℕ) \to 0^{k} = 0$
20	17 19	eqtrd	$⊢ ((φ \land A = 0) \land k \in ℕ) \to (n \in ℕ_{0} ⟼ A^{n}) (k) = 0$
21	3 4 7 8 20	climconst	$⊢ (φ \land A = 0) \to (n \in ℕ_{0} ⟼ A^{n}) ⇝ 0$
22		1zzd	$⊢ (φ \land A \neq 0) \to 1 \in ℤ$
23	2	adantr	$⊢ (φ \land A \neq 0) \to \|A\| < 1$
24		absrpcl	$⊢ (A \in ℂ \land A \neq 0) \to \|A\| \in ℝ^{+}$
25	1 24	sylan	$⊢ (φ \land A \neq 0) \to \|A\| \in ℝ^{+}$
26	25	reclt1d	$⊢ (φ \land A \neq 0) \to (\|A\| < 1 \leftrightarrow 1 < \frac{1}{\|A\|})$
27	23 26	mpbid	$⊢ (φ \land A \neq 0) \to 1 < \frac{1}{\|A\|}$
28		1re	$⊢ 1 \in ℝ$
29	25	rpreccld	$⊢ (φ \land A \neq 0) \to \frac{1}{\|A\|} \in ℝ^{+}$
30	29	rpred	$⊢ (φ \land A \neq 0) \to \frac{1}{\|A\|} \in ℝ$
31		difrp	$⊢ (1 \in ℝ \land \frac{1}{\|A\|} \in ℝ) \to (1 < \frac{1}{\|A\|} \leftrightarrow (\frac{1}{\|A\|}) - 1 \in ℝ^{+})$
32	28 30 31	sylancr	$⊢ (φ \land A \neq 0) \to (1 < \frac{1}{\|A\|} \leftrightarrow (\frac{1}{\|A\|}) - 1 \in ℝ^{+})$
33	27 32	mpbid	$⊢ (φ \land A \neq 0) \to (\frac{1}{\|A\|}) - 1 \in ℝ^{+}$
34	33	rpreccld	$⊢ (φ \land A \neq 0) \to \frac{1}{(\frac{1}{\|A\|}) - 1} \in ℝ^{+}$
35	34	rpcnd	$⊢ (φ \land A \neq 0) \to \frac{1}{(\frac{1}{\|A\|}) - 1} \in ℂ$
36		divcnv	$⊢ \frac{1}{(\frac{1}{\|A\|}) - 1} \in ℂ \to (n \in ℕ ⟼ \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{n}) ⇝ 0$
37	35 36	syl	$⊢ (φ \land A \neq 0) \to (n \in ℕ ⟼ \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{n}) ⇝ 0$
38		nnex	$⊢ ℕ \in V$
39	38	mptex	$⊢ (n \in ℕ ⟼ {\|A\|}^{n}) \in V$
40	39	a1i	$⊢ (φ \land A \neq 0) \to (n \in ℕ ⟼ {\|A\|}^{n}) \in V$
41		oveq2	$⊢ n = k \to \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{n} = \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{k}$
42		eqid	$⊢ (n \in ℕ ⟼ \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{n}) = (n \in ℕ ⟼ \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{n})$
43		ovex	$⊢ \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{k} \in V$
44	41 42 43	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{n}) (k) = \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{k}$
45	44	adantl	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to (n \in ℕ ⟼ \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{n}) (k) = \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{k}$
46	34	rpred	$⊢ (φ \land A \neq 0) \to \frac{1}{(\frac{1}{\|A\|}) - 1} \in ℝ$
47		nndivre	$⊢ (\frac{1}{(\frac{1}{\|A\|}) - 1} \in ℝ \land k \in ℕ) \to \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{k} \in ℝ$
48	46 47	sylan	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{k} \in ℝ$
49	45 48	eqeltrd	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to (n \in ℕ ⟼ \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{n}) (k) \in ℝ$
50		oveq2	$⊢ n = k \to {\|A\|}^{n} = {\|A\|}^{k}$
51		eqid	$⊢ (n \in ℕ ⟼ {\|A\|}^{n}) = (n \in ℕ ⟼ {\|A\|}^{n})$
52		ovex	$⊢ {\|A\|}^{k} \in V$
53	50 51 52	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ {\|A\|}^{n}) (k) = {\|A\|}^{k}$
54	53	adantl	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to (n \in ℕ ⟼ {\|A\|}^{n}) (k) = {\|A\|}^{k}$
55		nnz	$⊢ k \in ℕ \to k \in ℤ$
56		rpexpcl	$⊢ (\|A\| \in ℝ^{+} \land k \in ℤ) \to {\|A\|}^{k} \in ℝ^{+}$
57	25 55 56	syl2an	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to {\|A\|}^{k} \in ℝ^{+}$
58	54 57	eqeltrd	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to (n \in ℕ ⟼ {\|A\|}^{n}) (k) \in ℝ^{+}$
59	58	rpred	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to (n \in ℕ ⟼ {\|A\|}^{n}) (k) \in ℝ$
60		nnrp	$⊢ k \in ℕ \to k \in ℝ^{+}$
61		rpmulcl	$⊢ ((\frac{1}{\|A\|}) - 1 \in ℝ^{+} \land k \in ℝ^{+}) \to ((\frac{1}{\|A\|}) - 1) k \in ℝ^{+}$
62	33 60 61	syl2an	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to ((\frac{1}{\|A\|}) - 1) k \in ℝ^{+}$
63	62	rpred	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to ((\frac{1}{\|A\|}) - 1) k \in ℝ$
64		peano2re	$⊢ ((\frac{1}{\|A\|}) - 1) k \in ℝ \to ((\frac{1}{\|A\|}) - 1) k + 1 \in ℝ$
65	63 64	syl	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to ((\frac{1}{\|A\|}) - 1) k + 1 \in ℝ$
66		rpexpcl	$⊢ (\frac{1}{\|A\|} \in ℝ^{+} \land k \in ℤ) \to {(\frac{1}{\|A\|})}^{k} \in ℝ^{+}$
67	29 55 66	syl2an	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to {(\frac{1}{\|A\|})}^{k} \in ℝ^{+}$
68	67	rpred	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to {(\frac{1}{\|A\|})}^{k} \in ℝ$
69	63	lep1d	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to ((\frac{1}{\|A\|}) - 1) k \leq ((\frac{1}{\|A\|}) - 1) k + 1$
70	30	adantr	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to \frac{1}{\|A\|} \in ℝ$
71	9	adantl	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to k \in ℕ_{0}$
72	29	rpge0d	$⊢ (φ \land A \neq 0) \to 0 \leq \frac{1}{\|A\|}$
73	72	adantr	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to 0 \leq \frac{1}{\|A\|}$
74		bernneq2	$⊢ (\frac{1}{\|A\|} \in ℝ \land k \in ℕ_{0} \land 0 \leq \frac{1}{\|A\|}) \to ((\frac{1}{\|A\|}) - 1) k + 1 \leq {(\frac{1}{\|A\|})}^{k}$
75	70 71 73 74	syl3anc	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to ((\frac{1}{\|A\|}) - 1) k + 1 \leq {(\frac{1}{\|A\|})}^{k}$
76	63 65 68 69 75	letrd	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to ((\frac{1}{\|A\|}) - 1) k \leq {(\frac{1}{\|A\|})}^{k}$
77	25	rpcnne0d	$⊢ (φ \land A \neq 0) \to (\|A\| \in ℂ \land \|A\| \neq 0)$
78		exprec	$⊢ (\|A\| \in ℂ \land \|A\| \neq 0 \land k \in ℤ) \to {(\frac{1}{\|A\|})}^{k} = \frac{1}{{\|A\|}^{k}}$
79	78	3expa	$⊢ ((\|A\| \in ℂ \land \|A\| \neq 0) \land k \in ℤ) \to {(\frac{1}{\|A\|})}^{k} = \frac{1}{{\|A\|}^{k}}$
80	77 55 79	syl2an	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to {(\frac{1}{\|A\|})}^{k} = \frac{1}{{\|A\|}^{k}}$
81	76 80	breqtrd	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to ((\frac{1}{\|A\|}) - 1) k \leq \frac{1}{{\|A\|}^{k}}$
82	62 57 81	lerec2d	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to {\|A\|}^{k} \leq \frac{1}{((\frac{1}{\|A\|}) - 1) k}$
83	33	rpcnne0d	$⊢ (φ \land A \neq 0) \to ((\frac{1}{\|A\|}) - 1 \in ℂ \land (\frac{1}{\|A\|}) - 1 \neq 0)$
84		nncn	$⊢ k \in ℕ \to k \in ℂ$
85		nnne0	$⊢ k \in ℕ \to k \neq 0$
86	84 85	jca	$⊢ k \in ℕ \to (k \in ℂ \land k \neq 0)$
87		recdiv2	$⊢ (((\frac{1}{\|A\|}) - 1 \in ℂ \land (\frac{1}{\|A\|}) - 1 \neq 0) \land (k \in ℂ \land k \neq 0)) \to \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{k} = \frac{1}{((\frac{1}{\|A\|}) - 1) k}$
88	83 86 87	syl2an	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{k} = \frac{1}{((\frac{1}{\|A\|}) - 1) k}$
89	82 88	breqtrrd	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to {\|A\|}^{k} \leq \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{k}$
90	89 54 45	3brtr4d	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to (n \in ℕ ⟼ {\|A\|}^{n}) (k) \leq (n \in ℕ ⟼ \frac{\frac{1}{(\frac{1}{\|A\|}) - 1}}{n}) (k)$
91	58	rpge0d	$⊢ ((φ \land A \neq 0) \land k \in ℕ) \to 0 \leq (n \in ℕ ⟼ {\|A\|}^{n}) (k)$
92	3 22 37 40 49 59 90 91	climsqz2	$⊢ (φ \land A \neq 0) \to (n \in ℕ ⟼ {\|A\|}^{n}) ⇝ 0$
93		1zzd	$⊢ φ \to 1 \in ℤ$
94	6	a1i	$⊢ φ \to (n \in ℕ_{0} ⟼ A^{n}) \in V$
95	39	a1i	$⊢ φ \to (n \in ℕ ⟼ {\|A\|}^{n}) \in V$
96	9	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℕ_{0}$
97	96 13	syl	$⊢ (φ \land k \in ℕ) \to (n \in ℕ_{0} ⟼ A^{n}) (k) = A^{k}$
98		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
99	1 9 98	syl2an	$⊢ (φ \land k \in ℕ) \to A^{k} \in ℂ$
100	97 99	eqeltrd	$⊢ (φ \land k \in ℕ) \to (n \in ℕ_{0} ⟼ A^{n}) (k) \in ℂ$
101		absexp	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \|A^{k}\| = {\|A\|}^{k}$
102	1 9 101	syl2an	$⊢ (φ \land k \in ℕ) \to \|A^{k}\| = {\|A\|}^{k}$
103	97	fveq2d	$⊢ (φ \land k \in ℕ) \to \|(n \in ℕ_{0} ⟼ A^{n}) (k)\| = \|A^{k}\|$
104	53	adantl	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ {\|A\|}^{n}) (k) = {\|A\|}^{k}$
105	102 103 104	3eqtr4rd	$⊢ (φ \land k \in ℕ) \to (n \in ℕ ⟼ {\|A\|}^{n}) (k) = \|(n \in ℕ_{0} ⟼ A^{n}) (k)\|$
106	3 93 94 95 100 105	climabs0	$⊢ φ \to ((n \in ℕ_{0} ⟼ A^{n}) ⇝ 0 \leftrightarrow (n \in ℕ ⟼ {\|A\|}^{n}) ⇝ 0)$
107	106	biimpar	$⊢ (φ \land (n \in ℕ ⟼ {\|A\|}^{n}) ⇝ 0) \to (n \in ℕ_{0} ⟼ A^{n}) ⇝ 0$
108	92 107	syldan	$⊢ (φ \land A \neq 0) \to (n \in ℕ_{0} ⟼ A^{n}) ⇝ 0$
109	21 108	pm2.61dane	$⊢ φ \to (n \in ℕ_{0} ⟼ A^{n}) ⇝ 0$

Metamath Proof Explorer

Theorem expcnv

Proof