Metamath Proof Explorer

Theorem mulcan2g

Description: A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013)

Ref Expression
Assertion mulcan2g 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. C ) = ( B x. C ) <-> ( A = B \/ C = 0 ) ) )

Proof

Step Hyp Ref Expression
1 mulcom 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
2 1 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. C ) = ( C x. A ) )
3 mulcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
4 3 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
5 2 4 eqeq12d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. C ) = ( B x. C ) <-> ( C x. A ) = ( C x. B ) ) )
6 mulcan1g 
 |-  ( ( C e. CC /\ A e. CC /\ B e. CC ) -> ( ( C x. A ) = ( C x. B ) <-> ( C = 0 \/ A = B ) ) )
7 6 3coml 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( C x. A ) = ( C x. B ) <-> ( C = 0 \/ A = B ) ) )
8 orcom 
 |-  ( ( C = 0 \/ A = B ) <-> ( A = B \/ C = 0 ) )
9 7 8 bitrdi 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( C x. A ) = ( C x. B ) <-> ( A = B \/ C = 0 ) ) )
10 5 9 bitrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. C ) = ( B x. C ) <-> ( A = B \/ C = 0 ) ) )