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	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
	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	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
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^𝑛 𝐹 ) ‘ 𝑘 ) )

Metamath Proof Explorer

Theorem taylplem1

Proof