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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	taylfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	taylfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	taylfval.n	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
	taylfval.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
	taylfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
Assertion	eltayl	⊢ ( 𝜑 → ( 𝑋 𝑇 𝑌 ↔ ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		taylfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		taylfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		taylfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		taylfval.n	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
5		taylfval.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
6		taylfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7	1 2 3 4 5 6	taylfval	⊢ ( 𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
8	7	eleq2d	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝑇 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ) )
9		df-br	⊢ ( 𝑋 𝑇 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝑇 )
10	9	bicomi	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ 𝑇 ↔ 𝑋 𝑇 𝑌 )
11		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 𝐵 ) = ( 𝑋 − 𝐵 ) )
12	11	oveq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) = ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) )
13	12	oveq2d	⊢ ( 𝑥 = 𝑋 → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) = ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) )
14	13	mpteq2dv	⊢ ( 𝑥 = 𝑋 → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ) )
15	14	oveq2d	⊢ ( 𝑥 = 𝑋 → ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) = ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ) ) )
16	15	opeliunxp2	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ↔ ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
17	8 10 16	3bitr3g	⊢ ( 𝜑 → ( 𝑋 𝑇 𝑌 ↔ ( 𝑋 ∈ ℂ ∧ 𝑌 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ) )