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