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 \subseteq ℂ \land N \in ℕ_{0}) \to (F \in C^{n} (S) (N) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ))$

Proof

Step	Hyp	Ref	Expression
1		cpnfval	$⊢ S \subseteq ℂ \to C^{n} (S) = (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\})$
2	1	fveq1d	$⊢ S \subseteq ℂ \to C^{n} (S) (N) = (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\}) (N)$
3		fveq2	$⊢ n = N \to (S D^{n} f) (n) = (S D^{n} f) (N)$
4	3	eleq1d	$⊢ n = N \to ((S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ \leftrightarrow (S D^{n} f) (N) : dom f \underset{cn}{⟶} ℂ)$
5	4	rabbidv	$⊢ n = N \to \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\} = \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (N) : dom f \underset{cn}{⟶} ℂ\}$
6		eqid	$⊢ (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\}) = (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\})$
7		ovex	$⊢ ℂ ↑_{𝑝𝑚} S \in V$
8	7	rabex	$⊢ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (N) : dom f \underset{cn}{⟶} ℂ\} \in V$
9	5 6 8	fvmpt	$⊢ N \in ℕ_{0} \to (n \in ℕ_{0} ⟼ \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (n) : dom f \underset{cn}{⟶} ℂ\}) (N) = \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (N) : dom f \underset{cn}{⟶} ℂ\}$
10	2 9	sylan9eq	$⊢ (S \subseteq ℂ \land N \in ℕ_{0}) \to C^{n} (S) (N) = \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (N) : dom f \underset{cn}{⟶} ℂ\}$
11	10	eleq2d	$⊢ (S \subseteq ℂ \land N \in ℕ_{0}) \to (F \in C^{n} (S) (N) \leftrightarrow F \in \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (N) : dom f \underset{cn}{⟶} ℂ\})$
12		oveq2	$⊢ f = F \to S D^{n} f = S D^{n} F$
13	12	fveq1d	$⊢ f = F \to (S D^{n} f) (N) = (S D^{n} F) (N)$
14		dmeq	$⊢ f = F \to dom f = dom F$
15	14	oveq1d	$⊢ f = F \to dom f \underset{cn}{⟶} ℂ = dom F \underset{cn}{⟶} ℂ$
16	13 15	eleq12d	$⊢ f = F \to ((S D^{n} f) (N) : dom f \underset{cn}{⟶} ℂ \leftrightarrow (S D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ)$
17	16	elrab	$⊢ F \in \{f \in (ℂ ↑_{𝑝𝑚} S) \| (S D^{n} f) (N) : dom f \underset{cn}{⟶} ℂ\} \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ)$
18	11 17	bitrdi	$⊢ (S \subseteq ℂ \land N \in ℕ_{0}) \to (F \in C^{n} (S) (N) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} F) (N) : dom F \underset{cn}{⟶} ℂ))$