Theorem radcnv0

Description: Zero is always a convergent point for any power series. (Contributed by Mario Carneiro, 26-Feb-2015)

	Ref	Expression
Hypotheses	pser.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
	radcnv.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
Assertion	radcnv0	⊢ ( 𝜑 → 0 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )

Proof

Step	Hyp	Ref	Expression
1		pser.g	⊢ 𝐺 = ( 𝑥 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
2		radcnv.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
3		fveq2	⊢ ( 𝑟 = 0 → ( 𝐺 ‘ 𝑟 ) = ( 𝐺 ‘ 0 ) )
4	3	seqeq3d	⊢ ( 𝑟 = 0 → seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) = seq 0 ( + , ( 𝐺 ‘ 0 ) ) )
5	4	eleq1d	⊢ ( 𝑟 = 0 → ( seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( 𝐺 ‘ 0 ) ) ∈ dom ⇝ ) )
6		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
7		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
8		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
9		snfi	⊢ { 0 } ∈ Fin
10	9	a1i	⊢ ( 𝜑 → { 0 } ∈ Fin )
11		0nn0	⊢ 0 ∈ ℕ0
12	11	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
13	12	snssd	⊢ ( 𝜑 → { 0 } ⊆ ℕ0 )
14		ifid	⊢ if ( 𝑘 ∈ { 0 } , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) ) = ( ( 𝐺 ‘ 0 ) ‘ 𝑘 )
15		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
16	1	pserval2	⊢ ( ( 0 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) )
17	15 16	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) )
18	17	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
20		elnn0	⊢ ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
21	19 20	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
22	21	ord	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ¬ 𝑘 ∈ ℕ → 𝑘 = 0 ) )
23		velsn	⊢ ( 𝑘 ∈ { 0 } ↔ 𝑘 = 0 )
24	22 23	syl6ibr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ¬ 𝑘 ∈ ℕ → 𝑘 ∈ { 0 } ) )
25	24	con1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ¬ 𝑘 ∈ { 0 } → 𝑘 ∈ ℕ ) )
26	25	imp	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → 𝑘 ∈ ℕ )
27	26	0expd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( 0 ↑ 𝑘 ) = 0 )
28	27	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · 0 ) )
29	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
30	29	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
31	30	mul01d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( ( 𝐴 ‘ 𝑘 ) · 0 ) = 0 )
32	18 28 31	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) = 0 )
33	32	ifeq2da	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ { 0 } , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) ) = if ( 𝑘 ∈ { 0 } , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) , 0 ) )
34	14 33	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) = if ( 𝑘 ∈ { 0 } , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) , 0 ) )
35	13	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 0 } ) → 𝑘 ∈ ℕ0 )
36	1 2 15	psergf	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) : ℕ0 ⟶ ℂ )
37	36	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ )
38	35 37	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 0 } ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ )
39	7 8 10 13 34 38	fsumcvg3	⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 0 ) ) ∈ dom ⇝ )
40	5 6 39	elrabd	⊢ ( 𝜑 → 0 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )