Theorem psercn2

Description: Since by pserulm the series converges uniformly, it is also continuous by ulmcn . (Contributed by Mario Carneiro, 3-Mar-2015)

	Ref	Expression
Hypotheses	pserf.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
	pserf.f	⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
	pserf.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
	pserf.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
	pserulm.h	⊢ 𝐻 = ( 𝑖 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
	pserulm.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	pserulm.l	⊢ ( 𝜑 → 𝑀 < 𝑅 )
	pserulm.y	⊢ ( 𝜑 → 𝑆 ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
Assertion	psercn2	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		pserf.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2		pserf.f	⊢ 𝐹 = ( 𝑦 ∈ 𝑆 ↦ Σ 𝑗 ∈ ℕ0 ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑗 ) )
3		pserf.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
4		pserf.r	⊢ 𝑅 = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
5		pserulm.h	⊢ 𝐻 = ( 𝑖 ∈ ℕ0 ↦ ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
6		pserulm.m	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
7		pserulm.l	⊢ ( 𝜑 → 𝑀 < 𝑅 )
8		pserulm.y	⊢ ( 𝜑 → 𝑆 ⊆ ( ◡ abs “ ( 0 [,] 𝑀 ) ) )
9		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
10		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
11		cnvimass	⊢ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ dom abs
12		absf	⊢ abs : ℂ ⟶ ℝ
13	12	fdmi	⊢ dom abs = ℂ
14	11 13	sseqtri	⊢ ( ◡ abs “ ( 0 [,] 𝑀 ) ) ⊆ ℂ
15	8 14	sstrdi	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑆 ⊆ ℂ )
17	16	resmptd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ↾ 𝑆 ) = ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
18		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → 𝑦 ∈ ℂ )
19		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑖 ) → 𝑘 ∈ ℕ0 )
20	19	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → 𝑘 ∈ ℕ0 )
21	1	pserval2	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) )
22	18 20 21	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( ( 𝐺 ‘ 𝑦 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
24	23 9	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) → 𝑖 ∈ ( ℤ≥ ‘ 0 ) )
26	3	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐴 : ℕ0 ⟶ ℂ )
27	26	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
28	27	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
29		expcl	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦 ↑ 𝑘 ) ∈ ℂ )
30	29	adantll	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑦 ↑ 𝑘 ) ∈ ℂ )
31	28 30	mulcld	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ∈ ℂ )
32	19 31	sylan2	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ∈ ℂ )
33	22 25 32	fsumser	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑦 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑖 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) = ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) )
34	33	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑖 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) )
35		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
36	35	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
37	36	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
38		fzfid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 0 ... 𝑖 ) ∈ Fin )
39	36	a1i	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
40		ffvelcdm	⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
41	26 19 40	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
42	39 39 41	cnmptc	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑦 ∈ ℂ ↦ ( 𝐴 ‘ 𝑘 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
43	19	adantl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → 𝑘 ∈ ℕ0 )
44	35	expcn	⊢ ( 𝑘 ∈ ℕ0 → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑘 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
45	43 44	syl	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑘 ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
46	35	mulcn	⊢ · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) )
47	46	a1i	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → · ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( TopOpen ‘ ℂfld ) ) Cn ( TopOpen ‘ ℂfld ) ) )
48	39 42 45 47	cnmpt12f	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑖 ) ) → ( 𝑦 ∈ ℂ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
49	35 37 38 48	fsumcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑖 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) ) )
50	35	cncfcn1	⊢ ( ℂ –cn→ ℂ ) = ( ( TopOpen ‘ ℂfld ) Cn ( TopOpen ‘ ℂfld ) )
51	49 50	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑖 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑦 ↑ 𝑘 ) ) ) ∈ ( ℂ –cn→ ℂ ) )
52	34 51	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ ( ℂ –cn→ ℂ ) )
53		rescncf	⊢ ( 𝑆 ⊆ ℂ → ( ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ ( ℂ –cn→ ℂ ) → ( ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ↾ 𝑆 ) ∈ ( 𝑆 –cn→ ℂ ) ) )
54	16 52 53	sylc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑦 ∈ ℂ ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ↾ 𝑆 ) ∈ ( 𝑆 –cn→ ℂ ) )
55	17 54	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑦 ∈ 𝑆 ↦ ( seq 0 ( + , ( 𝐺 ‘ 𝑦 ) ) ‘ 𝑖 ) ) ∈ ( 𝑆 –cn→ ℂ ) )
56	55 5	fmptd	⊢ ( 𝜑 → 𝐻 : ℕ0 ⟶ ( 𝑆 –cn→ ℂ ) )
57	1 2 3 4 5 6 7 8	pserulm	⊢ ( 𝜑 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐹 )
58	9 10 56 57	ulmcn	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 –cn→ ℂ ) )