Metamath Proof Explorer

Theorem taylfvallem

Description: Lemma for taylfval . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses taylfval.s ⊢ φ → S ∈ ℝ ℂ
taylfval.f ⊢ φ → F : A ⟶ ℂ
taylfval.a ⊢ φ → A ⊆ S
taylfval.n ⊢ φ → N ∈ ℕ 0 ∨ N = +∞
taylfval.b ⊢ φ ∧ k ∈ 0 N ∩ ℤ → B ∈ dom ⁡ S D n F ⁡ k
Assertion taylfvallem ⊢ φ ∧ X ∈ ℂ → ℂ fld tsums k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ X − B k ⊆ ℂ

Proof

Step Hyp Ref Expression
1 taylfval.s ⊢ φ → S ∈ ℝ ℂ
2 taylfval.f ⊢ φ → F : A ⟶ ℂ
3 taylfval.a ⊢ φ → A ⊆ S
4 taylfval.n ⊢ φ → N ∈ ℕ 0 ∨ N = +∞
5 taylfval.b ⊢ φ ∧ k ∈ 0 N ∩ ℤ → B ∈ dom ⁡ S D n F ⁡ k
6 cnfldbas ⊢ ℂ = Base ℂ fld
7 cnring ⊢ ℂ fld ∈ Ring
8 ringcmn ⊢ ℂ fld ∈ Ring → ℂ fld ∈ CMnd
9 7 8 mp1i ⊢ φ ∧ X ∈ ℂ → ℂ fld ∈ CMnd
10 cnfldtps ⊢ ℂ fld ∈ TopSp
11 10 a1i ⊢ φ ∧ X ∈ ℂ → ℂ fld ∈ TopSp
12 ovex ⊢ 0 N ∈ V
13 12 inex1 ⊢ 0 N ∩ ℤ ∈ V
14 13 a1i ⊢ φ ∧ X ∈ ℂ → 0 N ∩ ℤ ∈ V
15 1 2 3 4 5 taylfvallem1 ⊢ φ ∧ X ∈ ℂ ∧ k ∈ 0 N ∩ ℤ → S D n F ⁡ k ⁡ B k ! ⁢ X − B k ∈ ℂ
16 15 fmpttd ⊢ φ ∧ X ∈ ℂ → k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ X − B k : 0 N ∩ ℤ ⟶ ℂ
17 6 9 11 14 16 tsmscl ⊢ φ ∧ X ∈ ℂ → ℂ fld tsums k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ X − B k ⊆ ℂ