Metamath Proof Explorer


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 ⇝ } )