Metamath Proof Explorer


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𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑋𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )