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

Metamath Proof Explorer

Theorem divccnOLD

Description: Obsolete version of divccn as of 6-Apr-2025. (Contributed by Mario Carneiro, 5-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 expcnOLD.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 ) )