Metamath Proof Explorer


Theorem dvdsmulcr

Description: Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdsmulcr MNKK0MKNKMN

Proof

Step Hyp Ref Expression
1 zmulcl MKMK
2 1 3adant2 MNKMK
3 zmulcl NKNK
4 3 3adant1 MNKNK
5 2 4 jca MNKMKNK
6 5 3adant3r MNKK0MKNK
7 3simpa MNKK0MN
8 simpr MNKK0xx
9 zcn xx
10 zcn MM
11 9 10 anim12i xMxM
12 zcn NN
13 zcn KK
14 13 anim1i KK0KK0
15 mulass xMKx MK=xMK
16 15 3expa xMKx MK=xMK
17 16 adantrr xMKK0x MK=xMK
18 17 3adant2 xMNKK0x MK=xMK
19 18 eqeq1d xMNKK0x MK=NKxMK=NK
20 mulcl xMx M
21 mulcan2 x MNKK0x MK=NKx M=N
22 20 21 syl3an1 xMNKK0x MK=NKx M=N
23 19 22 bitr3d xMNKK0xMK=NKx M=N
24 11 12 14 23 syl3an xMNKK0xMK=NKx M=N
25 24 3expb xMNKK0xMK=NKx M=N
26 25 3impa xMNKK0xMK=NKx M=N
27 26 3coml MNKK0xxMK=NKx M=N
28 27 3expia MNKK0xxMK=NKx M=N
29 28 3impb MNKK0xxMK=NKx M=N
30 29 imp MNKK0xxMK=NKx M=N
31 30 biimpd MNKK0xxMK=NKx M=N
32 6 7 8 31 dvds1lem MNKK0MKNKMN
33 dvdsmulc MNKMNMKNK
34 33 3adant3r MNKK0MNMKNK
35 32 34 impbid MNKK0MKNKMN