Metamath Proof Explorer


Theorem taylplem1

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 taylplem1 ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 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 biimpar ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
12 cnex ℂ ∈ V
13 12 a1i ( 𝜑 → ℂ ∈ V )
14 elpm2r ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
15 13 1 2 3 14 syl22anc ( 𝜑𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
16 1 15 jca ( 𝜑 → ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) )
17 dvn2bss ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
18 17 3expa ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
19 16 18 sylan ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
20 5 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
21 19 20 sseldd ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
22 11 21 syldan ( ( 𝜑𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )