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 elnn0 ⊢ k ∈ ℕ 0 ↔ k ∈ ℕ ∨ k = 0
20 19 bilani ⊢ φ ∧ k ∈ ℕ 0 → k ∈ ℕ ∨ k = 0
21 20 ord ⊢ φ ∧ k ∈ ℕ 0 → ¬ k ∈ ℕ → k = 0
22 velsn ⊢ k ∈ 0 ↔ k = 0
23 21 22 imbitrrdi ⊢ φ ∧ k ∈ ℕ 0 → ¬ k ∈ ℕ → k ∈ 0
24 23 con1d ⊢ φ ∧ k ∈ ℕ 0 → ¬ k ∈ 0 → k ∈ ℕ
25 24 imp ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → k ∈ ℕ
26 25 0expd ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → 0 k = 0
27 26 oveq2d ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → A ⁡ k ⁢ 0 k = A ⁡ k ⋅ 0
28 2 ffvelcdmda ⊢ φ ∧ k ∈ ℕ 0 → A ⁡ k ∈ ℂ
29 28 adantr ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → A ⁡ k ∈ ℂ
30 29 mul01d ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → A ⁡ k ⋅ 0 = 0
31 18 27 30 3eqtrd ⊢ φ ∧ k ∈ ℕ 0 ∧ ¬ k ∈ 0 → G ⁡ 0 ⁡ k = 0
32 31 ifeq2da ⊢ φ ∧ k ∈ ℕ 0 → if k ∈ 0 G ⁡ 0 ⁡ k G ⁡ 0 ⁡ k = if k ∈ 0 G ⁡ 0 ⁡ k 0
33 14 32 eqtr3id ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ 0 ⁡ k = if k ∈ 0 G ⁡ 0 ⁡ k 0
34 13 sselda ⊢ φ ∧ k ∈ 0 → k ∈ ℕ 0
35 1 2 15 psergf ⊢ φ → G ⁡ 0 : ℕ 0 ⟶ ℂ
36 35 ffvelcdmda ⊢ φ ∧ k ∈ ℕ 0 → G ⁡ 0 ⁡ k ∈ ℂ
37 34 36 syldan ⊢ φ ∧ k ∈ 0 → G ⁡ 0 ⁡ k ∈ ℂ
38 7 8 10 13 33 37 fsumcvg3 ⊢ φ → seq 0 + G ⁡ 0 ∈ dom ⁡ ⇝
39 5 6 38 elrabd ⊢ φ → 0 ∈ r ∈ ℝ | seq 0 + G ⁡ r ∈ dom ⁡ ⇝