Metamath Proof Explorer


Theorem mulcan2d

Description: Cancellation law for multiplication. Theorem I.7 of Apostol p. 18. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses mulcand.1
|- ( ph -> A e. CC )
mulcand.2
|- ( ph -> B e. CC )
mulcand.3
|- ( ph -> C e. CC )
mulcand.4
|- ( ph -> C =/= 0 )
Assertion mulcan2d
|- ( ph -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 mulcand.1
 |-  ( ph -> A e. CC )
2 mulcand.2
 |-  ( ph -> B e. CC )
3 mulcand.3
 |-  ( ph -> C e. CC )
4 mulcand.4
 |-  ( ph -> C =/= 0 )
5 1 3 mulcomd
 |-  ( ph -> ( A x. C ) = ( C x. A ) )
6 2 3 mulcomd
 |-  ( ph -> ( B x. C ) = ( C x. B ) )
7 5 6 eqeq12d
 |-  ( ph -> ( ( A x. C ) = ( B x. C ) <-> ( C x. A ) = ( C x. B ) ) )
8 1 2 3 4 mulcand
 |-  ( ph -> ( ( C x. A ) = ( C x. B ) <-> A = B ) )
9 7 8 bitrd
 |-  ( ph -> ( ( A x. C ) = ( B x. C ) <-> A = B ) )