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 ⊢ G = x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n
radcnv.a ⊢ φ → A : ℕ 0 ⟶ ℂ
Assertion radcnv0 ⊢ φ → 0 ∈ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 pser.g ⊢ G = x ∈ ℂ ⟼ n ∈ ℕ 0 ⟼ A ⁡ n ⁢ x n
2 radcnv.a ⊢ φ → A : ℕ 0 ⟶ ℂ
3 fveq2 ⊢ r = 0 → G ⁡ r = G ⁡ 0
4 3 seqeq3d ⊢ r = 0 → seq 0 + G ⁡ r = seq 0 + G ⁡ 0
5 4 eleq1d ⊢ r = 0 → seq 0 + G ⁡ r ∈ dom ⁡ ⇝ ↔ seq 0 + G ⁡ 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 k ∈ 0 G ⁡ 0 ⁡ k G ⁡ 0 ⁡ k = G ⁡ 0 ⁡ k
15 0cnd ⊢ φ → 0 ∈ ℂ
16 1 pserval2 ⊢ 0 ∈ ℂ ∧ k ∈ ℕ 0 → G ⁡ 0 ⁡ k = A ⁡ k ⁢ 0 k
17 15 16 sylan ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ 0 ⁡ k = A ⁡ k ⁢ 0 k
18 17 adantr ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → G ⁡ 0 ⁡ k = A ⁡ k ⁢ 0 k
19 simpr ⊢ φ ∧ k ∈ ℕ 0 → k ∈ ℕ 0
20 elnn0 ⊢ k ∈ ℕ 0 ↔ k ∈ ℕ ∨ k = 0
21 19 20 sylib ⊢ φ ∧ k ∈ ℕ 0 → k ∈ ℕ ∨ k = 0
22 21 ord ⊢ φ ∧ k ∈ ℕ 0 → ¬ k ∈ ℕ → k = 0
23 velsn ⊢ k ∈ 0 ↔ k = 0
24 22 23 imbitrrdi ⊢ φ ∧ k ∈ ℕ 0 → ¬ k ∈ ℕ → k ∈ 0
25 24 con1d ⊢ φ ∧ k ∈ ℕ 0 → ¬ k ∈ 0 → k ∈ ℕ
26 25 imp ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → k ∈ ℕ
27 26 0expd ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → 0 k = 0
28 27 oveq2d ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → A ⁡ k ⁢ 0 k = A ⁡ k ⋅ 0
29 2 ffvelcdmda ⊢ φ ∧ k ∈ ℕ 0 → A ⁡ k ∈ ℂ
30 29 adantr ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → A ⁡ k ∈ ℂ
31 30 mul01d ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → A ⁡ k ⋅ 0 = 0
32 18 28 31 3eqtrd ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → G ⁡ 0 ⁡ k = 0
33 32 ifeq2da ⊢ φ ∧ k ∈ ℕ 0 → if k ∈ 0 G ⁡ 0 ⁡ k G ⁡ 0 ⁡ k = if k ∈ 0 G ⁡ 0 ⁡ k 0
34 14 33 eqtr3id ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ 0 ⁡ k = if k ∈ 0 G ⁡ 0 ⁡ k 0
35 13 sselda ⊢ φ ∧ k ∈ 0 → k ∈ ℕ 0
36 1 2 15 psergf ⊢ φ → G ⁡ 0 : ℕ 0 ⟶ ℂ
37 36 ffvelcdmda ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ 0 ⁡ k ∈ ℂ
38 35 37 syldan ⊢ φ ∧ k ∈ 0 → G ⁡ 0 ⁡ k ∈ ℂ
39 7 8 10 13 34 38 fsumcvg3 ⊢ φ → seq 0 + G ⁡ 0 ∈ dom ⁡ ⇝
40 5 6 39 elrabd ⊢ φ → 0 ∈ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝