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

Metamath Proof Explorer

Theorem divccn

Description: Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( J tX J ) Cn J )
12 11 a1i 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( J tX J ) Cn J ) )
13 oveq12 
 |-  ( ( u = x /\ v = ( 1 / A ) ) -> ( u x. v ) = ( x x. ( 1 / A ) ) )
14 7 8 10 7 7 12 13 cnmpt12 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( x x. ( 1 / A ) ) ) e. ( J Cn J ) )
15 5 14 eqeltrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( x / A ) ) e. ( J Cn J ) )