gg-psercn2

Description: Since by pserulm the series converges uniformly, it is also continuous by ulmcn . (Contributed by Mario Carneiro, 3-Mar-2015) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

	Ref	Expression
Hypotheses	gg-pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
	gg-pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
	gg-pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	gg-pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
	gg-pserulm.h	$⊢ H = (i \in ℕ_{0} ⟼ (y \in S ⟼ seq 0 (+ G (y)) (i)))$
	gg-pserulm.m	$⊢ φ \to M \in ℝ$
	gg-pserulm.l	$⊢ φ \to M < R$
	gg-pserulm.y	$⊢ φ \to S \subseteq {abs}^{-1} [[0, M]]$
Assertion	gg-psercn2	$⊢ φ \to F : S \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		gg-pserf.g	$⊢ G = (x \in ℂ ⟼ (n \in ℕ_{0} ⟼ A (n) x^{n}))$
2		gg-pserf.f	$⊢ F = (y \in S ⟼ \sum_{j \in ℕ_{0}} G (y) (j))$
3		gg-pserf.a	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
4		gg-pserf.r	$⊢ R = sup (\{r \in ℝ \| seq 0 (+ G (r)) \in dom ⇝\} ℝ^{*} <)$
5		gg-pserulm.h	$⊢ H = (i \in ℕ_{0} ⟼ (y \in S ⟼ seq 0 (+ G (y)) (i)))$
6		gg-pserulm.m	$⊢ φ \to M \in ℝ$
7		gg-pserulm.l	$⊢ φ \to M < R$
8		gg-pserulm.y	$⊢ φ \to S \subseteq {abs}^{-1} [[0, M]]$
9		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
10		0zd	$⊢ φ \to 0 \in ℤ$
11		cnvimass	$⊢ {abs}^{-1} [[0, M]] \subseteq dom abs$
12		absf	$⊢ abs : ℂ ⟶ ℝ$
13	12	fdmi	$⊢ dom abs = ℂ$
14	11 13	sseqtri	$⊢ {abs}^{-1} [[0, M]] \subseteq ℂ$
15	8 14	sstrdi	$⊢ φ \to S \subseteq ℂ$
16	15	adantr	$⊢ (φ \land i \in ℕ_{0}) \to S \subseteq ℂ$
17	16	resmptd	$⊢ (φ \land i \in ℕ_{0}) \to {(y \in ℂ ⟼ seq 0 (+ G (y)) (i)) ↾}_{S} = (y \in S ⟼ seq 0 (+ G (y)) (i))$
18		simplr	$⊢ (((φ \land i \in ℕ_{0}) \land y \in ℂ) \land k \in (0 \dots i)) \to y \in ℂ$
19		elfznn0	$⊢ k \in (0 \dots i) \to k \in ℕ_{0}$
20	19	adantl	$⊢ (((φ \land i \in ℕ_{0}) \land y \in ℂ) \land k \in (0 \dots i)) \to k \in ℕ_{0}$
21	1	pserval2	$⊢ (y \in ℂ \land k \in ℕ_{0}) \to G (y) (k) = A (k) y^{k}$
22	18 20 21	syl2anc	$⊢ (((φ \land i \in ℕ_{0}) \land y \in ℂ) \land k \in (0 \dots i)) \to G (y) (k) = A (k) y^{k}$
23		simpr	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℕ_{0}$
24	23 9	eleqtrdi	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℤ_{\geq 0}$
25	24	adantr	$⊢ ((φ \land i \in ℕ_{0}) \land y \in ℂ) \to i \in ℤ_{\geq 0}$
26	3	adantr	$⊢ (φ \land i \in ℕ_{0}) \to A : ℕ_{0} ⟶ ℂ$
27	26	ffvelcdmda	$⊢ ((φ \land i \in ℕ_{0}) \land k \in ℕ_{0}) \to A (k) \in ℂ$
28	27	adantlr	$⊢ (((φ \land i \in ℕ_{0}) \land y \in ℂ) \land k \in ℕ_{0}) \to A (k) \in ℂ$
29		expcl	$⊢ (y \in ℂ \land k \in ℕ_{0}) \to y^{k} \in ℂ$
30	29	adantll	$⊢ (((φ \land i \in ℕ_{0}) \land y \in ℂ) \land k \in ℕ_{0}) \to y^{k} \in ℂ$
31	28 30	mulcld	$⊢ (((φ \land i \in ℕ_{0}) \land y \in ℂ) \land k \in ℕ_{0}) \to A (k) y^{k} \in ℂ$
32	19 31	sylan2	$⊢ (((φ \land i \in ℕ_{0}) \land y \in ℂ) \land k \in (0 \dots i)) \to A (k) y^{k} \in ℂ$
33	22 25 32	fsumser	$⊢ ((φ \land i \in ℕ_{0}) \land y \in ℂ) \to \sum_{k = 0}^{i} A (k) y^{k} = seq 0 (+ G (y)) (i)$
34	33	mpteq2dva	$⊢ (φ \land i \in ℕ_{0}) \to (y \in ℂ ⟼ \sum_{k = 0}^{i} A (k) y^{k}) = (y \in ℂ ⟼ seq 0 (+ G (y)) (i))$
35		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
36	35	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
37	36	a1i	$⊢ (φ \land i \in ℕ_{0}) \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
38		fzfid	$⊢ (φ \land i \in ℕ_{0}) \to (0 \dots i) \in Fin$
39	36	a1i	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
40		ffvelcdm	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to A (k) \in ℂ$
41	26 19 40	syl2an	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to A (k) \in ℂ$
42	39 39 41	cnmptc	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to (y \in ℂ ⟼ A (k)) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
43	19	adantl	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to k \in ℕ_{0}$
44	35	gg-expcn	$⊢ k \in ℕ_{0} \to (y \in ℂ ⟼ y^{k}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
45	43 44	syl	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to (y \in ℂ ⟼ y^{k}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
46	35	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
47	46	a1i	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
48		oveq12	$⊢ (u = A (k) \land v = y^{k}) \to u v = A (k) y^{k}$
49	39 42 45 39 39 47 48	cnmpt12	$⊢ ((φ \land i \in ℕ_{0}) \land k \in (0 \dots i)) \to (y \in ℂ ⟼ A (k) y^{k}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
50	35 37 38 49	fsumcn	$⊢ (φ \land i \in ℕ_{0}) \to (y \in ℂ ⟼ \sum_{k = 0}^{i} A (k) y^{k}) \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
51	35	cncfcn1	$⊢ ℂ \underset{cn}{⟶} ℂ = TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld})$
52	50 51	eleqtrrdi	$⊢ (φ \land i \in ℕ_{0}) \to (y \in ℂ ⟼ \sum_{k = 0}^{i} A (k) y^{k}) : ℂ \underset{cn}{⟶} ℂ$
53	34 52	eqeltrrd	$⊢ (φ \land i \in ℕ_{0}) \to (y \in ℂ ⟼ seq 0 (+ G (y)) (i)) : ℂ \underset{cn}{⟶} ℂ$
54		rescncf	$⊢ S \subseteq ℂ \to ((y \in ℂ ⟼ seq 0 (+ G (y)) (i)) : ℂ \underset{cn}{⟶} ℂ \to ({(y \in ℂ ⟼ seq 0 (+ G (y)) (i)) ↾}_{S}) : S \underset{cn}{⟶} ℂ)$
55	16 53 54	sylc	$⊢ (φ \land i \in ℕ_{0}) \to ({(y \in ℂ ⟼ seq 0 (+ G (y)) (i)) ↾}_{S}) : S \underset{cn}{⟶} ℂ$
56	17 55	eqeltrrd	$⊢ (φ \land i \in ℕ_{0}) \to (y \in S ⟼ seq 0 (+ G (y)) (i)) : S \underset{cn}{⟶} ℂ$
57	56 5	fmptd	$⊢ φ \to H : ℕ_{0} ⟶ S \underset{cn}{⟶} ℂ$
58	1 2 3 4 5 6 7 8	pserulm	$⊢ φ \to H \underset{u}{⇝} (S) F$
59	9 10 57 58	ulmcn	$⊢ φ \to F : S \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem gg-psercn2

Proof