This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ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 ⇝ } )