Metamath Proof Explorer

Theorem dvnbss

Description: The set of N-times differentiable points is a subset of the domain of the function. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	dvnbss	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑁 ∈ ℕ₀ ) → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		dvnff	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → ( 𝑆 D^𝑛 𝐹 ) : ℕ₀ ⟶ ( ℂ ↑_pm dom 𝐹 ) )
2	1	ffvelrnda	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( ℂ ↑_pm dom 𝐹 ) )
3	2	3impa	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( ℂ ↑_pm dom 𝐹 ) )
4		cnex	⊢ ℂ ∈ V
5		simp2	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑁 ∈ ℕ₀ ) → 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) )
6	5	dmexd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑁 ∈ ℕ₀ ) → dom 𝐹 ∈ V )
7		elpm2g	⊢ ( ( ℂ ∈ V ∧ dom 𝐹 ∈ V ) → ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( ℂ ↑_pm dom 𝐹 ) ↔ ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) : dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⟶ ℂ ∧ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 ) ) )
8	4 6 7	sylancr	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑁 ∈ ℕ₀ ) → ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ∈ ( ℂ ↑_pm dom 𝐹 ) ↔ ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) : dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⟶ ℂ ∧ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 ) ) )
9	3 8	mpbid	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑁 ∈ ℕ₀ ) → ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) : dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⟶ ℂ ∧ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 ) )
10	9	simprd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ∧ 𝑁 ∈ ℕ₀ ) → dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ⊆ dom 𝐹 )