Metamath Proof Explorer


Theorem lcmdvds

Description: The lcm of two integers divides any integer the two divide. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion lcmdvds KMNMKNKMlcmNK

Proof

Step Hyp Ref Expression
1 id 0K0K
2 breq1 M=0MK0K
3 2 adantl NM=0MK0K
4 oveq1 M=0MlcmN=0lcmN
5 0z 0
6 lcmcom 0N0lcmN=Nlcm0
7 5 6 mpan N0lcmN=Nlcm0
8 lcm0val NNlcm0=0
9 7 8 eqtrd N0lcmN=0
10 4 9 sylan9eqr NM=0MlcmN=0
11 10 breq1d NM=0MlcmNK0K
12 3 11 imbi12d NM=0MKMlcmNK0K0K
13 1 12 mpbiri NM=0MKMlcmNK
14 13 3ad2antl3 KMNM=0MKMlcmNK
15 14 adantrd KMNM=0MKNKMlcmNK
16 15 ex KMNM=0MKNKMlcmNK
17 breq1 N=0NK0K
18 17 adantl MN=0NK0K
19 oveq2 N=0MlcmN=Mlcm0
20 lcm0val MMlcm0=0
21 19 20 sylan9eqr MN=0MlcmN=0
22 21 breq1d MN=0MlcmNK0K
23 18 22 imbi12d MN=0NKMlcmNK0K0K
24 1 23 mpbiri MN=0NKMlcmNK
25 24 3ad2antl2 KMNN=0NKMlcmNK
26 25 adantld KMNN=0MKNKMlcmNK
27 26 ex KMNN=0MKNKMlcmNK
28 neanior M0N0¬M=0N=0
29 lcmcl MNMlcmN0
30 29 nn0zd MNMlcmN
31 dvds0 MlcmNMlcmN0
32 30 31 syl MNMlcmN0
33 32 a1d MNM0N0MlcmN0
34 33 adantr MNK=0M0N0MlcmN0
35 breq2 K=0MKM0
36 breq2 K=0NKN0
37 35 36 anbi12d K=0MKNKM0N0
38 breq2 K=0MlcmNKMlcmN0
39 37 38 imbi12d K=0MKNKMlcmNKM0N0MlcmN0
40 39 adantl MNK=0MKNKMlcmNKM0N0MlcmN0
41 34 40 mpbird MNK=0MKNKMlcmNK
42 41 adantrl MNKK=0MKNKMlcmNK
43 42 adantllr MM0NKK=0MKNKMlcmNK
44 43 adantlrr MM0NN0KK=0MKNKMlcmNK
45 44 anassrs MM0NN0KK=0MKNKMlcmNK
46 nnabscl MM0M
47 nnabscl NN0N
48 nnabscl KK0K
49 lcmgcdlem MNMlcmNMgcdN=MNKMKNKMlcmNK
50 49 simprd MNKMKNKMlcmNK
51 48 50 sylani MNKK0MKNKMlcmNK
52 46 47 51 syl2an MM0NN0KK0MKNKMlcmNK
53 52 expdimp MM0NN0KK0MKNKMlcmNK
54 dvdsabsb MKMKMK
55 zabscl KK
56 absdvdsb MKMKMK
57 55 56 sylan2 MKMKMK
58 54 57 bitrd MKMKMK
59 58 adantlr MNKMKMK
60 dvdsabsb NKNKNK
61 absdvdsb NKNKNK
62 55 61 sylan2 NKNKNK
63 60 62 bitrd NKNKNK
64 63 adantll MNKNKNK
65 59 64 anbi12d MNKMKNKMKNK
66 65 bicomd MNKMKNKMKNK
67 lcmabs MNMlcmN=MlcmN
68 67 breq1d MNMlcmNKMlcmNK
69 68 adantr MNKMlcmNKMlcmNK
70 dvdsabsb MlcmNKMlcmNKMlcmNK
71 30 70 sylan MNKMlcmNKMlcmNK
72 69 71 bitr4d MNKMlcmNKMlcmNK
73 66 72 imbi12d MNKMKNKMlcmNKMKNKMlcmNK
74 73 adantrr MNKK0MKNKMlcmNKMKNKMlcmNK
75 74 adantllr MM0NKK0MKNKMlcmNKMKNKMlcmNK
76 75 adantlrr MM0NN0KK0MKNKMlcmNKMKNKMlcmNK
77 53 76 mpbid MM0NN0KK0MKNKMlcmNK
78 77 anassrs MM0NN0KK0MKNKMlcmNK
79 45 78 pm2.61dane MM0NN0KMKNKMlcmNK
80 79 ex MM0NN0KMKNKMlcmNK
81 80 an4s MNM0N0KMKNKMlcmNK
82 28 81 sylan2br MN¬M=0N=0KMKNKMlcmNK
83 82 impancom MNK¬M=0N=0MKNKMlcmNK
84 83 3impa MNK¬M=0N=0MKNKMlcmNK
85 84 3comr KMN¬M=0N=0MKNKMlcmNK
86 16 27 85 ecase3d KMNMKNKMlcmNK