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

Metamath Proof Explorer

Theorem divccncf

Description: Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007)

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

Proof

Step Hyp Ref Expression
1 divccncf.1 
 |-  F = ( x e. CC |-> ( x / A ) )
2 divrec2 
 |-  ( ( x e. CC /\ A e. CC /\ A =/= 0 ) -> ( x / A ) = ( ( 1 / A ) x. x ) )
3 2 3expb 
 |-  ( ( x e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( x / A ) = ( ( 1 / A ) x. x ) )
4 3 ancoms 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ x e. CC ) -> ( x / A ) = ( ( 1 / A ) x. x ) )
5 4 mpteq2dva 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( x / A ) ) = ( x e. CC |-> ( ( 1 / A ) x. x ) ) )
6 1 5 eqtrid 
 |-  ( ( A e. CC /\ A =/= 0 ) -> F = ( x e. CC |-> ( ( 1 / A ) x. x ) ) )
7 reccl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
8 eqid 
 |-  ( x e. CC |-> ( ( 1 / A ) x. x ) ) = ( x e. CC |-> ( ( 1 / A ) x. x ) )
9 8 mulc1cncf 
 |-  ( ( 1 / A ) e. CC -> ( x e. CC |-> ( ( 1 / A ) x. x ) ) e. ( CC -cn-> CC ) )
10 7 9 syl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( x e. CC |-> ( ( 1 / A ) x. x ) ) e. ( CC -cn-> CC ) )
11 6 10 eqeltrd 
 |-  ( ( A e. CC /\ A =/= 0 ) -> F e. ( CC -cn-> CC ) )