dvradcnv

Description: The radius of convergence of the (formal) derivative H of the power series G is at least as large as the radius of convergence of G . (In fact they are equal, but we don't have as much use for the negative side of this claim.) (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Hypotheses	dvradcnv.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
	dvradcnv.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
	dvradcnv.h	$⊢ H = (n \in ℕ_{0} ⟼ (n + 1) A (n + 1) X^{n})$
	dvradcnv.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	dvradcnv.x	$⊢ φ \to X \in ℂ$
	dvradcnv.l	$⊢ φ \to \|X\| < R$
Assertion	dvradcnv	$⊢ φ \to seq 0 (+ H) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		dvradcnv.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		dvradcnv.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
3		dvradcnv.h	$⊢ H = (n \in ℕ_{0} ⟼ (n + 1) A (n + 1) X^{n})$
4		dvradcnv.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
5		dvradcnv.x	$⊢ φ \to X \in ℂ$
6		dvradcnv.l	$⊢ φ \to \|X\| < R$
7		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
8		1nn0	$⊢ 1 \in ℕ_{0}$
9	8	a1i	$⊢ φ \to 1 \in ℕ_{0}$
10		ax-1cn	$⊢ 1 \in ℂ$
11		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
12	11	adantl	$⊢ (φ \land k \in ℕ_{0}) \to k \in ℂ$
13		nn0ex	$⊢ ℕ_{0} \in V$
14	13	mptex	$⊢ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) \in V$
15	14	shftval4	$⊢ (1 \in ℂ \land k \in ℂ) \to ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1) (k) = (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (1 + k)$
16	10 12 15	sylancr	$⊢ (φ \land k \in ℕ_{0}) \to ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1) (k) = (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (1 + k)$
17		addcom	$⊢ (1 \in ℂ \land k \in ℂ) \to 1 + k = k + 1$
18	10 12 17	sylancr	$⊢ (φ \land k \in ℕ_{0}) \to 1 + k = k + 1$
19	18	fveq2d	$⊢ (φ \land k \in ℕ_{0}) \to (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (1 + k) = (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (k + 1)$
20		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
21	20	adantl	$⊢ (φ \land k \in ℕ_{0}) \to k + 1 \in ℕ_{0}$
22		id	$⊢ i = k + 1 \to i = k + 1$
23		2fveq3	$⊢ i = k + 1 \to \|G (X) (i)\| = \|G (X) (k + 1)\|$
24	22 23	oveq12d	$⊢ i = k + 1 \to i \|G (X) (i)\| = (k + 1) \|G (X) (k + 1)\|$
25		eqid	$⊢ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) = (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)$
26		ovex	$⊢ (k + 1) \|G (X) (k + 1)\| \in V$
27	24 25 26	fvmpt	$⊢ k + 1 \in ℕ_{0} \to (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (k + 1) = (k + 1) \|G (X) (k + 1)\|$
28	21 27	syl	$⊢ (φ \land k \in ℕ_{0}) \to (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (k + 1) = (k + 1) \|G (X) (k + 1)\|$
29	1	pserval2	$⊢ (X \in ℂ \land k + 1 \in ℕ_{0}) \to G (X) (k + 1) = A (k + 1) X^{k + 1}$
30	5 20 29	syl2an	$⊢ (φ \land k \in ℕ_{0}) \to G (X) (k + 1) = A (k + 1) X^{k + 1}$
31	30	fveq2d	$⊢ (φ \land k \in ℕ_{0}) \to \|G (X) (k + 1)\| = \|A (k + 1) X^{k + 1}\|$
32	31	oveq2d	$⊢ (φ \land k \in ℕ_{0}) \to (k + 1) \|G (X) (k + 1)\| = (k + 1) \|A (k + 1) X^{k + 1}\|$
33	28 32	eqtrd	$⊢ (φ \land k \in ℕ_{0}) \to (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (k + 1) = (k + 1) \|A (k + 1) X^{k + 1}\|$
34	16 19 33	3eqtrd	$⊢ (φ \land k \in ℕ_{0}) \to ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1) (k) = (k + 1) \|A (k + 1) X^{k + 1}\|$
35	21	nn0red	$⊢ (φ \land k \in ℕ_{0}) \to k + 1 \in ℝ$
36		ffvelrn	$⊢ (A : ℕ_{0} ⟶ ℂ \land k + 1 \in ℕ_{0}) \to A (k + 1) \in ℂ$
37	4 20 36	syl2an	$⊢ (φ \land k \in ℕ_{0}) \to A (k + 1) \in ℂ$
38		expcl	$⊢ (X \in ℂ \land k + 1 \in ℕ_{0}) \to X^{k + 1} \in ℂ$
39	5 20 38	syl2an	$⊢ (φ \land k \in ℕ_{0}) \to X^{k + 1} \in ℂ$
40	37 39	mulcld	$⊢ (φ \land k \in ℕ_{0}) \to A (k + 1) X^{k + 1} \in ℂ$
41	40	abscld	$⊢ (φ \land k \in ℕ_{0}) \to \|A (k + 1) X^{k + 1}\| \in ℝ$
42	35 41	remulcld	$⊢ (φ \land k \in ℕ_{0}) \to (k + 1) \|A (k + 1) X^{k + 1}\| \in ℝ$
43	34 42	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1) (k) \in ℝ$
44		oveq1	$⊢ n = k \to n + 1 = k + 1$
45	44	fveq2d	$⊢ n = k \to A (n + 1) = A (k + 1)$
46	44 45	oveq12d	$⊢ n = k \to (n + 1) A (n + 1) = (k + 1) A (k + 1)$
47		oveq2	$⊢ n = k \to X^{n} = X^{k}$
48	46 47	oveq12d	$⊢ n = k \to (n + 1) A (n + 1) X^{n} = (k + 1) A (k + 1) X^{k}$
49		ovex	$⊢ (k + 1) A (k + 1) X^{k} \in V$
50	48 3 49	fvmpt	$⊢ k \in ℕ_{0} \to H (k) = (k + 1) A (k + 1) X^{k}$
51	50	adantl	$⊢ (φ \land k \in ℕ_{0}) \to H (k) = (k + 1) A (k + 1) X^{k}$
52	21	nn0cnd	$⊢ (φ \land k \in ℕ_{0}) \to k + 1 \in ℂ$
53	52 37	mulcld	$⊢ (φ \land k \in ℕ_{0}) \to (k + 1) A (k + 1) \in ℂ$
54		expcl	$⊢ (X \in ℂ \land k \in ℕ_{0}) \to X^{k} \in ℂ$
55	5 54	sylan	$⊢ (φ \land k \in ℕ_{0}) \to X^{k} \in ℂ$
56	53 55	mulcld	$⊢ (φ \land k \in ℕ_{0}) \to (k + 1) A (k + 1) X^{k} \in ℂ$
57	51 56	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to H (k) \in ℂ$
58		id	$⊢ i = k \to i = k$
59		2fveq3	$⊢ i = k \to \|G (X) (i)\| = \|G (X) (k)\|$
60	58 59	oveq12d	$⊢ i = k \to i \|G (X) (i)\| = k \|G (X) (k)\|$
61	60	cbvmptv	$⊢ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) = (k \in ℕ_{0} ⟼ k \|G (X) (k)\|)$
62	1 4 2 5 6 61	radcnvlt1	$⊢ φ \to (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)) \in dom ⇝ \land seq 0 (+ (abs \circ G (X))) \in dom ⇝)$
63	62	simpld	$⊢ φ \to seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)) \in dom ⇝$
64		climdm	$⊢ seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)) \in dom ⇝ \leftrightarrow seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)) ⇝ ⇝ (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)))$
65	63 64	sylib	$⊢ φ \to seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)) ⇝ ⇝ (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)))$
66		0z	$⊢ 0 \in ℤ$
67		neg1z	$⊢ - 1 \in ℤ$
68	14	isershft	$⊢ (0 \in ℤ \land - 1 \in ℤ) \to (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)) ⇝ ⇝ (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|))) \leftrightarrow seq (0 + -1) (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) ⇝ ⇝ (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|))))$
69	66 67 68	mp2an	$⊢ seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)) ⇝ ⇝ (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|))) \leftrightarrow seq (0 + -1) (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) ⇝ ⇝ (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)))$
70	65 69	sylib	$⊢ φ \to seq (0 + -1) (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) ⇝ ⇝ (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|)))$
71		seqex	$⊢ seq (0 + -1) (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) \in V$
72		fvex	$⊢ ⇝ (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|))) \in V$
73	71 72	breldm	$⊢ seq (0 + -1) (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) ⇝ ⇝ (seq 0 (+ (i \in ℕ_{0} ⟼ i \|G (X) (i)\|))) \to seq (0 + -1) (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) \in dom ⇝$
74	70 73	syl	$⊢ φ \to seq (0 + -1) (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) \in dom ⇝$
75		eqid	$⊢ ℤ_{\geq (0 + -1)} = ℤ_{\geq (0 + -1)}$
76		neg1cn	$⊢ - 1 \in ℂ$
77	76	addid2i	$⊢ 0 + -1 = - 1$
78		0le1	$⊢ 0 \leq 1$
79		1re	$⊢ 1 \in ℝ$
80		le0neg2	$⊢ 1 \in ℝ \to (0 \leq 1 \leftrightarrow - 1 \leq 0)$
81	79 80	ax-mp	$⊢ 0 \leq 1 \leftrightarrow - 1 \leq 0$
82	78 81	mpbi	$⊢ - 1 \leq 0$
83	77 82	eqbrtri	$⊢ 0 + -1 \leq 0$
84	77 67	eqeltri	$⊢ 0 + -1 \in ℤ$
85	84	eluz1i	$⊢ 0 \in ℤ_{\geq (0 + -1)} \leftrightarrow (0 \in ℤ \land 0 + -1 \leq 0)$
86	66 83 85	mpbir2an	$⊢ 0 \in ℤ_{\geq (0 + -1)}$
87	86	a1i	$⊢ φ \to 0 \in ℤ_{\geq (0 + -1)}$
88		eluzelcn	$⊢ k \in ℤ_{\geq (0 + -1)} \to k \in ℂ$
89	88	adantl	$⊢ (φ \land k \in ℤ_{\geq (0 + -1)}) \to k \in ℂ$
90	10 89 15	sylancr	$⊢ (φ \land k \in ℤ_{\geq (0 + -1)}) \to ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1) (k) = (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (1 + k)$
91		nn0re	$⊢ i \in ℕ_{0} \to i \in ℝ$
92	91	adantl	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℝ$
93	1 4 5	psergf	$⊢ φ \to G (X) : ℕ_{0} ⟶ ℂ$
94	93	ffvelrnda	$⊢ (φ \land i \in ℕ_{0}) \to G (X) (i) \in ℂ$
95	94	abscld	$⊢ (φ \land i \in ℕ_{0}) \to \|G (X) (i)\| \in ℝ$
96	92 95	remulcld	$⊢ (φ \land i \in ℕ_{0}) \to i \|G (X) (i)\| \in ℝ$
97	96	recnd	$⊢ (φ \land i \in ℕ_{0}) \to i \|G (X) (i)\| \in ℂ$
98	97	fmpttd	$⊢ φ \to (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) : ℕ_{0} ⟶ ℂ$
99	10 88 17	sylancr	$⊢ k \in ℤ_{\geq (0 + -1)} \to 1 + k = k + 1$
100		eluzp1p1	$⊢ k \in ℤ_{\geq (0 + -1)} \to k + 1 \in ℤ_{\geq (0 + -1 + 1)}$
101	77	oveq1i	$⊢ 0 + -1 + 1 = - 1 + 1$
102		1pneg1e0	$⊢ 1 + -1 = 0$
103	10 76 102	addcomli	$⊢ - 1 + 1 = 0$
104	101 103	eqtri	$⊢ 0 + -1 + 1 = 0$
105	104	fveq2i	$⊢ ℤ_{\geq (0 + -1 + 1)} = ℤ_{\geq 0}$
106	7 105	eqtr4i	$⊢ ℕ_{0} = ℤ_{\geq (0 + -1 + 1)}$
107	100 106	eleqtrrdi	$⊢ k \in ℤ_{\geq (0 + -1)} \to k + 1 \in ℕ_{0}$
108	99 107	eqeltrd	$⊢ k \in ℤ_{\geq (0 + -1)} \to 1 + k \in ℕ_{0}$
109		ffvelrn	$⊢ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) : ℕ_{0} ⟶ ℂ \land 1 + k \in ℕ_{0}) \to (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (1 + k) \in ℂ$
110	98 108 109	syl2an	$⊢ (φ \land k \in ℤ_{\geq (0 + -1)}) \to (i \in ℕ_{0} ⟼ i \|G (X) (i)\|) (1 + k) \in ℂ$
111	90 110	eqeltrd	$⊢ (φ \land k \in ℤ_{\geq (0 + -1)}) \to ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1) (k) \in ℂ$
112	75 87 111	iserex	$⊢ φ \to (seq (0 + -1) (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) \in dom ⇝ \leftrightarrow seq 0 (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) \in dom ⇝)$
113	74 112	mpbid	$⊢ φ \to seq 0 (+ ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1)) \in dom ⇝$
114		1red	$⊢ (φ \land X = 0) \to 1 \in ℝ$
115		neqne	$⊢ \neg X = 0 \to X \neq 0$
116		absrpcl	$⊢ (X \in ℂ \land X \neq 0) \to \|X\| \in ℝ^{+}$
117	5 115 116	syl2an	$⊢ (φ \land \neg X = 0) \to \|X\| \in ℝ^{+}$
118	117	rprecred	$⊢ (φ \land \neg X = 0) \to \frac{1}{\|X\|} \in ℝ$
119	114 118	ifclda	$⊢ φ \to if (X = 0, 1, \frac{1}{\|X\|}) \in ℝ$
120		oveq1	$⊢ 1 = if (X = 0, 1, \frac{1}{\|X\|}) \to 1 (k + 1) \|A (k + 1) X^{k + 1}\| = if (X = 0, 1, \frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|$
121	120	breq2d	$⊢ 1 = if (X = 0, 1, \frac{1}{\|X\|}) \to (\|(k + 1) A (k + 1) X^{k}\| \leq 1 (k + 1) \|A (k + 1) X^{k + 1}\| \leftrightarrow \|(k + 1) A (k + 1) X^{k}\| \leq if (X = 0, 1, \frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|)$
122		oveq1	$⊢ \frac{1}{\|X\|} = if (X = 0, 1, \frac{1}{\|X\|}) \to (\frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\| = if (X = 0, 1, \frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|$
123	122	breq2d	$⊢ \frac{1}{\|X\|} = if (X = 0, 1, \frac{1}{\|X\|}) \to (\|(k + 1) A (k + 1) X^{k}\| \leq (\frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\| \leftrightarrow \|(k + 1) A (k + 1) X^{k}\| \leq if (X = 0, 1, \frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|)$
124		elnnuz	$⊢ k \in ℕ \leftrightarrow k \in ℤ_{\geq 1}$
125		nnnn0	$⊢ k \in ℕ \to k \in ℕ_{0}$
126	124 125	sylbir	$⊢ k \in ℤ_{\geq 1} \to k \in ℕ_{0}$
127	21	nn0ge0d	$⊢ (φ \land k \in ℕ_{0}) \to 0 \leq k + 1$
128	40	absge0d	$⊢ (φ \land k \in ℕ_{0}) \to 0 \leq \|A (k + 1) X^{k + 1}\|$
129	35 41 127 128	mulge0d	$⊢ (φ \land k \in ℕ_{0}) \to 0 \leq (k + 1) \|A (k + 1) X^{k + 1}\|$
130	126 129	sylan2	$⊢ (φ \land k \in ℤ_{\geq 1}) \to 0 \leq (k + 1) \|A (k + 1) X^{k + 1}\|$
131	130	adantr	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land X = 0) \to 0 \leq (k + 1) \|A (k + 1) X^{k + 1}\|$
132		oveq1	$⊢ X = 0 \to X^{k} = 0^{k}$
133		simpr	$⊢ (φ \land k \in ℤ_{\geq 1}) \to k \in ℤ_{\geq 1}$
134	133 124	sylibr	$⊢ (φ \land k \in ℤ_{\geq 1}) \to k \in ℕ$
135	134	0expd	$⊢ (φ \land k \in ℤ_{\geq 1}) \to 0^{k} = 0$
136	132 135	sylan9eqr	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land X = 0) \to X^{k} = 0$
137	136	oveq2d	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land X = 0) \to (k + 1) A (k + 1) X^{k} = (k + 1) A (k + 1) \cdot 0$
138	53	mul01d	$⊢ (φ \land k \in ℕ_{0}) \to (k + 1) A (k + 1) \cdot 0 = 0$
139	126 138	sylan2	$⊢ (φ \land k \in ℤ_{\geq 1}) \to (k + 1) A (k + 1) \cdot 0 = 0$
140	139	adantr	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land X = 0) \to (k + 1) A (k + 1) \cdot 0 = 0$
141	137 140	eqtrd	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land X = 0) \to (k + 1) A (k + 1) X^{k} = 0$
142	141	abs00bd	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land X = 0) \to \|(k + 1) A (k + 1) X^{k}\| = 0$
143	42	recnd	$⊢ (φ \land k \in ℕ_{0}) \to (k + 1) \|A (k + 1) X^{k + 1}\| \in ℂ$
144	143	mulid2d	$⊢ (φ \land k \in ℕ_{0}) \to 1 (k + 1) \|A (k + 1) X^{k + 1}\| = (k + 1) \|A (k + 1) X^{k + 1}\|$
145	126 144	sylan2	$⊢ (φ \land k \in ℤ_{\geq 1}) \to 1 (k + 1) \|A (k + 1) X^{k + 1}\| = (k + 1) \|A (k + 1) X^{k + 1}\|$
146	145	adantr	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land X = 0) \to 1 (k + 1) \|A (k + 1) X^{k + 1}\| = (k + 1) \|A (k + 1) X^{k + 1}\|$
147	131 142 146	3brtr4d	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land X = 0) \to \|(k + 1) A (k + 1) X^{k}\| \leq 1 (k + 1) \|A (k + 1) X^{k + 1}\|$
148		df-ne	$⊢ X \neq 0 \leftrightarrow \neg X = 0$
149	56	abscld	$⊢ (φ \land k \in ℕ_{0}) \to \|(k + 1) A (k + 1) X^{k}\| \in ℝ$
150	52 37 55	mulassd	$⊢ (φ \land k \in ℕ_{0}) \to (k + 1) A (k + 1) X^{k} = (k + 1) A (k + 1) X^{k}$
151	150	fveq2d	$⊢ (φ \land k \in ℕ_{0}) \to \|(k + 1) A (k + 1) X^{k}\| = \|(k + 1) A (k + 1) X^{k}\|$
152	37 55	mulcld	$⊢ (φ \land k \in ℕ_{0}) \to A (k + 1) X^{k} \in ℂ$
153	52 152	absmuld	$⊢ (φ \land k \in ℕ_{0}) \to \|(k + 1) A (k + 1) X^{k}\| = \|k + 1\| \|A (k + 1) X^{k}\|$
154	35 127	absidd	$⊢ (φ \land k \in ℕ_{0}) \to \|k + 1\| = k + 1$
155	154	oveq1d	$⊢ (φ \land k \in ℕ_{0}) \to \|k + 1\| \|A (k + 1) X^{k}\| = (k + 1) \|A (k + 1) X^{k}\|$
156	151 153 155	3eqtrd	$⊢ (φ \land k \in ℕ_{0}) \to \|(k + 1) A (k + 1) X^{k}\| = (k + 1) \|A (k + 1) X^{k}\|$
157	149 156	eqled	$⊢ (φ \land k \in ℕ_{0}) \to \|(k + 1) A (k + 1) X^{k}\| \leq (k + 1) \|A (k + 1) X^{k}\|$
158	157	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|(k + 1) A (k + 1) X^{k}\| \leq (k + 1) \|A (k + 1) X^{k}\|$
159	5	adantr	$⊢ (φ \land k \in ℕ_{0}) \to X \in ℂ$
160	116	rpreccld	$⊢ (X \in ℂ \land X \neq 0) \to \frac{1}{\|X\|} \in ℝ^{+}$
161	159 160	sylan	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \frac{1}{\|X\|} \in ℝ^{+}$
162	161	rpcnd	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \frac{1}{\|X\|} \in ℂ$
163	52	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to k + 1 \in ℂ$
164	41	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|A (k + 1) X^{k + 1}\| \in ℝ$
165	164	recnd	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|A (k + 1) X^{k + 1}\| \in ℂ$
166	162 163 165	mul12d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to (\frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\| = (k + 1) (\frac{1}{\|X\|}) \|A (k + 1) X^{k + 1}\|$
167	40	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to A (k + 1) X^{k + 1} \in ℂ$
168	5	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to X \in ℂ$
169		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to X \neq 0$
170	167 168 169	absdivd	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|\frac{A (k + 1) X^{k + 1}}{X}\| = \frac{\|A (k + 1) X^{k + 1}\|}{\|X\|}$
171	37	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to A (k + 1) \in ℂ$
172	39	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to X^{k + 1} \in ℂ$
173	171 172 168 169	divassd	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \frac{A (k + 1) X^{k + 1}}{X} = A (k + 1) (\frac{X^{k + 1}}{X})$
174	12	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to k \in ℂ$
175		pncan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k + 1 - 1 = k$
176	174 10 175	sylancl	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to k + 1 - 1 = k$
177	176	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to X^{k + 1 - 1} = X^{k}$
178	21	nn0zd	$⊢ (φ \land k \in ℕ_{0}) \to k + 1 \in ℤ$
179	178	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to k + 1 \in ℤ$
180	168 169 179	expm1d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to X^{k + 1 - 1} = \frac{X^{k + 1}}{X}$
181	177 180	eqtr3d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to X^{k} = \frac{X^{k + 1}}{X}$
182	181	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to A (k + 1) X^{k} = A (k + 1) (\frac{X^{k + 1}}{X})$
183	173 182	eqtr4d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \frac{A (k + 1) X^{k + 1}}{X} = A (k + 1) X^{k}$
184	183	fveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|\frac{A (k + 1) X^{k + 1}}{X}\| = \|A (k + 1) X^{k}\|$
185	5	abscld	$⊢ φ \to \|X\| \in ℝ$
186	185	ad2antrr	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|X\| \in ℝ$
187	186	recnd	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|X\| \in ℂ$
188	159 116	sylan	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|X\| \in ℝ^{+}$
189	188	rpne0d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|X\| \neq 0$
190	165 187 189	divrec2d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \frac{\|A (k + 1) X^{k + 1}\|}{\|X\|} = (\frac{1}{\|X\|}) \|A (k + 1) X^{k + 1}\|$
191	170 184 190	3eqtr3rd	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to (\frac{1}{\|X\|}) \|A (k + 1) X^{k + 1}\| = \|A (k + 1) X^{k}\|$
192	191	oveq2d	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to (k + 1) (\frac{1}{\|X\|}) \|A (k + 1) X^{k + 1}\| = (k + 1) \|A (k + 1) X^{k}\|$
193	166 192	eqtrd	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to (\frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\| = (k + 1) \|A (k + 1) X^{k}\|$
194	158 193	breqtrrd	$⊢ ((φ \land k \in ℕ_{0}) \land X \neq 0) \to \|(k + 1) A (k + 1) X^{k}\| \leq (\frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|$
195	126 194	sylanl2	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land X \neq 0) \to \|(k + 1) A (k + 1) X^{k}\| \leq (\frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|$
196	148 195	sylan2br	$⊢ ((φ \land k \in ℤ_{\geq 1}) \land \neg X = 0) \to \|(k + 1) A (k + 1) X^{k}\| \leq (\frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|$
197	121 123 147 196	ifbothda	$⊢ (φ \land k \in ℤ_{\geq 1}) \to \|(k + 1) A (k + 1) X^{k}\| \leq if (X = 0, 1, \frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|$
198	51	fveq2d	$⊢ (φ \land k \in ℕ_{0}) \to \|H (k)\| = \|(k + 1) A (k + 1) X^{k}\|$
199	126 198	sylan2	$⊢ (φ \land k \in ℤ_{\geq 1}) \to \|H (k)\| = \|(k + 1) A (k + 1) X^{k}\|$
200	34	oveq2d	$⊢ (φ \land k \in ℕ_{0}) \to if (X = 0, 1, \frac{1}{\|X\|}) ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1) (k) = if (X = 0, 1, \frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|$
201	126 200	sylan2	$⊢ (φ \land k \in ℤ_{\geq 1}) \to if (X = 0, 1, \frac{1}{\|X\|}) ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1) (k) = if (X = 0, 1, \frac{1}{\|X\|}) (k + 1) \|A (k + 1) X^{k + 1}\|$
202	197 199 201	3brtr4d	$⊢ (φ \land k \in ℤ_{\geq 1}) \to \|H (k)\| \leq if (X = 0, 1, \frac{1}{\|X\|}) ((i \in ℕ_{0} ⟼ i \|G (X) (i)\|) shift -1) (k)$
203	7 9 43 57 113 119 202	cvgcmpce	$⊢ φ \to seq 0 (+ H) \in dom ⇝$

Metamath Proof Explorer

Theorem dvradcnv

Proof