This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid 
 |-  ( ( 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 ) )