Theorem cpncn

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

	Ref	Expression
Assertion	cpncn	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
2	1	adantr	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝑆 ⊆ ℂ )
3		simpl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝑆 ∈ { ℝ , ℂ } )
4		0nn0	⊢ 0 ∈ ℕ0
5	4	a1i	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 0 ∈ ℕ0 )
6		elfvdm	⊢ ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) → 𝑁 ∈ dom ( 𝓑C𝑛 ‘ 𝑆 ) )
7	6	adantl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝑁 ∈ dom ( 𝓑C𝑛 ‘ 𝑆 ) )
8		fncpn	⊢ ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) Fn ℕ0 )
9		fndm	⊢ ( ( 𝓑C𝑛 ‘ 𝑆 ) Fn ℕ0 → dom ( 𝓑C𝑛 ‘ 𝑆 ) = ℕ0 )
10	2 8 9	3syl	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → dom ( 𝓑C𝑛 ‘ 𝑆 ) = ℕ0 )
11	7 10	eleqtrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
12		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
13	11 12	eleqtrdi	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
14		cpnord	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 0 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 0 ) ) → ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ⊆ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 0 ) )
15	3 5 13 14	syl3anc	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ⊆ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 0 ) )
16		simpr	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) )
17	15 16	sseldd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 0 ) )
18		elcpn	⊢ ( ( 𝑆 ⊆ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 0 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) )
19	2 5 18	syl2anc	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → ( 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 0 ) ↔ ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) ) )
20	17 19	mpbid	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → ( 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) ) )
21	20	simpld	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
22		dvn0	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
23	2 21 22	syl2anc	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) = 𝐹 )
24	20	simprd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 0 ) ∈ ( dom 𝐹 –cn→ ℂ ) )
25	23 24	eqeltrrd	⊢ ( ( 𝑆 ∈ { ℝ , ℂ } ∧ 𝐹 ∈ ( ( 𝓑C𝑛 ‘ 𝑆 ) ‘ 𝑁 ) ) → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )