Theorem divrec2

Description: Relationship between division and reciprocal. (Contributed by NM, 7-Feb-2006)

	Ref	Expression
Assertion	divrec2	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( ( 1 / B ) x. A ) )

Proof

Step	Hyp	Ref	Expression
1		divrec	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( A x. ( 1 / B ) ) )
2		simp1	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> A e. CC )
3		reccl	|- ( ( B e. CC /\ B =/= 0 ) -> ( 1 / B ) e. CC )
4	3	3adant1	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( 1 / B ) e. CC )
5	2 4	mulcomd	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A x. ( 1 / B ) ) = ( ( 1 / B ) x. A ) )
6	1 5	eqtrd	|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) = ( ( 1 / B ) x. A ) )