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

Metamath Proof Explorer

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→ ℂ ) )