radcnvlem1

Description: Lemma for radcnvlt1 , radcnvle . If X is a point closer to zero than Y and the power series converges at Y , then it converges absolutely at X , even if the terms in the sequence are multiplied by n . (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Hypotheses	pser.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
	radcnv.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	psergf.x	$⊢ φ \to X \in ℂ$
	radcnvlem2.y	$⊢ φ \to Y \in ℂ$
	radcnvlem2.a	$⊢ φ \to \|X\| < \|Y\|$
	radcnvlem2.c	$⊢ φ \to seq 0 (+ G (Y)) \in dom ⇝$
	radcnvlem1.h	$⊢ H = (m \in ℕ_{0} ⟼ m \|G (X) (m)\|)$
Assertion	radcnvlem1	$⊢ φ \to seq 0 (+ H) \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		pser.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		radcnv.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
3		psergf.x	$⊢ φ \to X \in ℂ$
4		radcnvlem2.y	$⊢ φ \to Y \in ℂ$
5		radcnvlem2.a	$⊢ φ \to \|X\| < \|Y\|$
6		radcnvlem2.c	$⊢ φ \to seq 0 (+ G (Y)) \in dom ⇝$
7		radcnvlem1.h	$⊢ H = (m \in ℕ_{0} ⟼ m \|G (X) (m)\|)$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9		0zd	$⊢ φ \to 0 \in ℤ$
10		1rp	$⊢ 1 \in ℝ^{+}$
11	10	a1i	$⊢ φ \to 1 \in ℝ^{+}$
12	1	pserval2	$⊢ (Y \in ℂ \land k \in ℕ_{0}) \to G (Y) (k) = A (k) Y^{k}$
13	4 12	sylan	$⊢ (φ \land k \in ℕ_{0}) \to G (Y) (k) = A (k) Y^{k}$
14		fvexd	$⊢ φ \to G (Y) \in V$
15	1 2 4	psergf	$⊢ φ \to G (Y) : ℕ_{0} ⟶ ℂ$
16	15	ffvelrnda	$⊢ (φ \land k \in ℕ_{0}) \to G (Y) (k) \in ℂ$
17	8 9 14 6 16	serf0	$⊢ φ \to G (Y) ⇝ 0$
18	8 9 11 13 17	climi0	$⊢ φ \to \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1$
19		simprl	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to j \in ℕ_{0}$
20		nn0re	$⊢ i \in ℕ_{0} \to i \in ℝ$
21	20	adantl	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land i \in ℕ_{0}) \to i \in ℝ$
22	3	adantr	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to X \in ℂ$
23	22	abscld	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to \|X\| \in ℝ$
24	4	adantr	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to Y \in ℂ$
25	24	abscld	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to \|Y\| \in ℝ$
26		0red	$⊢ φ \to 0 \in ℝ$
27	3	abscld	$⊢ φ \to \|X\| \in ℝ$
28	4	abscld	$⊢ φ \to \|Y\| \in ℝ$
29	3	absge0d	$⊢ φ \to 0 \leq \|X\|$
30	26 27 28 29 5	lelttrd	$⊢ φ \to 0 < \|Y\|$
31	30	gt0ne0d	$⊢ φ \to \|Y\| \neq 0$
32	31	adantr	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to \|Y\| \neq 0$
33	23 25 32	redivcld	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to \frac{\|X\|}{\|Y\|} \in ℝ$
34		reexpcl	$⊢ (\frac{\|X\|}{\|Y\|} \in ℝ \land i \in ℕ_{0}) \to {(\frac{\|X\|}{\|Y\|})}^{i} \in ℝ$
35	33 34	sylan	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land i \in ℕ_{0}) \to {(\frac{\|X\|}{\|Y\|})}^{i} \in ℝ$
36	21 35	remulcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land i \in ℕ_{0}) \to i {(\frac{\|X\|}{\|Y\|})}^{i} \in ℝ$
37		eqid	$⊢ (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i}) = (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i})$
38	36 37	fmptd	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i}) : ℕ_{0} ⟶ ℝ$
39	38	ffvelrnda	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℕ_{0}) \to (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i}) (m) \in ℝ$
40		nn0re	$⊢ m \in ℕ_{0} \to m \in ℝ$
41	40	adantl	$⊢ (φ \land m \in ℕ_{0}) \to m \in ℝ$
42	1 2 3	psergf	$⊢ φ \to G (X) : ℕ_{0} ⟶ ℂ$
43	42	ffvelrnda	$⊢ (φ \land m \in ℕ_{0}) \to G (X) (m) \in ℂ$
44	43	abscld	$⊢ (φ \land m \in ℕ_{0}) \to \|G (X) (m)\| \in ℝ$
45	41 44	remulcld	$⊢ (φ \land m \in ℕ_{0}) \to m \|G (X) (m)\| \in ℝ$
46	45 7	fmptd	$⊢ φ \to H : ℕ_{0} ⟶ ℝ$
47	46	adantr	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to H : ℕ_{0} ⟶ ℝ$
48	47	ffvelrnda	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℕ_{0}) \to H (m) \in ℝ$
49	48	recnd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℕ_{0}) \to H (m) \in ℂ$
50	27 28 31	redivcld	$⊢ φ \to \frac{\|X\|}{\|Y\|} \in ℝ$
51	50	recnd	$⊢ φ \to \frac{\|X\|}{\|Y\|} \in ℂ$
52		divge0	$⊢ ((\|X\| \in ℝ \land 0 \leq \|X\|) \land (\|Y\| \in ℝ \land 0 < \|Y\|)) \to 0 \leq \frac{\|X\|}{\|Y\|}$
53	27 29 28 30 52	syl22anc	$⊢ φ \to 0 \leq \frac{\|X\|}{\|Y\|}$
54	50 53	absidd	$⊢ φ \to \|\frac{\|X\|}{\|Y\|}\| = \frac{\|X\|}{\|Y\|}$
55	28	recnd	$⊢ φ \to \|Y\| \in ℂ$
56	55	mulid1d	$⊢ φ \to \|Y\| \cdot 1 = \|Y\|$
57	5 56	breqtrrd	$⊢ φ \to \|X\| < \|Y\| \cdot 1$
58		1red	$⊢ φ \to 1 \in ℝ$
59		ltdivmul	$⊢ (\|X\| \in ℝ \land 1 \in ℝ \land (\|Y\| \in ℝ \land 0 < \|Y\|)) \to (\frac{\|X\|}{\|Y\|} < 1 \leftrightarrow \|X\| < \|Y\| \cdot 1)$
60	27 58 28 30 59	syl112anc	$⊢ φ \to (\frac{\|X\|}{\|Y\|} < 1 \leftrightarrow \|X\| < \|Y\| \cdot 1)$
61	57 60	mpbird	$⊢ φ \to \frac{\|X\|}{\|Y\|} < 1$
62	54 61	eqbrtrd	$⊢ φ \to \|\frac{\|X\|}{\|Y\|}\| < 1$
63	37	geomulcvg	$⊢ (\frac{\|X\|}{\|Y\|} \in ℂ \land \|\frac{\|X\|}{\|Y\|}\| < 1) \to seq 0 (+ (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i})) \in dom ⇝$
64	51 62 63	syl2anc	$⊢ φ \to seq 0 (+ (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i})) \in dom ⇝$
65	64	adantr	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to seq 0 (+ (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i})) \in dom ⇝$
66		1red	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to 1 \in ℝ$
67	42	ad2antrr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to G (X) : ℕ_{0} ⟶ ℂ$
68		eluznn0	$⊢ (j \in ℕ_{0} \land m \in ℤ_{\geq j}) \to m \in ℕ_{0}$
69	19 68	sylan	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to m \in ℕ_{0}$
70	67 69	ffvelrnd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to G (X) (m) \in ℂ$
71	70	abscld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|G (X) (m)\| \in ℝ$
72	33	adantr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \frac{\|X\|}{\|Y\|} \in ℝ$
73	72 69	reexpcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to {(\frac{\|X\|}{\|Y\|})}^{m} \in ℝ$
74	69	nn0red	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to m \in ℝ$
75	69	nn0ge0d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 0 \leq m$
76	2	ad2antrr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to A : ℕ_{0} ⟶ ℂ$
77	76 69	ffvelrnd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to A (m) \in ℂ$
78	4	ad2antrr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to Y \in ℂ$
79	78 69	expcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to Y^{m} \in ℂ$
80	77 79	mulcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to A (m) Y^{m} \in ℂ$
81	80	abscld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) Y^{m}\| \in ℝ$
82		1red	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 1 \in ℝ$
83	3	ad2antrr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to X \in ℂ$
84	83	abscld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|X\| \in ℝ$
85	84 69	reexpcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to {\|X\|}^{m} \in ℝ$
86	83	absge0d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 0 \leq \|X\|$
87	84 69 86	expge0d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 0 \leq {\|X\|}^{m}$
88		simprr	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1$
89		fveq2	$⊢ k = m \to A (k) = A (m)$
90		oveq2	$⊢ k = m \to Y^{k} = Y^{m}$
91	89 90	oveq12d	$⊢ k = m \to A (k) Y^{k} = A (m) Y^{m}$
92	91	fveq2d	$⊢ k = m \to \|A (k) Y^{k}\| = \|A (m) Y^{m}\|$
93	92	breq1d	$⊢ k = m \to (\|A (k) Y^{k}\| < 1 \leftrightarrow \|A (m) Y^{m}\| < 1)$
94	93	rspccva	$⊢ (\forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1 \land m \in ℤ_{\geq j}) \to \|A (m) Y^{m}\| < 1$
95	88 94	sylan	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) Y^{m}\| < 1$
96		1re	$⊢ 1 \in ℝ$
97		ltle	$⊢ (\|A (m) Y^{m}\| \in ℝ \land 1 \in ℝ) \to (\|A (m) Y^{m}\| < 1 \to \|A (m) Y^{m}\| \leq 1)$
98	81 96 97	sylancl	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to (\|A (m) Y^{m}\| < 1 \to \|A (m) Y^{m}\| \leq 1)$
99	95 98	mpd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) Y^{m}\| \leq 1$
100	81 82 85 87 99	lemul1ad	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) Y^{m}\| {\|X\|}^{m} \leq 1 {\|X\|}^{m}$
101	83 69	expcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to X^{m} \in ℂ$
102	77 101	mulcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to A (m) X^{m} \in ℂ$
103	102 79	absmuld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) X^{m} Y^{m}\| = \|A (m) X^{m}\| \|Y^{m}\|$
104	80 101	absmuld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) Y^{m} X^{m}\| = \|A (m) Y^{m}\| \|X^{m}\|$
105	77 79 101	mul32d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to A (m) Y^{m} X^{m} = A (m) X^{m} Y^{m}$
106	105	fveq2d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) Y^{m} X^{m}\| = \|A (m) X^{m} Y^{m}\|$
107	83 69	absexpd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|X^{m}\| = {\|X\|}^{m}$
108	107	oveq2d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) Y^{m}\| \|X^{m}\| = \|A (m) Y^{m}\| {\|X\|}^{m}$
109	104 106 108	3eqtr3d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) X^{m} Y^{m}\| = \|A (m) Y^{m}\| {\|X\|}^{m}$
110	78 69	absexpd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|Y^{m}\| = {\|Y\|}^{m}$
111	110	oveq2d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) X^{m}\| \|Y^{m}\| = \|A (m) X^{m}\| {\|Y\|}^{m}$
112	103 109 111	3eqtr3d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) Y^{m}\| {\|X\|}^{m} = \|A (m) X^{m}\| {\|Y\|}^{m}$
113	85	recnd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to {\|X\|}^{m} \in ℂ$
114	113	mulid2d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 1 {\|X\|}^{m} = {\|X\|}^{m}$
115	100 112 114	3brtr3d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) X^{m}\| {\|Y\|}^{m} \leq {\|X\|}^{m}$
116	102	abscld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) X^{m}\| \in ℝ$
117	25	adantr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|Y\| \in ℝ$
118	117 69	reexpcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to {\|Y\|}^{m} \in ℝ$
119		eluzelz	$⊢ m \in ℤ_{\geq j} \to m \in ℤ$
120	119	adantl	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to m \in ℤ$
121	30	ad2antrr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 0 < \|Y\|$
122		expgt0	$⊢ (\|Y\| \in ℝ \land m \in ℤ \land 0 < \|Y\|) \to 0 < {\|Y\|}^{m}$
123	117 120 121 122	syl3anc	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 0 < {\|Y\|}^{m}$
124		lemuldiv	$⊢ (\|A (m) X^{m}\| \in ℝ \land {\|X\|}^{m} \in ℝ \land ({\|Y\|}^{m} \in ℝ \land 0 < {\|Y\|}^{m})) \to (\|A (m) X^{m}\| {\|Y\|}^{m} \leq {\|X\|}^{m} \leftrightarrow \|A (m) X^{m}\| \leq \frac{{\|X\|}^{m}}{{\|Y\|}^{m}})$
125	116 85 118 123 124	syl112anc	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to (\|A (m) X^{m}\| {\|Y\|}^{m} \leq {\|X\|}^{m} \leftrightarrow \|A (m) X^{m}\| \leq \frac{{\|X\|}^{m}}{{\|Y\|}^{m}})$
126	115 125	mpbid	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|A (m) X^{m}\| \leq \frac{{\|X\|}^{m}}{{\|Y\|}^{m}}$
127	1	pserval2	$⊢ (X \in ℂ \land m \in ℕ_{0}) \to G (X) (m) = A (m) X^{m}$
128	83 69 127	syl2anc	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to G (X) (m) = A (m) X^{m}$
129	128	fveq2d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|G (X) (m)\| = \|A (m) X^{m}\|$
130	23	recnd	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to \|X\| \in ℂ$
131	130	adantr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|X\| \in ℂ$
132	25	recnd	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to \|Y\| \in ℂ$
133	132	adantr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|Y\| \in ℂ$
134	31	ad2antrr	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|Y\| \neq 0$
135	131 133 134 69	expdivd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to {(\frac{\|X\|}{\|Y\|})}^{m} = \frac{{\|X\|}^{m}}{{\|Y\|}^{m}}$
136	126 129 135	3brtr4d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|G (X) (m)\| \leq {(\frac{\|X\|}{\|Y\|})}^{m}$
137	71 73 74 75 136	lemul2ad	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to m \|G (X) (m)\| \leq m {(\frac{\|X\|}{\|Y\|})}^{m}$
138	74 71	remulcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to m \|G (X) (m)\| \in ℝ$
139	70	absge0d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 0 \leq \|G (X) (m)\|$
140	74 71 75 139	mulge0d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 0 \leq m \|G (X) (m)\|$
141	138 140	absidd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|m \|G (X) (m)\|\| = m \|G (X) (m)\|$
142	74 73	remulcld	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to m {(\frac{\|X\|}{\|Y\|})}^{m} \in ℝ$
143	142	recnd	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to m {(\frac{\|X\|}{\|Y\|})}^{m} \in ℂ$
144	143	mulid2d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 1 m {(\frac{\|X\|}{\|Y\|})}^{m} = m {(\frac{\|X\|}{\|Y\|})}^{m}$
145	137 141 144	3brtr4d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|m \|G (X) (m)\|\| \leq 1 m {(\frac{\|X\|}{\|Y\|})}^{m}$
146		ovex	$⊢ m \|G (X) (m)\| \in V$
147	7	fvmpt2	$⊢ (m \in ℕ_{0} \land m \|G (X) (m)\| \in V) \to H (m) = m \|G (X) (m)\|$
148	69 146 147	sylancl	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to H (m) = m \|G (X) (m)\|$
149	148	fveq2d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|H (m)\| = \|m \|G (X) (m)\|\|$
150		id	$⊢ i = m \to i = m$
151		oveq2	$⊢ i = m \to {(\frac{\|X\|}{\|Y\|})}^{i} = {(\frac{\|X\|}{\|Y\|})}^{m}$
152	150 151	oveq12d	$⊢ i = m \to i {(\frac{\|X\|}{\|Y\|})}^{i} = m {(\frac{\|X\|}{\|Y\|})}^{m}$
153		ovex	$⊢ m {(\frac{\|X\|}{\|Y\|})}^{m} \in V$
154	152 37 153	fvmpt	$⊢ m \in ℕ_{0} \to (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i}) (m) = m {(\frac{\|X\|}{\|Y\|})}^{m}$
155	69 154	syl	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i}) (m) = m {(\frac{\|X\|}{\|Y\|})}^{m}$
156	155	oveq2d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to 1 (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i}) (m) = 1 m {(\frac{\|X\|}{\|Y\|})}^{m}$
157	145 149 156	3brtr4d	$⊢ ((φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \land m \in ℤ_{\geq j}) \to \|H (m)\| \leq 1 (i \in ℕ_{0} ⟼ i {(\frac{\|X\|}{\|Y\|})}^{i}) (m)$
158	8 19 39 49 65 66 157	cvgcmpce	$⊢ (φ \land (j \in ℕ_{0} \land \forall k \in ℤ_{\geq j} \|A (k) Y^{k}\| < 1)) \to seq 0 (+ H) \in dom ⇝$
159	18 158	rexlimddv	$⊢ φ \to seq 0 (+ H) \in dom ⇝$

Metamath Proof Explorer

Theorem radcnvlem1

Proof