Theorem taylplem2

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

	Ref	Expression
Hypotheses	taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
Assertion	taylplem2	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
6		0z	⊢ 0 ∈ ℤ
7	4	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
8		fzval2	⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ... 𝑁 ) = ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
9	6 7 8	sylancr	⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
10	9	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) )
12	11	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
13	4	orcd	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
14	1 2 3 4 5	taylplem1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
15	1 2 3 13 14	taylfvallem1	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )
16	12 15	syldan	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )