Metamath Proof Explorer

Theorem cpncn

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

Ref Expression
Assertion cpncn 
|- ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> F e. ( dom F -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
2 1 adantr 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> S C_ CC )
3 simpl 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> S e. { RR , CC } )
4 0nn0 
 |-  0 e. NN0
5 4 a1i 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> 0 e. NN0 )
6 elfvdm 
 |-  ( F e. ( ( C^n ` S ) ` N ) -> N e. dom ( C^n ` S ) )
7 6 adantl 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> N e. dom ( C^n ` S ) )
8 fncpn 
 |-  ( S C_ CC -> ( C^n ` S ) Fn NN0 )
9 fndm 
 |-  ( ( C^n ` S ) Fn NN0 -> dom ( C^n ` S ) = NN0 )
10 2 8 9 3syl 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> dom ( C^n ` S ) = NN0 )
11 7 10 eleqtrd 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> N e. NN0 )
12 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
13 11 12 eleqtrdi 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> N e. ( ZZ>= ` 0 ) )
14 cpnord 
 |-  ( ( S e. { RR , CC } /\ 0 e. NN0 /\ N e. ( ZZ>= ` 0 ) ) -> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` 0 ) )
15 3 5 13 14 syl3anc 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> ( ( C^n ` S ) ` N ) C_ ( ( C^n ` S ) ` 0 ) )
16 simpr 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> F e. ( ( C^n ` S ) ` N ) )
17 15 16 sseldd 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> F e. ( ( C^n ` S ) ` 0 ) )
18 elcpn 
 |-  ( ( S C_ CC /\ 0 e. NN0 ) -> ( F e. ( ( C^n ` S ) ` 0 ) <-> ( F e. ( CC ^pm S ) /\ ( ( S Dn F ) ` 0 ) e. ( dom F -cn-> CC ) ) ) )
19 2 5 18 syl2anc 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> ( F e. ( ( C^n ` S ) ` 0 ) <-> ( F e. ( CC ^pm S ) /\ ( ( S Dn F ) ` 0 ) e. ( dom F -cn-> CC ) ) ) )
20 17 19 mpbid 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> ( F e. ( CC ^pm S ) /\ ( ( S Dn F ) ` 0 ) e. ( dom F -cn-> CC ) ) )
21 20 simpld 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> F e. ( CC ^pm S ) )
22 dvn0 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
23 2 21 22 syl2anc 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> ( ( S Dn F ) ` 0 ) = F )
24 20 simprd 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> ( ( S Dn F ) ` 0 ) e. ( dom F -cn-> CC ) )
25 23 24 eqeltrrd 
 |-  ( ( S e. { RR , CC } /\ F e. ( ( C^n ` S ) ` N ) ) -> F e. ( dom F -cn-> CC ) )