pserdvlem1

	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	pserdvlem1	$⊢ (φ \land a \in S) \to (\frac{\|a\| + M}{2} \in ℝ^{+} \land \|a\| < \frac{\|a\| + M}{2} \land \frac{\|a\| + M}{2} < 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	1 2 3 4 5 6	psercnlem1	$⊢ (φ \land a \in S) \to (M \in ℝ^{+} \land \|a\| < M \land M < R)$
16	15	simp1d	$⊢ (φ \land a \in S) \to M \in ℝ^{+}$
17	16	rpred	$⊢ (φ \land a \in S) \to M \in ℝ$
18	14 17	readdcld	$⊢ (φ \land a \in S) \to \|a\| + M \in ℝ$
19		0red	$⊢ (φ \land a \in S) \to 0 \in ℝ$
20	13	absge0d	$⊢ (φ \land a \in S) \to 0 \leq \|a\|$
21	14 16	ltaddrpd	$⊢ (φ \land a \in S) \to \|a\| < \|a\| + M$
22	19 14 18 20 21	lelttrd	$⊢ (φ \land a \in S) \to 0 < \|a\| + M$
23	18 22	elrpd	$⊢ (φ \land a \in S) \to \|a\| + M \in ℝ^{+}$
24	23	rphalfcld	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} \in ℝ^{+}$
25	15	simp2d	$⊢ (φ \land a \in S) \to \|a\| < M$
26		avglt1	$⊢ (\|a\| \in ℝ \land M \in ℝ) \to (\|a\| < M \leftrightarrow \|a\| < \frac{\|a\| + M}{2})$
27	14 17 26	syl2anc	$⊢ (φ \land a \in S) \to (\|a\| < M \leftrightarrow \|a\| < \frac{\|a\| + M}{2})$
28	25 27	mpbid	$⊢ (φ \land a \in S) \to \|a\| < \frac{\|a\| + M}{2}$
29	18	rehalfcld	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} \in ℝ$
30	29	rexrd	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} \in ℝ^{*}$
31	17	rexrd	$⊢ (φ \land a \in S) \to M \in ℝ^{*}$
32		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
33	1 3 4	radcnvcl	$⊢ φ \to R \in [0, +∞]$
34	32 33	sseldi	$⊢ φ \to R \in ℝ^{*}$
35	34	adantr	$⊢ (φ \land a \in S) \to R \in ℝ^{*}$
36		avglt2	$⊢ (\|a\| \in ℝ \land M \in ℝ) \to (\|a\| < M \leftrightarrow \frac{\|a\| + M}{2} < M)$
37	14 17 36	syl2anc	$⊢ (φ \land a \in S) \to (\|a\| < M \leftrightarrow \frac{\|a\| + M}{2} < M)$
38	25 37	mpbid	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} < M$
39	15	simp3d	$⊢ (φ \land a \in S) \to M < R$
40	30 31 35 38 39	xrlttrd	$⊢ (φ \land a \in S) \to \frac{\|a\| + M}{2} < R$
41	24 28 40	3jca	$⊢ (φ \land a \in S) \to (\frac{\|a\| + M}{2} \in ℝ^{+} \land \|a\| < \frac{\|a\| + M}{2} \land \frac{\|a\| + M}{2} < R)$

Metamath Proof Explorer

Theorem pserdvlem1

Proof