Metamath Proof Explorer


Theorem dvdscmulr

Description: Cancellation law for the divides relation. Theorem 1.1(e) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdscmulr MNKK0K MK NMN

Proof

Step Hyp Ref Expression
1 zmulcl KMK M
2 1 3adant3 KMNK M
3 zmulcl KNK N
4 3 3adant2 KMNK N
5 2 4 jca KMNK MK N
6 5 3coml MNKK MK N
7 6 3adant3r MNKK0K MK N
8 3simpa MNKK0MN
9 simpr MNKK0xx
10 zcn xx
11 zcn MM
12 10 11 anim12i xMxM
13 zcn NN
14 zcn KK
15 14 anim1i KK0KK0
16 mul12 KxMKx M=xK M
17 16 3adant1r KK0xMKx M=xK M
18 17 3expb KK0xMKx M=xK M
19 18 ancoms xMKK0Kx M=xK M
20 19 3adant2 xMNKK0Kx M=xK M
21 20 eqeq1d xMNKK0Kx M=K NxK M=K N
22 mulcl xMx M
23 mulcan x MNKK0Kx M=K Nx M=N
24 22 23 syl3an1 xMNKK0Kx M=K Nx M=N
25 21 24 bitr3d xMNKK0xK M=K Nx M=N
26 12 13 15 25 syl3an xMNKK0xK M=K Nx M=N
27 26 3expb xMNKK0xK M=K Nx M=N
28 27 3impa xMNKK0xK M=K Nx M=N
29 28 3coml MNKK0xxK M=K Nx M=N
30 29 3expia MNKK0xxK M=K Nx M=N
31 30 3impb MNKK0xxK M=K Nx M=N
32 31 imp MNKK0xxK M=K Nx M=N
33 32 biimpd MNKK0xxK M=K Nx M=N
34 7 8 9 33 dvds1lem MNKK0K MK NMN
35 dvdscmul MNKMNK MK N
36 35 3adant3r MNKK0MNK MK N
37 34 36 impbid MNKK0K MK NMN