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		elnn0	⊢ ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
20	19	bilani	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
21	20	ord	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ¬ 𝑘 ∈ ℕ → 𝑘 = 0 ) )
22		velsn	⊢ ( 𝑘 ∈ { 0 } ↔ 𝑘 = 0 )
23	21 22	imbitrrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ¬ 𝑘 ∈ ℕ → 𝑘 ∈ { 0 } ) )
24	23	con1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ¬ 𝑘 ∈ { 0 } → 𝑘 ∈ ℕ ) )
25	24	imp	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → 𝑘 ∈ ℕ )
26	25	0expd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( 0 ↑ 𝑘 ) = 0 )
27	26	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · 0 ) )
28	2	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
29	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
30	29	mul01d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( ( 𝐴 ‘ 𝑘 ) · 0 ) = 0 )
31	18 27 30	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ { 0 } ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) = 0 )
32	31	ifeq2da	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ { 0 } , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) ) = if ( 𝑘 ∈ { 0 } , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) , 0 ) )
33	14 32	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) = if ( 𝑘 ∈ { 0 } , ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) , 0 ) )
34	13	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 0 } ) → 𝑘 ∈ ℕ0 )
35	1 2 15	psergf	⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) : ℕ0 ⟶ ℂ )
36	35	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ )
37	34 36	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 0 } ) → ( ( 𝐺 ‘ 0 ) ‘ 𝑘 ) ∈ ℂ )
38	7 8 10 13 33 37	fsumcvg3	⊢ ( 𝜑 → seq 0 ( + , ( 𝐺 ‘ 0 ) ) ∈ dom ⇝ )
39	5 6 38	elrabd	⊢ ( 𝜑 → 0 ∈ { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( 𝐺 ‘ 𝑟 ) ) ∈ dom ⇝ } )