psercnlem1

	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)]$
	psercn.m	$⊢ M = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
Assertion	psercnlem1	$⊢ (φ \land a \in S) \to (M \in ℝ^{+} \land \|a\| < M \land M < R)$

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		psercn.m	$⊢ M = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
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		readdcl	$⊢ (\|a\| \in ℝ \land R \in ℝ) \to \|a\| + R \in ℝ$
16	14 15	sylan	$⊢ ((φ \land a \in S) \land R \in ℝ) \to \|a\| + R \in ℝ$
17	16	rehalfcld	$⊢ ((φ \land a \in S) \land R \in ℝ) \to \frac{\|a\| + R}{2} \in ℝ$
18		peano2re	$⊢ \|a\| \in ℝ \to \|a\| + 1 \in ℝ$
19	14 18	syl	$⊢ (φ \land a \in S) \to \|a\| + 1 \in ℝ$
20	19	adantr	$⊢ ((φ \land a \in S) \land \neg R \in ℝ) \to \|a\| + 1 \in ℝ$
21	17 20	ifclda	$⊢ (φ \land a \in S) \to if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) \in ℝ$
22	6 21	eqeltrid	$⊢ (φ \land a \in S) \to M \in ℝ$
23		0re	$⊢ 0 \in ℝ$
24	23	a1i	$⊢ (φ \land a \in S) \to 0 \in ℝ$
25	13	absge0d	$⊢ (φ \land a \in S) \to 0 \leq \|a\|$
26		breq2	$⊢ \frac{\|a\| + R}{2} = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) \to (\|a\| < \frac{\|a\| + R}{2} \leftrightarrow \|a\| < if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1))$
27		breq2	$⊢ \|a\| + 1 = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) \to (\|a\| < \|a\| + 1 \leftrightarrow \|a\| < if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1))$
28		simpr	$⊢ (φ \land a \in S) \to a \in S$
29	28 5	eleqtrdi	$⊢ (φ \land a \in S) \to a \in {abs}^{-1} [[0, R)]$
30		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
31		elpreima	$⊢ abs Fn ℂ \to (a \in {abs}^{-1} [[0, R)] \leftrightarrow (a \in ℂ \land \|a\| \in [0, R)))$
32	8 30 31	mp2b	$⊢ a \in {abs}^{-1} [[0, R)] \leftrightarrow (a \in ℂ \land \|a\| \in [0, R))$
33	29 32	sylib	$⊢ (φ \land a \in S) \to (a \in ℂ \land \|a\| \in [0, R))$
34	33	simprd	$⊢ (φ \land a \in S) \to \|a\| \in [0, R)$
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		elico2	$⊢ (0 \in ℝ \land R \in ℝ^{*}) \to (\|a\| \in [0, R) \leftrightarrow (\|a\| \in ℝ \land 0 \leq \|a\| \land \|a\| < R))$
40	23 38 39	sylancr	$⊢ (φ \land a \in S) \to (\|a\| \in [0, R) \leftrightarrow (\|a\| \in ℝ \land 0 \leq \|a\| \land \|a\| < R))$
41	34 40	mpbid	$⊢ (φ \land a \in S) \to (\|a\| \in ℝ \land 0 \leq \|a\| \land \|a\| < R)$
42	41	simp3d	$⊢ (φ \land a \in S) \to \|a\| < R$
43	42	adantr	$⊢ ((φ \land a \in S) \land R \in ℝ) \to \|a\| < R$
44		avglt1	$⊢ (\|a\| \in ℝ \land R \in ℝ) \to (\|a\| < R \leftrightarrow \|a\| < \frac{\|a\| + R}{2})$
45	14 44	sylan	$⊢ ((φ \land a \in S) \land R \in ℝ) \to (\|a\| < R \leftrightarrow \|a\| < \frac{\|a\| + R}{2})$
46	43 45	mpbid	$⊢ ((φ \land a \in S) \land R \in ℝ) \to \|a\| < \frac{\|a\| + R}{2}$
47	14	ltp1d	$⊢ (φ \land a \in S) \to \|a\| < \|a\| + 1$
48	47	adantr	$⊢ ((φ \land a \in S) \land \neg R \in ℝ) \to \|a\| < \|a\| + 1$
49	26 27 46 48	ifbothda	$⊢ (φ \land a \in S) \to \|a\| < if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1)$
50	49 6	breqtrrdi	$⊢ (φ \land a \in S) \to \|a\| < M$
51	24 14 22 25 50	lelttrd	$⊢ (φ \land a \in S) \to 0 < M$
52	22 51	elrpd	$⊢ (φ \land a \in S) \to M \in ℝ^{+}$
53		breq1	$⊢ \frac{\|a\| + R}{2} = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) \to (\frac{\|a\| + R}{2} < R \leftrightarrow if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) < R)$
54		breq1	$⊢ \|a\| + 1 = if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) \to (\|a\| + 1 < R \leftrightarrow if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) < R)$
55		avglt2	$⊢ (\|a\| \in ℝ \land R \in ℝ) \to (\|a\| < R \leftrightarrow \frac{\|a\| + R}{2} < R)$
56	14 55	sylan	$⊢ ((φ \land a \in S) \land R \in ℝ) \to (\|a\| < R \leftrightarrow \frac{\|a\| + R}{2} < R)$
57	43 56	mpbid	$⊢ ((φ \land a \in S) \land R \in ℝ) \to \frac{\|a\| + R}{2} < R$
58	19	rexrd	$⊢ (φ \land a \in S) \to \|a\| + 1 \in ℝ^{*}$
59	38 58	xrlenltd	$⊢ (φ \land a \in S) \to (R \leq \|a\| + 1 \leftrightarrow \neg \|a\| + 1 < R)$
60		0xr	$⊢ 0 \in ℝ^{*}$
61		pnfxr	$⊢ +∞ \in ℝ^{*}$
62		elicc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{}) \to (R \in [0, +∞] \leftrightarrow (R \in ℝ^{*} \land 0 \leq R \land R \leq +∞))$
63	60 61 62	mp2an	$⊢ R \in [0, +∞] \leftrightarrow (R \in ℝ^{*} \land 0 \leq R \land R \leq +∞)$
64	36 63	sylib	$⊢ φ \to (R \in ℝ^{*} \land 0 \leq R \land R \leq +∞)$
65	64	simp2d	$⊢ φ \to 0 \leq R$
66	65	adantr	$⊢ (φ \land a \in S) \to 0 \leq R$
67		ge0gtmnf	$⊢ (R \in ℝ^{*} \land 0 \leq R) \to −∞ < R$
68	38 66 67	syl2anc	$⊢ (φ \land a \in S) \to −∞ < R$
69		xrre	$⊢ ((R \in ℝ^{*} \land \|a\| + 1 \in ℝ) \land (−∞ < R \land R \leq \|a\| + 1)) \to R \in ℝ$
70	69	expr	$⊢ ((R \in ℝ^{*} \land \|a\| + 1 \in ℝ) \land −∞ < R) \to (R \leq \|a\| + 1 \to R \in ℝ)$
71	38 19 68 70	syl21anc	$⊢ (φ \land a \in S) \to (R \leq \|a\| + 1 \to R \in ℝ)$
72	59 71	sylbird	$⊢ (φ \land a \in S) \to (\neg \|a\| + 1 < R \to R \in ℝ)$
73	72	con1d	$⊢ (φ \land a \in S) \to (\neg R \in ℝ \to \|a\| + 1 < R)$
74	73	imp	$⊢ ((φ \land a \in S) \land \neg R \in ℝ) \to \|a\| + 1 < R$
75	53 54 57 74	ifbothda	$⊢ (φ \land a \in S) \to if (R \in ℝ, \frac{\|a\| + R}{2}, \|a\| + 1) < R$
76	6 75	eqbrtrid	$⊢ (φ \land a \in S) \to M < R$
77	52 50 76	3jca	$⊢ (φ \land a \in S) \to (M \in ℝ^{+} \land \|a\| < M \land M < R)$

Metamath Proof Explorer

Theorem psercnlem1

Proof