Metamath Proof Explorer

Theorem cdivcncf

Description: Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypothesis cdivcncf.1 
|- F = ( x e. ( CC \ { 0 } ) |-> ( A / x ) )
Assertion cdivcncf 
|- ( A e. CC -> F e. ( ( CC \ { 0 } ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 cdivcncf.1 
 |-  F = ( x e. ( CC \ { 0 } ) |-> ( A / x ) )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
4 3 a1i 
 |-  ( A e. CC -> ( TopOpen ` CCfld ) e. ( TopOn ` CC ) )
5 difss 
 |-  ( CC \ { 0 } ) C_ CC
6 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( CC \ { 0 } ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) )
7 4 5 6 sylancl 
 |-  ( A e. CC -> ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) )
8 id 
 |-  ( A e. CC -> A e. CC )
9 7 4 8 cnmptc 
 |-  ( A e. CC -> ( x e. ( CC \ { 0 } ) |-> A ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) )
10 7 cnmptid 
 |-  ( A e. CC -> ( x e. ( CC \ { 0 } ) |-> x ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) )
11 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) )
12 2 11 divcn 
 |-  / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) )
13 12 a1i 
 |-  ( A e. CC -> / e. ( ( ( TopOpen ` CCfld ) tX ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) ) Cn ( TopOpen ` CCfld ) ) )
14 7 9 10 13 cnmpt12f 
 |-  ( A e. CC -> ( x e. ( CC \ { 0 } ) |-> ( A / x ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) )
15 ssid 
 |-  CC C_ CC
16 3 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
17 2 11 16 cncfcn 
 |-  ( ( ( CC \ { 0 } ) C_ CC /\ CC C_ CC ) -> ( ( CC \ { 0 } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) )
18 5 15 17 mp2an 
 |-  ( ( CC \ { 0 } ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( CC \ { 0 } ) ) Cn ( TopOpen ` CCfld ) )
19 14 1 18 3eltr4g 
 |-  ( A e. CC -> F e. ( ( CC \ { 0 } ) -cn-> CC ) )