Metamath Proof Explorer

Theorem eltayl

Description: Value of the Taylor series as a relation (elementhood in the domain here expresses that the series is convergent). (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
taylfval.t ⊢ T = N S Tayl F B
Assertion eltayl ⊢ φ → X T Y ↔ X ∈ ℂ ∧ Y ∈ ℂ 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 taylfval.t ⊢ T = N S Tayl F B
7 1 2 3 4 5 6 taylfval ⊢ φ → T = ⋃ x ∈ ℂ x × ℂ fld tsums k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ x − B k
8 7 eleq2d ⊢ φ → X Y ∈ T ↔ X Y ∈ ⋃ x ∈ ℂ x × ℂ fld tsums k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ x − B k
9 df-br ⊢ X T Y ↔ X Y ∈ T
10 9 bicomi ⊢ X Y ∈ T ↔ X T Y
11 oveq1 ⊢ x = X → x − B = X − B
12 11 oveq1d ⊢ x = X → x − B k = X − B k
13 12 oveq2d ⊢ x = X → S D n F ⁡ k ⁡ B k ! ⁢ x − B k = S D n F ⁡ k ⁡ B k ! ⁢ X − B k
14 13 mpteq2dv ⊢ x = X → k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ x − B k = k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ X − B k
15 14 oveq2d ⊢ x = X → ℂ fld tsums k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ x − B k = ℂ fld tsums k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ X − B k
16 15 opeliunxp2 ⊢ X Y ∈ ⋃ x ∈ ℂ x × ℂ fld tsums k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ x − B k ↔ X ∈ ℂ ∧ Y ∈ ℂ fld tsums k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ X − B k
17 8 10 16 3bitr3g ⊢ φ → X T Y ↔ X ∈ ℂ ∧ Y ∈ ℂ fld tsums k ∈ 0 N ∩ ℤ ⟼ S D n F ⁡ k ⁡ B k ! ⁢ X − B k