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 ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โ†’ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†” ๐ต = ๐ถ ) )

Proof

Step Hyp Ref Expression
1 mulclpi โŠข ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โ†’ ( ๐ด ยทN ๐ต ) โˆˆ N )
2 eleq1 โŠข ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†’ ( ( ๐ด ยทN ๐ต ) โˆˆ N โ†” ( ๐ด ยทN ๐ถ ) โˆˆ N ) )
3 1 2 syl5ib โŠข ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†’ ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โ†’ ( ๐ด ยทN ๐ถ ) โˆˆ N ) )
4 3 imp โŠข ( ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โˆง ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) ) โ†’ ( ๐ด ยทN ๐ถ ) โˆˆ N )
5 dmmulpi โŠข dom ยทN = ( N ร— N )
6 0npi โŠข ยฌ โˆ… โˆˆ N
7 5 6 ndmovrcl โŠข ( ( ๐ด ยทN ๐ถ ) โˆˆ N โ†’ ( ๐ด โˆˆ N โˆง ๐ถ โˆˆ N ) )
8 simpr โŠข ( ( ๐ด โˆˆ N โˆง ๐ถ โˆˆ N ) โ†’ ๐ถ โˆˆ N )
9 4 7 8 3syl โŠข ( ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โˆง ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) ) โ†’ ๐ถ โˆˆ N )
10 mulpiord โŠข ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โ†’ ( ๐ด ยทN ๐ต ) = ( ๐ด ยทo ๐ต ) )
11 10 adantr โŠข ( ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โˆง ๐ถ โˆˆ N ) โ†’ ( ๐ด ยทN ๐ต ) = ( ๐ด ยทo ๐ต ) )
12 mulpiord โŠข ( ( ๐ด โˆˆ N โˆง ๐ถ โˆˆ N ) โ†’ ( ๐ด ยทN ๐ถ ) = ( ๐ด ยทo ๐ถ ) )
13 12 adantlr โŠข ( ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โˆง ๐ถ โˆˆ N ) โ†’ ( ๐ด ยทN ๐ถ ) = ( ๐ด ยทo ๐ถ ) )
14 11 13 eqeq12d โŠข ( ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โˆง ๐ถ โˆˆ N ) โ†’ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†” ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) ) )
15 pinn โŠข ( ๐ด โˆˆ N โ†’ ๐ด โˆˆ ฯ‰ )
16 pinn โŠข ( ๐ต โˆˆ N โ†’ ๐ต โˆˆ ฯ‰ )
17 pinn โŠข ( ๐ถ โˆˆ N โ†’ ๐ถ โˆˆ ฯ‰ )
18 elni2 โŠข ( ๐ด โˆˆ N โ†” ( ๐ด โˆˆ ฯ‰ โˆง โˆ… โˆˆ ๐ด ) )
19 18 simprbi โŠข ( ๐ด โˆˆ N โ†’ โˆ… โˆˆ ๐ด )
20 nnmcan โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ†” ๐ต = ๐ถ ) )
21 20 biimpd โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง โˆ… โˆˆ ๐ด ) โ†’ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ†’ ๐ต = ๐ถ ) )
22 19 21 sylan2 โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โˆง ๐ด โˆˆ N ) โ†’ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ†’ ๐ต = ๐ถ ) )
23 22 ex โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ โˆˆ ฯ‰ ) โ†’ ( ๐ด โˆˆ N โ†’ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ†’ ๐ต = ๐ถ ) ) )
24 15 16 17 23 syl3an โŠข ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N โˆง ๐ถ โˆˆ N ) โ†’ ( ๐ด โˆˆ N โ†’ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ†’ ๐ต = ๐ถ ) ) )
25 24 3exp โŠข ( ๐ด โˆˆ N โ†’ ( ๐ต โˆˆ N โ†’ ( ๐ถ โˆˆ N โ†’ ( ๐ด โˆˆ N โ†’ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ†’ ๐ต = ๐ถ ) ) ) ) )
26 25 com4r โŠข ( ๐ด โˆˆ N โ†’ ( ๐ด โˆˆ N โ†’ ( ๐ต โˆˆ N โ†’ ( ๐ถ โˆˆ N โ†’ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ†’ ๐ต = ๐ถ ) ) ) ) )
27 26 pm2.43i โŠข ( ๐ด โˆˆ N โ†’ ( ๐ต โˆˆ N โ†’ ( ๐ถ โˆˆ N โ†’ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ†’ ๐ต = ๐ถ ) ) ) )
28 27 imp31 โŠข ( ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โˆง ๐ถ โˆˆ N ) โ†’ ( ( ๐ด ยทo ๐ต ) = ( ๐ด ยทo ๐ถ ) โ†’ ๐ต = ๐ถ ) )
29 14 28 sylbid โŠข ( ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โˆง ๐ถ โˆˆ N ) โ†’ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†’ ๐ต = ๐ถ ) )
30 9 29 sylan2 โŠข ( ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โˆง ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โˆง ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) ) ) โ†’ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†’ ๐ต = ๐ถ ) )
31 30 exp32 โŠข ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โ†’ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†’ ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โ†’ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†’ ๐ต = ๐ถ ) ) ) )
32 31 imp4b โŠข ( ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โˆง ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) ) โ†’ ( ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โˆง ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) ) โ†’ ๐ต = ๐ถ ) )
33 32 pm2.43i โŠข ( ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โˆง ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) ) โ†’ ๐ต = ๐ถ )
34 33 ex โŠข ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โ†’ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†’ ๐ต = ๐ถ ) )
35 oveq2 โŠข ( ๐ต = ๐ถ โ†’ ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) )
36 34 35 impbid1 โŠข ( ( ๐ด โˆˆ N โˆง ๐ต โˆˆ N ) โ†’ ( ( ๐ด ยทN ๐ต ) = ( ๐ด ยทN ๐ถ ) โ†” ๐ต = ๐ถ ) )