Metamath Proof Explorer

Theorem taylplem2

Description: Lemma for taylpfval and similar theorems. (Contributed by Mario Carneiro, 31-Dec-2016)

Ref Expression
Hypotheses taylpfval.s ⊢ φ → S ∈ ℝ ℂ
taylpfval.f ⊢ φ → F : A ⟶ ℂ
taylpfval.a ⊢ φ → A ⊆ S
taylpfval.n ⊢ φ → N ∈ ℕ 0
taylpfval.b ⊢ φ → B ∈ dom ⁡ S D n F ⁡ N
Assertion taylplem2 ⊢ φ ∧ X ∈ ℂ ∧ k ∈ 0 … N → S D n F ⁡ k ⁡ B k ! ⁢ X − B k ∈ ℂ

Proof

Step Hyp Ref Expression
1 taylpfval.s ⊢ φ → S ∈ ℝ ℂ
2 taylpfval.f ⊢ φ → F : A ⟶ ℂ
3 taylpfval.a ⊢ φ → A ⊆ S
4 taylpfval.n ⊢ φ → N ∈ ℕ 0
5 taylpfval.b ⊢ φ → B ∈ dom ⁡ S D n F ⁡ N
6 0z ⊢ 0 ∈ ℤ
7 4 nn0zd ⊢ φ → N ∈ ℤ
8 fzval2 ⊢ 0 ∈ ℤ ∧ N ∈ ℤ → 0 … N = 0 N ∩ ℤ
9 6 7 8 sylancr ⊢ φ → 0 … N = 0 N ∩ ℤ
10 9 eleq2d ⊢ φ → k ∈ 0 … N ↔ k ∈ 0 N ∩ ℤ
11 10 adantr ⊢ φ ∧ X ∈ ℂ → k ∈ 0 … N ↔ k ∈ 0 N ∩ ℤ
12 11 biimpa ⊢ φ ∧ X ∈ ℂ ∧ k ∈ 0 … N → k ∈ 0 N ∩ ℤ
13 4 orcd ⊢ φ → N ∈ ℕ 0 ∨ N = +∞
14 1 2 3 4 5 taylplem1 ⊢ φ ∧ k ∈ 0 N ∩ ℤ → B ∈ dom ⁡ S D n F ⁡ k
15 1 2 3 13 14 taylfvallem1 ⊢ φ ∧ X ∈ ℂ ∧ k ∈ 0 N ∩ ℤ → S D n F ⁡ k ⁡ B k ! ⁢ X − B k ∈ ℂ
16 12 15 syldan ⊢ φ ∧ X ∈ ℂ ∧ k ∈ 0 … N → S D n F ⁡ k ⁡ B k ! ⁢ X − B k ∈ ℂ