Metamath Proof Explorer


Theorem recdiv2

Description: Division into a reciprocal. (Contributed by NM, 19-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 ax-1cn
 |-  1 e. CC
2 divdiv1
 |-  ( ( 1 e. CC /\ ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )
3 1 2 mp3an1
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )