Metamath Proof Explorer

Theorem nnmcan

Description: Cancellation law for multiplication of natural numbers. (Contributed by NM, 26-Oct-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnmcan 
|- ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )

Proof

Step Hyp Ref Expression
1 3anrot 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) <-> ( B e. _om /\ C e. _om /\ A e. _om ) )
2 nnmword 
 |-  ( ( ( B e. _om /\ C e. _om /\ A e. _om ) /\ (/) e. A ) -> ( B C_ C <-> ( A .o B ) C_ ( A .o C ) ) )
3 1 2 sylanb 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. A ) -> ( B C_ C <-> ( A .o B ) C_ ( A .o C ) ) )
4 3anrev 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) <-> ( C e. _om /\ B e. _om /\ A e. _om ) )
5 nnmword 
 |-  ( ( ( C e. _om /\ B e. _om /\ A e. _om ) /\ (/) e. A ) -> ( C C_ B <-> ( A .o C ) C_ ( A .o B ) ) )
6 4 5 sylanb 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. A ) -> ( C C_ B <-> ( A .o C ) C_ ( A .o B ) ) )
7 3 6 anbi12d 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. A ) -> ( ( B C_ C /\ C C_ B ) <-> ( ( A .o B ) C_ ( A .o C ) /\ ( A .o C ) C_ ( A .o B ) ) ) )
8 7 bicomd 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. A ) -> ( ( ( A .o B ) C_ ( A .o C ) /\ ( A .o C ) C_ ( A .o B ) ) <-> ( B C_ C /\ C C_ B ) ) )
9 eqss 
 |-  ( ( A .o B ) = ( A .o C ) <-> ( ( A .o B ) C_ ( A .o C ) /\ ( A .o C ) C_ ( A .o B ) ) )
10 eqss 
 |-  ( B = C <-> ( B C_ C /\ C C_ B ) )
11 8 9 10 3bitr4g 
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )