radcnvlt1

Description: If X is within the open disk of radius R centered at zero, then the infinite series converges absolutely at X , and also converges when the series is multiplied by n . (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Hypotheses	pser.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
	radcnv.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	radcnv.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
	radcnvlt.x	$⊢ φ \to X \in ℂ$
	radcnvlt.a	$⊢ φ \to \|X\| < R$
	radcnvlt1.h	$⊢ H = (m \in ℕ_{0} ⟼ m \|G (X) (m)\|)$
Assertion	radcnvlt1	$⊢ φ \to (seq 0 (+ H) \in dom ⇝ \land seq 0 (+ (abs \circ G (X))) \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		radcnv.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
4		radcnvlt.x	$⊢ φ \to X \in ℂ$
5		radcnvlt.a	$⊢ φ \to \|X\| < R$
6		radcnvlt1.h	$⊢ H = (m \in ℕ_{0} ⟼ m \|G (X) (m)\|)$
7		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
8	4	abscld	$⊢ φ \to \|X\| \in ℝ$
9	7 8	sselid	$⊢ φ \to \|X\| \in ℝ^{*}$
10		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
11	1 2 3	radcnvcl	$⊢ φ \to R \in [0, +∞]$
12	10 11	sselid	$⊢ φ \to R \in ℝ^{*}$
13		xrltnle	$⊢ (\|X\| \in ℝ^{} \land R \in ℝ^{}) \to (\|X\| < R \leftrightarrow \neg R \leq \|X\|)$
14	9 12 13	syl2anc	$⊢ φ \to (\|X\| < R \leftrightarrow \neg R \leq \|X\|)$
15	5 14	mpbid	$⊢ φ \to \neg R \leq \|X\|$
16	3	breq1i	$⊢ R \leq \|X\| \leftrightarrow sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <) \leq \|X\|$
17		ssrab2	$⊢ \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \subseteq ℝ$
18	17 7	sstri	$⊢ \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \subseteq ℝ^{*}$
19		supxrleub	$⊢ (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} \subseteq ℝ^{} \land \|X\| \in ℝ^{}) \to (sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <) \leq \|X\| \leftrightarrow \forall s \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} s \leq \|X\|)$
20	18 9 19	sylancr	$⊢ φ \to (sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <) \leq \|X\| \leftrightarrow \forall s \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} s \leq \|X\|)$
21	16 20	bitrid	$⊢ φ \to (R \leq \|X\| \leftrightarrow \forall s \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} s \leq \|X\|)$
22		fveq2	$⊢ r = s \to G (r) = G (s)$
23	22	seqeq3d	$⊢ r = s \to seq 0 (+ G (r)) = seq 0 (+ G (s))$
24	23	eleq1d	$⊢ r = s \to (seq 0 (+ G (r)) \in dom ⇝ \leftrightarrow seq 0 (+ G (s)) \in dom ⇝)$
25	24	ralrab	$⊢ \forall s \in \{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} s \leq \|X\| \leftrightarrow \forall s \in ℝ (seq 0 (+ G (s)) \in dom ⇝ \to s \leq \|X\|)$
26	21 25	bitrdi	$⊢ φ \to (R \leq \|X\| \leftrightarrow \forall s \in ℝ (seq 0 (+ G (s)) \in dom ⇝ \to s \leq \|X\|))$
27	15 26	mtbid	$⊢ φ \to \neg \forall s \in ℝ (seq 0 (+ G (s)) \in dom ⇝ \to s \leq \|X\|)$
28		rexanali	$⊢ \exists s \in ℝ (seq 0 (+ G (s)) \in dom ⇝ \land \neg s \leq \|X\|) \leftrightarrow \neg \forall s \in ℝ (seq 0 (+ G (s)) \in dom ⇝ \to s \leq \|X\|)$
29	27 28	sylibr	$⊢ φ \to \exists s \in ℝ (seq 0 (+ G (s)) \in dom ⇝ \land \neg s \leq \|X\|)$
30		ltnle	$⊢ (\|X\| \in ℝ \land s \in ℝ) \to (\|X\| < s \leftrightarrow \neg s \leq \|X\|)$
31	8 30	sylan	$⊢ (φ \land s \in ℝ) \to (\|X\| < s \leftrightarrow \neg s \leq \|X\|)$
32	31	adantr	$⊢ ((φ \land s \in ℝ) \land seq 0 (+ G (s)) \in dom ⇝) \to (\|X\| < s \leftrightarrow \neg s \leq \|X\|)$
33	2	ad2antrr	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to A : ℕ_{0} ⟶ ℂ$
34	4	ad2antrr	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to X \in ℂ$
35		simplr	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to s \in ℝ$
36	35	recnd	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to s \in ℂ$
37		simprr	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to \|X\| < s$
38		0red	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to 0 \in ℝ$
39	34	abscld	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to \|X\| \in ℝ$
40	34	absge0d	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to 0 \leq \|X\|$
41	38 39 35 40 37	lelttrd	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to 0 < s$
42	38 35 41	ltled	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to 0 \leq s$
43	35 42	absidd	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to \|s\| = s$
44	37 43	breqtrrd	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to \|X\| < \|s\|$
45		simprl	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to seq 0 (+ G (s)) \in dom ⇝$
46	1 33 34 36 44 45 6	radcnvlem1	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to seq 0 (+ H) \in dom ⇝$
47	1 33 34 36 44 45	radcnvlem2	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to seq 0 (+ (abs \circ G (X))) \in dom ⇝$
48	46 47	jca	$⊢ ((φ \land s \in ℝ) \land (seq 0 (+ G (s)) \in dom ⇝ \land \|X\| < s)) \to (seq 0 (+ H) \in dom ⇝ \land seq 0 (+ (abs \circ G (X))) \in dom ⇝)$
49	48	expr	$⊢ ((φ \land s \in ℝ) \land seq 0 (+ G (s)) \in dom ⇝) \to (\|X\| < s \to (seq 0 (+ H) \in dom ⇝ \land seq 0 (+ (abs \circ G (X))) \in dom ⇝))$
50	32 49	sylbird	$⊢ ((φ \land s \in ℝ) \land seq 0 (+ G (s)) \in dom ⇝) \to (\neg s \leq \|X\| \to (seq 0 (+ H) \in dom ⇝ \land seq 0 (+ (abs \circ G (X))) \in dom ⇝))$
51	50	expimpd	$⊢ (φ \land s \in ℝ) \to ((seq 0 (+ G (s)) \in dom ⇝ \land \neg s \leq \|X\|) \to (seq 0 (+ H) \in dom ⇝ \land seq 0 (+ (abs \circ G (X))) \in dom ⇝))$
52	51	rexlimdva	$⊢ φ \to (\exists s \in ℝ (seq 0 (+ G (s)) \in dom ⇝ \land \neg s \leq \|X\|) \to (seq 0 (+ H) \in dom ⇝ \land seq 0 (+ (abs \circ G (X))) \in dom ⇝))$
53	29 52	mpd	$⊢ φ \to (seq 0 (+ H) \in dom ⇝ \land seq 0 (+ (abs \circ G (X))) \in dom ⇝)$

Metamath Proof Explorer

Theorem radcnvlt1

Proof