psercnlem2

	Ref	Expression
Hypotheses	pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
	pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
	pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
	psercn.s	$⊢ S = {abs}^{-1} [[0, R)]$
	psercnlem2.i	$⊢ (φ \land a \in S) \to (M \in ℝ^{+} \land \|a\| < M \land M < R)$
Assertion	psercnlem2	$⊢ (φ \land a \in S) \to (a \in (0 ball (abs \circ -) M) \land 0 ball (abs \circ -) M \subseteq {abs}^{-1} [[0, M]] \land {abs}^{-1} [[0, M]] \subseteq S)$

Proof

Step	Hyp	Ref	Expression
1		pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
3		pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
4		pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
5		psercn.s	$⊢ S = {abs}^{-1} [[0, R)]$
6		psercnlem2.i	$⊢ (φ \land a \in S) \to (M \in ℝ^{+} \land \|a\| < M \land M < R)$
7		cnvimass	$⊢ {abs}^{-1} [[0, R)] \subseteq dom abs$
8		absf	$⊢ abs : ℂ ⟶ ℝ$
9	8	fdmi	$⊢ dom abs = ℂ$
10	7 9	sseqtri	$⊢ {abs}^{-1} [[0, R)] \subseteq ℂ$
11	5 10	eqsstri	$⊢ S \subseteq ℂ$
12	11	a1i	$⊢ φ \to S \subseteq ℂ$
13	12	sselda	$⊢ (φ \land a \in S) \to a \in ℂ$
14	13	abscld	$⊢ (φ \land a \in S) \to \|a\| \in ℝ$
15	13	absge0d	$⊢ (φ \land a \in S) \to 0 \leq \|a\|$
16	6	simp2d	$⊢ (φ \land a \in S) \to \|a\| < M$
17		0re	$⊢ 0 \in ℝ$
18	6	simp1d	$⊢ (φ \land a \in S) \to M \in ℝ^{+}$
19	18	rpxrd	$⊢ (φ \land a \in S) \to M \in ℝ^{*}$
20		elico2	$⊢ (0 \in ℝ \land M \in ℝ^{*}) \to (\|a\| \in [0, M) \leftrightarrow (\|a\| \in ℝ \land 0 \leq \|a\| \land \|a\| < M))$
21	17 19 20	sylancr	$⊢ (φ \land a \in S) \to (\|a\| \in [0, M) \leftrightarrow (\|a\| \in ℝ \land 0 \leq \|a\| \land \|a\| < M))$
22	14 15 16 21	mpbir3and	$⊢ (φ \land a \in S) \to \|a\| \in [0, M)$
23		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
24		elpreima	$⊢ abs Fn ℂ \to (a \in {abs}^{-1} [[0, M)] \leftrightarrow (a \in ℂ \land \|a\| \in [0, M)))$
25	8 23 24	mp2b	$⊢ a \in {abs}^{-1} [[0, M)] \leftrightarrow (a \in ℂ \land \|a\| \in [0, M))$
26	13 22 25	sylanbrc	$⊢ (φ \land a \in S) \to a \in {abs}^{-1} [[0, M)]$
27		eqid	$⊢ abs \circ - = abs \circ -$
28	27	cnbl0	$⊢ M \in ℝ^{*} \to {abs}^{-1} [[0, M)] = 0 ball (abs \circ -) M$
29	19 28	syl	$⊢ (φ \land a \in S) \to {abs}^{-1} [[0, M)] = 0 ball (abs \circ -) M$
30	26 29	eleqtrd	$⊢ (φ \land a \in S) \to a \in (0 ball (abs \circ -) M)$
31		icossicc	$⊢ [0, M) \subseteq [0, M]$
32		imass2	$⊢ [0, M) \subseteq [0, M] \to {abs}^{-1} [[0, M)] \subseteq {abs}^{-1} [[0, M]]$
33	31 32	mp1i	$⊢ (φ \land a \in S) \to {abs}^{-1} [[0, M)] \subseteq {abs}^{-1} [[0, M]]$
34	29 33	eqsstrrd	$⊢ (φ \land a \in S) \to 0 ball (abs \circ -) M \subseteq {abs}^{-1} [[0, M]]$
35		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
36	1 3 4	radcnvcl	$⊢ φ \to R \in [0, +∞]$
37	36	adantr	$⊢ (φ \land a \in S) \to R \in [0, +∞]$
38	35 37	sseldi	$⊢ (φ \land a \in S) \to R \in ℝ^{*}$
39	6	simp3d	$⊢ (φ \land a \in S) \to M < R$
40		df-ico	$⊢ [.) = (u \in ℝ^{}, v \in ℝ^{} ⟼ \{w \in ℝ^{*} \| (u \leq w \land w < v)\})$
41		df-icc	$⊢ [.] = (u \in ℝ^{}, v \in ℝ^{} ⟼ \{w \in ℝ^{*} \| (u \leq w \land w \leq v)\})$
42		xrlelttr	$⊢ (z \in ℝ^{} \land M \in ℝ^{} \land R \in ℝ^{*}) \to ((z \leq M \land M < R) \to z < R)$
43	40 41 42	ixxss2	$⊢ (R \in ℝ^{*} \land M < R) \to [0, M] \subseteq [0, R)$
44	38 39 43	syl2anc	$⊢ (φ \land a \in S) \to [0, M] \subseteq [0, R)$
45		imass2	$⊢ [0, M] \subseteq [0, R) \to {abs}^{-1} [[0, M]] \subseteq {abs}^{-1} [[0, R)]$
46	44 45	syl	$⊢ (φ \land a \in S) \to {abs}^{-1} [[0, M]] \subseteq {abs}^{-1} [[0, R)]$
47	46 5	sseqtrrdi	$⊢ (φ \land a \in S) \to {abs}^{-1} [[0, M]] \subseteq S$
48	30 34 47	3jca	$⊢ (φ \land a \in S) \to (a \in (0 ball (abs \circ -) M) \land 0 ball (abs \circ -) M \subseteq {abs}^{-1} [[0, M]] \land {abs}^{-1} [[0, M]] \subseteq S)$

Metamath Proof Explorer

Theorem psercnlem2

Proof