Metamath Proof Explorer

Theorem dvnf

Description: The N-times derivative is a function. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvnf ⊢ S ∈ ℝ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S ∧ N ∈ ℕ 0 → S D n F ⁡ N : dom ⁡ S D n F ⁡ N ⟶ ℂ

Proof

Step Hyp Ref Expression
1 dvnff ⊢ S ∈ ℝ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S → S D n F : ℕ 0 ⟶ ℂ ↑ 𝑝𝑚 dom ⁡ F
2 1 ffvelrnda ⊢ S ∈ ℝ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S ∧ N ∈ ℕ 0 → S D n F ⁡ N ∈ ℂ ↑ 𝑝𝑚 dom ⁡ F
3 2 3impa ⊢ S ∈ ℝ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S ∧ N ∈ ℕ 0 → S D n F ⁡ N ∈ ℂ ↑ 𝑝𝑚 dom ⁡ F
4 cnex ⊢ ℂ ∈ V
5 simp2 ⊢ S ∈ ℝ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S ∧ N ∈ ℕ 0 → F ∈ ℂ ↑ 𝑝𝑚 S
6 5 dmexd ⊢ S ∈ ℝ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S ∧ N ∈ ℕ 0 → dom ⁡ F ∈ V
7 elpm2g ⊢ ℂ ∈ V ∧ dom ⁡ F ∈ V → S D n F ⁡ N ∈ ℂ ↑ 𝑝𝑚 dom ⁡ F ↔ S D n F ⁡ N : dom ⁡ S D n F ⁡ N ⟶ ℂ ∧ dom ⁡ S D n F ⁡ N ⊆ dom ⁡ F
8 4 6 7 sylancr ⊢ S ∈ ℝ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S ∧ N ∈ ℕ 0 → S D n F ⁡ N ∈ ℂ ↑ 𝑝𝑚 dom ⁡ F ↔ S D n F ⁡ N : dom ⁡ S D n F ⁡ N ⟶ ℂ ∧ dom ⁡ S D n F ⁡ N ⊆ dom ⁡ F
9 3 8 mpbid ⊢ S ∈ ℝ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S ∧ N ∈ ℕ 0 → S D n F ⁡ N : dom ⁡ S D n F ⁡ N ⟶ ℂ ∧ dom ⁡ S D n F ⁡ N ⊆ dom ⁡ F
10 9 simpld ⊢ S ∈ ℝ ℂ ∧ F ∈ ℂ ↑ 𝑝𝑚 S ∧ N ∈ ℕ 0 → S D n F ⁡ N : dom ⁡ S D n F ⁡ N ⟶ ℂ