Metamath Proof Explorer


Theorem mulcanpi

Description: Multiplication cancellation law for positive integers. (Contributed by NM, 4-Feb-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulcanpi
|- ( ( A e. N. /\ B e. N. ) -> ( ( A .N B ) = ( A .N C ) <-> B = C ) )

Proof

Step Hyp Ref Expression
1 mulclpi
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .N B ) e. N. )
2 eleq1
 |-  ( ( A .N B ) = ( A .N C ) -> ( ( A .N B ) e. N. <-> ( A .N C ) e. N. ) )
3 1 2 syl5ib
 |-  ( ( A .N B ) = ( A .N C ) -> ( ( A e. N. /\ B e. N. ) -> ( A .N C ) e. N. ) )
4 3 imp
 |-  ( ( ( A .N B ) = ( A .N C ) /\ ( A e. N. /\ B e. N. ) ) -> ( A .N C ) e. N. )
5 dmmulpi
 |-  dom .N = ( N. X. N. )
6 0npi
 |-  -. (/) e. N.
7 5 6 ndmovrcl
 |-  ( ( A .N C ) e. N. -> ( A e. N. /\ C e. N. ) )
8 simpr
 |-  ( ( A e. N. /\ C e. N. ) -> C e. N. )
9 4 7 8 3syl
 |-  ( ( ( A .N B ) = ( A .N C ) /\ ( A e. N. /\ B e. N. ) ) -> C e. N. )
10 mulpiord
 |-  ( ( A e. N. /\ B e. N. ) -> ( A .N B ) = ( A .o B ) )
11 10 adantr
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A .N B ) = ( A .o B ) )
12 mulpiord
 |-  ( ( A e. N. /\ C e. N. ) -> ( A .N C ) = ( A .o C ) )
13 12 adantlr
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( A .N C ) = ( A .o C ) )
14 11 13 eqeq12d
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( A .N B ) = ( A .N C ) <-> ( A .o B ) = ( A .o C ) ) )
15 pinn
 |-  ( A e. N. -> A e. _om )
16 pinn
 |-  ( B e. N. -> B e. _om )
17 pinn
 |-  ( C e. N. -> C e. _om )
18 elni2
 |-  ( A e. N. <-> ( A e. _om /\ (/) e. A ) )
19 18 simprbi
 |-  ( A e. N. -> (/) e. A )
20 nnmcan
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )
21 20 biimpd
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) -> B = C ) )
22 19 21 sylan2
 |-  ( ( ( A e. _om /\ B e. _om /\ C e. _om ) /\ A e. N. ) -> ( ( A .o B ) = ( A .o C ) -> B = C ) )
23 22 ex
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( A e. N. -> ( ( A .o B ) = ( A .o C ) -> B = C ) ) )
24 15 16 17 23 syl3an
 |-  ( ( A e. N. /\ B e. N. /\ C e. N. ) -> ( A e. N. -> ( ( A .o B ) = ( A .o C ) -> B = C ) ) )
25 24 3exp
 |-  ( A e. N. -> ( B e. N. -> ( C e. N. -> ( A e. N. -> ( ( A .o B ) = ( A .o C ) -> B = C ) ) ) ) )
26 25 com4r
 |-  ( A e. N. -> ( A e. N. -> ( B e. N. -> ( C e. N. -> ( ( A .o B ) = ( A .o C ) -> B = C ) ) ) ) )
27 26 pm2.43i
 |-  ( A e. N. -> ( B e. N. -> ( C e. N. -> ( ( A .o B ) = ( A .o C ) -> B = C ) ) ) )
28 27 imp31
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( A .o B ) = ( A .o C ) -> B = C ) )
29 14 28 sylbid
 |-  ( ( ( A e. N. /\ B e. N. ) /\ C e. N. ) -> ( ( A .N B ) = ( A .N C ) -> B = C ) )
30 9 29 sylan2
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( ( A .N B ) = ( A .N C ) /\ ( A e. N. /\ B e. N. ) ) ) -> ( ( A .N B ) = ( A .N C ) -> B = C ) )
31 30 exp32
 |-  ( ( A e. N. /\ B e. N. ) -> ( ( A .N B ) = ( A .N C ) -> ( ( A e. N. /\ B e. N. ) -> ( ( A .N B ) = ( A .N C ) -> B = C ) ) ) )
32 31 imp4b
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( A .N B ) = ( A .N C ) ) -> ( ( ( A e. N. /\ B e. N. ) /\ ( A .N B ) = ( A .N C ) ) -> B = C ) )
33 32 pm2.43i
 |-  ( ( ( A e. N. /\ B e. N. ) /\ ( A .N B ) = ( A .N C ) ) -> B = C )
34 33 ex
 |-  ( ( A e. N. /\ B e. N. ) -> ( ( A .N B ) = ( A .N C ) -> B = C ) )
35 oveq2
 |-  ( B = C -> ( A .N B ) = ( A .N C ) )
36 34 35 impbid1
 |-  ( ( A e. N. /\ B e. N. ) -> ( ( A .N B ) = ( A .N C ) <-> B = C ) )