Metamath Proof Explorer

Theorem divcan6

Description: Cancellation of inverted fractions. (Contributed by NM, 28-Dec-2007)

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

Proof

Step Hyp Ref Expression
1 recdiv 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( 1 / ( A / B ) ) = ( B / A ) )
2 1 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) x. ( 1 / ( A / B ) ) ) = ( ( A / B ) x. ( B / A ) ) )
3 divcl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
4 3 3expb 
 |-  ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) e. CC )
5 4 adantlr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) e. CC )
6 divne0 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / B ) =/= 0 )
7 recid 
 |-  ( ( ( A / B ) e. CC /\ ( A / B ) =/= 0 ) -> ( ( A / B ) x. ( 1 / ( A / B ) ) ) = 1 )
8 5 6 7 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) x. ( 1 / ( A / B ) ) ) = 1 )
9 2 8 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) x. ( B / A ) ) = 1 )