geomulcvg

Description: The geometric series converges even if it is multiplied by k to result in the larger series k x. A ^ k . (Contributed by Mario Carneiro, 27-Mar-2015)

		Ref	Expression
	Hypothesis	geomulcvg.1	$⊢ F = (k \in ℕ_{0} ⟼ k A^{k})$
	Assertion	geomulcvg	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ F) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		geomulcvg.1	$⊢ F = (k \in ℕ_{0} ⟼ k A^{k})$
2		elnn0	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℕ \lor k = 0)$
3		simpr	$⊢ ((A \in ℂ \land \|A\| < 1) \land A = 0) \to A = 0$
4	3	oveq1d	$⊢ ((A \in ℂ \land \|A\| < 1) \land A = 0) \to A^{k} = 0^{k}$
5		0exp	$⊢ k \in ℕ \to 0^{k} = 0$
6	4 5	sylan9eq	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k \in ℕ) \to A^{k} = 0$
7	6	oveq2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k \in ℕ) \to k A^{k} = k \cdot 0$
8		nncn	$⊢ k \in ℕ \to k \in ℂ$
9	8	adantl	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k \in ℕ) \to k \in ℂ$
10	9	mul01d	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k \in ℕ) \to k \cdot 0 = 0$
11	7 10	eqtrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k \in ℕ) \to k A^{k} = 0$
12		simpr	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k = 0) \to k = 0$
13	12	oveq1d	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k = 0) \to k A^{k} = 0 \cdot A^{k}$
14		simplll	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k = 0) \to A \in ℂ$
15		0nn0	$⊢ 0 \in ℕ_{0}$
16	12 15	eqeltrdi	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k = 0) \to k \in ℕ_{0}$
17	14 16	expcld	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k = 0) \to A^{k} \in ℂ$
18	17	mul02d	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k = 0) \to 0 \cdot A^{k} = 0$
19	13 18	eqtrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k = 0) \to k A^{k} = 0$
20	11 19	jaodan	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land (k \in ℕ \lor k = 0)) \to k A^{k} = 0$
21	2 20	sylan2b	$⊢ (((A \in ℂ \land \|A\| < 1) \land A = 0) \land k \in ℕ_{0}) \to k A^{k} = 0$
22	21	mpteq2dva	$⊢ ((A \in ℂ \land \|A\| < 1) \land A = 0) \to (k \in ℕ_{0} ⟼ k A^{k}) = (k \in ℕ_{0} ⟼ 0)$
23	1 22	syl5eq	$⊢ ((A \in ℂ \land \|A\| < 1) \land A = 0) \to F = (k \in ℕ_{0} ⟼ 0)$
24		fconstmpt	$⊢ ℕ_{0} \times \{0\} = (k \in ℕ_{0} ⟼ 0)$
25		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
26	25	xpeq1i	$⊢ ℕ_{0} \times \{0\} = ℤ_{\geq 0} \times \{0\}$
27	24 26	eqtr3i	$⊢ (k \in ℕ_{0} ⟼ 0) = ℤ_{\geq 0} \times \{0\}$
28	23 27	eqtrdi	$⊢ ((A \in ℂ \land \|A\| < 1) \land A = 0) \to F = ℤ_{\geq 0} \times \{0\}$
29	28	seqeq3d	$⊢ ((A \in ℂ \land \|A\| < 1) \land A = 0) \to seq 0 (+ F) = seq 0 (+ (ℤ_{\geq 0} \times \{0\}))$
30		0z	$⊢ 0 \in ℤ$
31		serclim0	$⊢ 0 \in ℤ \to seq 0 (+ (ℤ_{\geq 0} \times \{0\})) ⇝ 0$
32	30 31	ax-mp	$⊢ seq 0 (+ (ℤ_{\geq 0} \times \{0\})) ⇝ 0$
33	29 32	eqbrtrdi	$⊢ ((A \in ℂ \land \|A\| < 1) \land A = 0) \to seq 0 (+ F) ⇝ 0$
34		seqex	$⊢ seq 0 (+ F) \in V$
35		c0ex	$⊢ 0 \in V$
36	34 35	breldm	$⊢ seq 0 (+ F) ⇝ 0 \to seq 0 (+ F) \in dom ⇝$
37	33 36	syl	$⊢ ((A \in ℂ \land \|A\| < 1) \land A = 0) \to seq 0 (+ F) \in dom ⇝$
38		1red	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to 1 \in ℝ$
39		abscl	$⊢ A \in ℂ \to \|A\| \in ℝ$
40	39	adantr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| \in ℝ$
41		peano2re	$⊢ \|A\| \in ℝ \to \|A\| + 1 \in ℝ$
42	40 41	syl	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| + 1 \in ℝ$
43	42	rehalfcld	$⊢ (A \in ℂ \land \|A\| < 1) \to \frac{\|A\| + 1}{2} \in ℝ$
44	43	adantr	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to \frac{\|A\| + 1}{2} \in ℝ$
45		absrpcl	$⊢ (A \in ℂ \land A \neq 0) \to \|A\| \in ℝ^{+}$
46	45	adantlr	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to \|A\| \in ℝ^{+}$
47	44 46	rerpdivcld	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to \frac{\frac{\|A\| + 1}{2}}{\|A\|} \in ℝ$
48	40	recnd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| \in ℂ$
49	48	mulid2d	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \|A\| = \|A\|$
50		simpr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| < 1$
51		1re	$⊢ 1 \in ℝ$
52		avglt1	$⊢ (\|A\| \in ℝ \land 1 \in ℝ) \to (\|A\| < 1 \leftrightarrow \|A\| < \frac{\|A\| + 1}{2})$
53	40 51 52	sylancl	$⊢ (A \in ℂ \land \|A\| < 1) \to (\|A\| < 1 \leftrightarrow \|A\| < \frac{\|A\| + 1}{2})$
54	50 53	mpbid	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| < \frac{\|A\| + 1}{2}$
55	49 54	eqbrtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \|A\| < \frac{\|A\| + 1}{2}$
56	55	adantr	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to 1 \|A\| < \frac{\|A\| + 1}{2}$
57	38 44 46	ltmuldivd	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to (1 \|A\| < \frac{\|A\| + 1}{2} \leftrightarrow 1 < \frac{\frac{\|A\| + 1}{2}}{\|A\|})$
58	56 57	mpbid	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to 1 < \frac{\frac{\|A\| + 1}{2}}{\|A\|}$
59		expmulnbnd	$⊢ (1 \in ℝ \land \frac{\frac{\|A\| + 1}{2}}{\|A\|} \in ℝ \land 1 < \frac{\frac{\|A\| + 1}{2}}{\|A\|}) \to \exists n \in ℕ_{0} \forall k \in ℤ_{\geq n} 1 k < {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k}$
60	38 47 58 59	syl3anc	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to \exists n \in ℕ_{0} \forall k \in ℤ_{\geq n} 1 k < {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k}$
61		eluznn0	$⊢ (n \in ℕ_{0} \land k \in ℤ_{\geq n}) \to k \in ℕ_{0}$
62		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
63	62	adantl	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to k \in ℂ$
64	63	mulid2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to 1 k = k$
65	43	recnd	$⊢ (A \in ℂ \land \|A\| < 1) \to \frac{\|A\| + 1}{2} \in ℂ$
66	65	ad2antrr	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to \frac{\|A\| + 1}{2} \in ℂ$
67	48	ad2antrr	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to \|A\| \in ℂ$
68	46	adantr	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to \|A\| \in ℝ^{+}$
69	68	rpne0d	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to \|A\| \neq 0$
70		simpr	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to k \in ℕ_{0}$
71	66 67 69 70	expdivd	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k} = \frac{{(\frac{\|A\| + 1}{2})}^{k}}{{\|A\|}^{k}}$
72	64 71	breq12d	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to (1 k < {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k} \leftrightarrow k < \frac{{(\frac{\|A\| + 1}{2})}^{k}}{{\|A\|}^{k}})$
73		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
74	73	adantl	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to k \in ℝ$
75		reexpcl	$⊢ (\frac{\|A\| + 1}{2} \in ℝ \land k \in ℕ_{0}) \to {(\frac{\|A\| + 1}{2})}^{k} \in ℝ$
76	44 75	sylan	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to {(\frac{\|A\| + 1}{2})}^{k} \in ℝ$
77	40	adantr	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to \|A\| \in ℝ$
78		reexpcl	$⊢ (\|A\| \in ℝ \land k \in ℕ_{0}) \to {\|A\|}^{k} \in ℝ$
79	77 78	sylan	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to {\|A\|}^{k} \in ℝ$
80	77	adantr	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to \|A\| \in ℝ$
81		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
82	81	adantl	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to k \in ℤ$
83	68	rpgt0d	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to 0 < \|A\|$
84		expgt0	$⊢ (\|A\| \in ℝ \land k \in ℤ \land 0 < \|A\|) \to 0 < {\|A\|}^{k}$
85	80 82 83 84	syl3anc	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to 0 < {\|A\|}^{k}$
86		ltmuldiv	$⊢ (k \in ℝ \land {(\frac{\|A\| + 1}{2})}^{k} \in ℝ \land ({\|A\|}^{k} \in ℝ \land 0 < {\|A\|}^{k})) \to (k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k} \leftrightarrow k < \frac{{(\frac{\|A\| + 1}{2})}^{k}}{{\|A\|}^{k}})$
87	74 76 79 85 86	syl112anc	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to (k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k} \leftrightarrow k < \frac{{(\frac{\|A\| + 1}{2})}^{k}}{{\|A\|}^{k}})$
88	72 87	bitr4d	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land k \in ℕ_{0}) \to (1 k < {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k} \leftrightarrow k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})$
89	61 88	sylan2	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land (n \in ℕ_{0} \land k \in ℤ_{\geq n})) \to (1 k < {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k} \leftrightarrow k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})$
90	89	anassrs	$⊢ ((((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land n \in ℕ_{0}) \land k \in ℤ_{\geq n}) \to (1 k < {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k} \leftrightarrow k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})$
91	90	ralbidva	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land n \in ℕ_{0}) \to (\forall k \in ℤ_{\geq n} 1 k < {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k} \leftrightarrow \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})$
92		simprl	$⊢ ((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \to n \in ℕ_{0}$
93		oveq2	$⊢ k = m \to {(\frac{\|A\| + 1}{2})}^{k} = {(\frac{\|A\| + 1}{2})}^{m}$
94		eqid	$⊢ (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k}) = (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k})$
95		ovex	$⊢ {(\frac{\|A\| + 1}{2})}^{m} \in V$
96	93 94 95	fvmpt	$⊢ m \in ℕ_{0} \to (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k}) (m) = {(\frac{\|A\| + 1}{2})}^{m}$
97	96	adantl	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k}) (m) = {(\frac{\|A\| + 1}{2})}^{m}$
98	43	ad2antrr	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to \frac{\|A\| + 1}{2} \in ℝ$
99		simpr	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to m \in ℕ_{0}$
100	98 99	reexpcld	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to {(\frac{\|A\| + 1}{2})}^{m} \in ℝ$
101	97 100	eqeltrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k}) (m) \in ℝ$
102		id	$⊢ k = m \to k = m$
103		oveq2	$⊢ k = m \to A^{k} = A^{m}$
104	102 103	oveq12d	$⊢ k = m \to k A^{k} = m A^{m}$
105		ovex	$⊢ m A^{m} \in V$
106	104 1 105	fvmpt	$⊢ m \in ℕ_{0} \to F (m) = m A^{m}$
107	106	adantl	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to F (m) = m A^{m}$
108		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
109	108	adantl	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to m \in ℂ$
110		expcl	$⊢ (A \in ℂ \land m \in ℕ_{0}) \to A^{m} \in ℂ$
111	110	ad4ant14	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to A^{m} \in ℂ$
112	109 111	mulcld	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to m A^{m} \in ℂ$
113	107 112	eqeltrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℕ_{0}) \to F (m) \in ℂ$
114		0red	$⊢ (A \in ℂ \land \|A\| < 1) \to 0 \in ℝ$
115		absge0	$⊢ A \in ℂ \to 0 \leq \|A\|$
116	115	adantr	$⊢ (A \in ℂ \land \|A\| < 1) \to 0 \leq \|A\|$
117	114 40 43 116 54	lelttrd	$⊢ (A \in ℂ \land \|A\| < 1) \to 0 < \frac{\|A\| + 1}{2}$
118	114 43 117	ltled	$⊢ (A \in ℂ \land \|A\| < 1) \to 0 \leq \frac{\|A\| + 1}{2}$
119	43 118	absidd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|\frac{\|A\| + 1}{2}\| = \frac{\|A\| + 1}{2}$
120		avglt2	$⊢ (\|A\| \in ℝ \land 1 \in ℝ) \to (\|A\| < 1 \leftrightarrow \frac{\|A\| + 1}{2} < 1)$
121	40 51 120	sylancl	$⊢ (A \in ℂ \land \|A\| < 1) \to (\|A\| < 1 \leftrightarrow \frac{\|A\| + 1}{2} < 1)$
122	50 121	mpbid	$⊢ (A \in ℂ \land \|A\| < 1) \to \frac{\|A\| + 1}{2} < 1$
123	119 122	eqbrtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|\frac{\|A\| + 1}{2}\| < 1$
124		oveq2	$⊢ k = n \to {(\frac{\|A\| + 1}{2})}^{k} = {(\frac{\|A\| + 1}{2})}^{n}$
125		ovex	$⊢ {(\frac{\|A\| + 1}{2})}^{n} \in V$
126	124 94 125	fvmpt	$⊢ n \in ℕ_{0} \to (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k}) (n) = {(\frac{\|A\| + 1}{2})}^{n}$
127	126	adantl	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k}) (n) = {(\frac{\|A\| + 1}{2})}^{n}$
128	65 123 127	geolim	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k})) ⇝ (\frac{1}{1 - (\frac{\|A\| + 1}{2})})$
129		seqex	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k})) \in V$
130		ovex	$⊢ \frac{1}{1 - (\frac{\|A\| + 1}{2})} \in V$
131	129 130	breldm	$⊢ seq 0 (+ (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k})) ⇝ (\frac{1}{1 - (\frac{\|A\| + 1}{2})}) \to seq 0 (+ (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k})) \in dom ⇝$
132	128 131	syl	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k})) \in dom ⇝$
133	132	adantr	$⊢ ((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \to seq 0 (+ (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k})) \in dom ⇝$
134		1red	$⊢ ((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \to 1 \in ℝ$
135		eluznn0	$⊢ (n \in ℕ_{0} \land m \in ℤ_{\geq n}) \to m \in ℕ_{0}$
136	92 135	sylan	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to m \in ℕ_{0}$
137	136	nn0red	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to m \in ℝ$
138		simplll	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to A \in ℂ$
139	138	abscld	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to \|A\| \in ℝ$
140	139 136	reexpcld	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to {\|A\|}^{m} \in ℝ$
141	137 140	remulcld	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to m {\|A\|}^{m} \in ℝ$
142	136 100	syldan	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to {(\frac{\|A\| + 1}{2})}^{m} \in ℝ$
143		simprr	$⊢ ((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \to \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k}$
144		oveq2	$⊢ k = m \to {\|A\|}^{k} = {\|A\|}^{m}$
145	102 144	oveq12d	$⊢ k = m \to k {\|A\|}^{k} = m {\|A\|}^{m}$
146	145 93	breq12d	$⊢ k = m \to (k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k} \leftrightarrow m {\|A\|}^{m} < {(\frac{\|A\| + 1}{2})}^{m})$
147	146	rspccva	$⊢ (\forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k} \land m \in ℤ_{\geq n}) \to m {\|A\|}^{m} < {(\frac{\|A\| + 1}{2})}^{m}$
148	143 147	sylan	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to m {\|A\|}^{m} < {(\frac{\|A\| + 1}{2})}^{m}$
149	141 142 148	ltled	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to m {\|A\|}^{m} \leq {(\frac{\|A\| + 1}{2})}^{m}$
150	136	nn0cnd	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to m \in ℂ$
151	138 136	expcld	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to A^{m} \in ℂ$
152	150 151	absmuld	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to \|m A^{m}\| = \|m\| \|A^{m}\|$
153	136	nn0ge0d	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to 0 \leq m$
154	137 153	absidd	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to \|m\| = m$
155	138 136	absexpd	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to \|A^{m}\| = {\|A\|}^{m}$
156	154 155	oveq12d	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to \|m\| \|A^{m}\| = m {\|A\|}^{m}$
157	152 156	eqtrd	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to \|m A^{m}\| = m {\|A\|}^{m}$
158	142	recnd	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to {(\frac{\|A\| + 1}{2})}^{m} \in ℂ$
159	158	mulid2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to 1 {(\frac{\|A\| + 1}{2})}^{m} = {(\frac{\|A\| + 1}{2})}^{m}$
160	149 157 159	3brtr4d	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to \|m A^{m}\| \leq 1 {(\frac{\|A\| + 1}{2})}^{m}$
161	136 106	syl	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to F (m) = m A^{m}$
162	161	fveq2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to \|F (m)\| = \|m A^{m}\|$
163	136 96	syl	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k}) (m) = {(\frac{\|A\| + 1}{2})}^{m}$
164	163	oveq2d	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to 1 (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k}) (m) = 1 {(\frac{\|A\| + 1}{2})}^{m}$
165	160 162 164	3brtr4d	$⊢ (((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \land m \in ℤ_{\geq n}) \to \|F (m)\| \leq 1 (k \in ℕ_{0} ⟼ {(\frac{\|A\| + 1}{2})}^{k}) (m)$
166	25 92 101 113 133 134 165	cvgcmpce	$⊢ ((A \in ℂ \land \|A\| < 1) \land (n \in ℕ_{0} \land \forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k})) \to seq 0 (+ F) \in dom ⇝$
167	166	expr	$⊢ ((A \in ℂ \land \|A\| < 1) \land n \in ℕ_{0}) \to (\forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k} \to seq 0 (+ F) \in dom ⇝)$
168	167	adantlr	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land n \in ℕ_{0}) \to (\forall k \in ℤ_{\geq n} k {\|A\|}^{k} < {(\frac{\|A\| + 1}{2})}^{k} \to seq 0 (+ F) \in dom ⇝)$
169	91 168	sylbid	$⊢ (((A \in ℂ \land \|A\| < 1) \land A \neq 0) \land n \in ℕ_{0}) \to (\forall k \in ℤ_{\geq n} 1 k < {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k} \to seq 0 (+ F) \in dom ⇝)$
170	169	rexlimdva	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to (\exists n \in ℕ_{0} \forall k \in ℤ_{\geq n} 1 k < {(\frac{\frac{\|A\| + 1}{2}}{\|A\|})}^{k} \to seq 0 (+ F) \in dom ⇝)$
171	60 170	mpd	$⊢ ((A \in ℂ \land \|A\| < 1) \land A \neq 0) \to seq 0 (+ F) \in dom ⇝$
172	37 171	pm2.61dane	$⊢ (A \in ℂ \land \|A\| < 1) \to seq 0 (+ F) \in dom ⇝$

Metamath Proof Explorer

Theorem geomulcvg

Proof