Metamath Proof Explorer

Theorem divccn

Description: Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014)

Ref Expression
Hypothesis expcn.j 
|- J = ( TopOpen ` CCfld )
Assertion divccn 
|- ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( x / A ) ) e. ( J Cn J ) )

Proof

Step Hyp Ref Expression
1 expcn.j 
 |-  J = ( TopOpen ` CCfld )
2 divrec 
 |-  ( ( x e. CC /\ A e. CC /\ A =/= 0 ) -> ( x / A ) = ( x x. ( 1 / A ) ) )
3 2 3expb 
 |-  ( ( x e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( x / A ) = ( x x. ( 1 / A ) ) )
4 3 ancoms 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ x e. CC ) -> ( x / A ) = ( x x. ( 1 / A ) ) )
5 4 mpteq2dva 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( x / A ) ) = ( x e. CC |-> ( x x. ( 1 / A ) ) ) )
6 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
7 6 a1i 
 |-  ( ( A e. CC /\ A =/= 0 ) -> J e. ( TopOn ` CC ) )
8 7 cnmptid 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> x ) e. ( J Cn J ) )
9 reccl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
10 7 7 9 cnmptc 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( 1 / A ) ) e. ( J Cn J ) )
11 1 mulcn 
 |-  x. e. ( ( J tX J ) Cn J )
12 11 a1i 
 |-  ( ( A e. CC /\ A =/= 0 ) -> x. e. ( ( J tX J ) Cn J ) )
13 7 8 10 12 cnmpt12f 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( x x. ( 1 / A ) ) ) e. ( J Cn J ) )
14 5 13 eqeltrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( x / A ) ) e. ( J Cn J ) )