cpncn

Description: A C^n function is continuous. (Contributed by Mario Carneiro, 11-Feb-2015)

		Ref	Expression
	Assertion	cpncn	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to F : dom F \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
2	1	adantr	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to S \subseteq ℂ$
3		simpl	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to S \in \{ℝ, ℂ\}$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5	4	a1i	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to 0 \in ℕ_{0}$
6		elfvdm	$⊢ F \in C^{n} (S) (N) \to N \in dom C^{n} (S)$
7	6	adantl	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to N \in dom C^{n} (S)$
8		fncpn	$⊢ S \subseteq ℂ \to C^{n} (S) Fn ℕ_{0}$
9		fndm	$⊢ C^{n} (S) Fn ℕ_{0} \to dom C^{n} (S) = ℕ_{0}$
10	2 8 9	3syl	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to dom C^{n} (S) = ℕ_{0}$
11	7 10	eleqtrd	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to N \in ℕ_{0}$
12		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
13	11 12	eleqtrdi	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to N \in ℤ_{\geq 0}$
14		cpnord	$⊢ (S \in \{ℝ, ℂ\} \land 0 \in ℕ_{0} \land N \in ℤ_{\geq 0}) \to C^{n} (S) (N) \subseteq C^{n} (S) (0)$
15	3 5 13 14	syl3anc	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to C^{n} (S) (N) \subseteq C^{n} (S) (0)$
16		simpr	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to F \in C^{n} (S) (N)$
17	15 16	sseldd	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to F \in C^{n} (S) (0)$
18		elcpn	$⊢ (S \subseteq ℂ \land 0 \in ℕ_{0}) \to (F \in C^{n} (S) (0) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} F) (0) : dom F \underset{cn}{⟶} ℂ))$
19	2 5 18	syl2anc	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to (F \in C^{n} (S) (0) \leftrightarrow (F \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} F) (0) : dom F \underset{cn}{⟶} ℂ))$
20	17 19	mpbid	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to (F \in (ℂ ↑_{𝑝𝑚} S) \land (S D^{n} F) (0) : dom F \underset{cn}{⟶} ℂ)$
21	20	simpld	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
22		dvn0	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0) = F$
23	2 21 22	syl2anc	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to (S D^{n} F) (0) = F$
24	20	simprd	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to (S D^{n} F) (0) : dom F \underset{cn}{⟶} ℂ$
25	23 24	eqeltrrd	$⊢ (S \in \{ℝ, ℂ\} \land F \in C^{n} (S) (N)) \to F : dom F \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem cpncn

Proof