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 ) )