This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elcpn

Description: Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion elcpn ⊢ S ⊆ ℂ ∧ N ∈ ℕ 0 → F ∈ C n ⁡ S ⁡ N ↔ F ∈ ℂ ↑ 𝑝𝑚 S ∧ S D n F ⁡ N : dom ⁡ F ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 cpnfval ⊢ S ⊆ ℂ → C n ⁡ S = n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ
2 1 fveq1d ⊢ S ⊆ ℂ → C n ⁡ S ⁡ N = n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ ⁡ N
3 fveq2 ⊢ n = N → S D n f ⁡ n = S D n f ⁡ N
4 3 eleq1d ⊢ n = N → S D n f ⁡ n : dom ⁡ f ⟶cn ℂ ↔ S D n f ⁡ N : dom ⁡ f ⟶cn ℂ
5 4 rabbidv ⊢ n = N → f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ = f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ N : dom ⁡ f ⟶cn ℂ
6 eqid ⊢ n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ = n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ
7 ovex ⊢ ℂ ↑ 𝑝𝑚 S ∈ V
8 7 rabex ⊢ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ N : dom ⁡ f ⟶cn ℂ ∈ V
9 5 6 8 fvmpt ⊢ N ∈ ℕ 0 → n ∈ ℕ 0 ⟼ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ n : dom ⁡ f ⟶cn ℂ ⁡ N = f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ N : dom ⁡ f ⟶cn ℂ
10 2 9 sylan9eq ⊢ S ⊆ ℂ ∧ N ∈ ℕ 0 → C n ⁡ S ⁡ N = f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ N : dom ⁡ f ⟶cn ℂ
11 10 eleq2d ⊢ S ⊆ ℂ ∧ N ∈ ℕ 0 → F ∈ C n ⁡ S ⁡ N ↔ F ∈ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ N : dom ⁡ f ⟶cn ℂ
12 oveq2 ⊢ f = F → S D n f = S D n F
13 12 fveq1d ⊢ f = F → S D n f ⁡ N = S D n F ⁡ N
14 dmeq ⊢ f = F → dom ⁡ f = dom ⁡ F
15 14 oveq1d ⊢ f = F → dom ⁡ f ⟶cn ℂ = dom ⁡ F ⟶cn ℂ
16 13 15 eleq12d ⊢ f = F → S D n f ⁡ N : dom ⁡ f ⟶cn ℂ ↔ S D n F ⁡ N : dom ⁡ F ⟶cn ℂ
17 16 elrab ⊢ F ∈ f ∈ ℂ ↑ 𝑝𝑚 S | S D n f ⁡ N : dom ⁡ f ⟶cn ℂ ↔ F ∈ ℂ ↑ 𝑝𝑚 S ∧ S D n F ⁡ N : dom ⁡ F ⟶cn ℂ
18 11 17 bitrdi ⊢ S ⊆ ℂ ∧ N ∈ ℕ 0 → F ∈ C n ⁡ S ⁡ N ↔ F ∈ ℂ ↑ 𝑝𝑚 S ∧ S D n F ⁡ N : dom ⁡ F ⟶cn ℂ