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 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M ∥ K ∧ N ∥ K → M lcm N ∥ K

Proof

Step Hyp Ref Expression
1 id ⊢ 0 ∥ K → 0 ∥ K
2 breq1 ⊢ M = 0 → M ∥ K ↔ 0 ∥ K
3 2 adantl ⊢ N ∈ ℤ ∧ M = 0 → M ∥ K ↔ 0 ∥ K
4 oveq1 ⊢ M = 0 → M lcm N = 0 lcm N
5 0z ⊢ 0 ∈ ℤ
6 lcmcom ⊢ 0 ∈ ℤ ∧ N ∈ ℤ → 0 lcm N = N lcm 0
7 5 6 mpan ⊢ N ∈ ℤ → 0 lcm N = N lcm 0
8 lcm0val ⊢ N ∈ ℤ → N lcm 0 = 0
9 7 8 eqtrd ⊢ N ∈ ℤ → 0 lcm N = 0
10 4 9 sylan9eqr ⊢ N ∈ ℤ ∧ M = 0 → M lcm N = 0
11 10 breq1d ⊢ N ∈ ℤ ∧ M = 0 → M lcm N ∥ K ↔ 0 ∥ K
12 3 11 imbi12d ⊢ N ∈ ℤ ∧ M = 0 → M ∥ K → M lcm N ∥ K ↔ 0 ∥ K → 0 ∥ K
13 1 12 mpbiri ⊢ N ∈ ℤ ∧ M = 0 → M ∥ K → M lcm N ∥ K
14 13 3ad2antl3 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 → M ∥ K → M lcm N ∥ K
15 14 adantrd ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
16 15 ex ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
17 breq1 ⊢ N = 0 → N ∥ K ↔ 0 ∥ K
18 17 adantl ⊢ M ∈ ℤ ∧ N = 0 → N ∥ K ↔ 0 ∥ K
19 oveq2 ⊢ N = 0 → M lcm N = M lcm 0
20 lcm0val ⊢ M ∈ ℤ → M lcm 0 = 0
21 19 20 sylan9eqr ⊢ M ∈ ℤ ∧ N = 0 → M lcm N = 0
22 21 breq1d ⊢ M ∈ ℤ ∧ N = 0 → M lcm N ∥ K ↔ 0 ∥ K
23 18 22 imbi12d ⊢ M ∈ ℤ ∧ N = 0 → N ∥ K → M lcm N ∥ K ↔ 0 ∥ K → 0 ∥ K
24 1 23 mpbiri ⊢ M ∈ ℤ ∧ N = 0 → N ∥ K → M lcm N ∥ K
25 24 3ad2antl2 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ N = 0 → N ∥ K → M lcm N ∥ K
26 25 adantld ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ N = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
27 26 ex ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → N = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
28 neanior ⊢ M ≠ 0 ∧ N ≠ 0 ↔ ¬ M = 0 ∨ N = 0
29 lcmcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N ∈ ℕ 0
30 29 nn0zd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N ∈ ℤ
31 dvds0 ⊢ M lcm N ∈ ℤ → M lcm N ∥ 0
32 30 31 syl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N ∥ 0
33 32 a1d ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ 0 ∧ N ∥ 0 → M lcm N ∥ 0
34 33 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K = 0 → M ∥ 0 ∧ N ∥ 0 → M lcm N ∥ 0
35 breq2 ⊢ K = 0 → M ∥ K ↔ M ∥ 0
36 breq2 ⊢ K = 0 → N ∥ K ↔ N ∥ 0
37 35 36 anbi12d ⊢ K = 0 → M ∥ K ∧ N ∥ K ↔ M ∥ 0 ∧ N ∥ 0
38 breq2 ⊢ K = 0 → M lcm N ∥ K ↔ M lcm N ∥ 0
39 37 38 imbi12d ⊢ K = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K ↔ M ∥ 0 ∧ N ∥ 0 → M lcm N ∥ 0
40 39 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K ↔ M ∥ 0 ∧ N ∥ 0 → M lcm N ∥ 0
41 34 40 mpbird ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
42 41 adantrl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ K = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
43 42 adantllr ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ K = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
44 43 adantlrr ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ N ≠ 0 ∧ K ∈ ℤ ∧ K = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
45 44 anassrs ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ N ≠ 0 ∧ K ∈ ℤ ∧ K = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
46 nnabscl ⊢ M ∈ ℤ ∧ M ≠ 0 → M ∈ ℕ
47 nnabscl ⊢ N ∈ ℤ ∧ N ≠ 0 → N ∈ ℕ
48 nnabscl ⊢ K ∈ ℤ ∧ K ≠ 0 → K ∈ ℕ
49 lcmgcdlem ⊢ M ∈ ℕ ∧ N ∈ ℕ → M lcm N ⁢ M gcd N = M ⁢ N ∧ K ∈ ℕ ∧ M ∥ K ∧ N ∥ K → M lcm N ∥ K
50 49 simprd ⊢ M ∈ ℕ ∧ N ∈ ℕ → K ∈ ℕ ∧ M ∥ K ∧ N ∥ K → M lcm N ∥ K
51 48 50 sylani ⊢ M ∈ ℕ ∧ N ∈ ℕ → K ∈ ℤ ∧ K ≠ 0 ∧ M ∥ K ∧ N ∥ K → M lcm N ∥ K
52 46 47 51 syl2an ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ N ≠ 0 → K ∈ ℤ ∧ K ≠ 0 ∧ M ∥ K ∧ N ∥ K → M lcm N ∥ K
53 52 expdimp ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ N ≠ 0 ∧ K ∈ ℤ ∧ K ≠ 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
54 dvdsabsb ⊢ M ∈ ℤ ∧ K ∈ ℤ → M ∥ K ↔ M ∥ K
55 zabscl ⊢ K ∈ ℤ → K ∈ ℤ
56 absdvdsb ⊢ M ∈ ℤ ∧ K ∈ ℤ → M ∥ K ↔ M ∥ K
57 55 56 sylan2 ⊢ M ∈ ℤ ∧ K ∈ ℤ → M ∥ K ↔ M ∥ K
58 54 57 bitrd ⊢ M ∈ ℤ ∧ K ∈ ℤ → M ∥ K ↔ M ∥ K
59 58 adantlr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M ∥ K ↔ M ∥ K
60 dvdsabsb ⊢ N ∈ ℤ ∧ K ∈ ℤ → N ∥ K ↔ N ∥ K
61 absdvdsb ⊢ N ∈ ℤ ∧ K ∈ ℤ → N ∥ K ↔ N ∥ K
62 55 61 sylan2 ⊢ N ∈ ℤ ∧ K ∈ ℤ → N ∥ K ↔ N ∥ K
63 60 62 bitrd ⊢ N ∈ ℤ ∧ K ∈ ℤ → N ∥ K ↔ N ∥ K
64 63 adantll ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → N ∥ K ↔ N ∥ K
65 59 64 anbi12d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M ∥ K ∧ N ∥ K ↔ M ∥ K ∧ N ∥ K
66 65 bicomd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M ∥ K ∧ N ∥ K ↔ M ∥ K ∧ N ∥ K
67 lcmabs ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = M lcm N
68 67 breq1d ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N ∥ K ↔ M lcm N ∥ K
69 68 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M lcm N ∥ K ↔ M lcm N ∥ K
70 dvdsabsb ⊢ M lcm N ∈ ℤ ∧ K ∈ ℤ → M lcm N ∥ K ↔ M lcm N ∥ K
71 30 70 sylan ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M lcm N ∥ K ↔ M lcm N ∥ K
72 69 71 bitr4d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M lcm N ∥ K ↔ M lcm N ∥ K
73 66 72 imbi12d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M ∥ K ∧ N ∥ K → M lcm N ∥ K ↔ M ∥ K ∧ N ∥ K → M lcm N ∥ K
74 73 adantrr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ K ≠ 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K ↔ M ∥ K ∧ N ∥ K → M lcm N ∥ K
75 74 adantllr ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ K ≠ 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K ↔ M ∥ K ∧ N ∥ K → M lcm N ∥ K
76 75 adantlrr ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ N ≠ 0 ∧ K ∈ ℤ ∧ K ≠ 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K ↔ M ∥ K ∧ N ∥ K → M lcm N ∥ K
77 53 76 mpbid ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ N ≠ 0 ∧ K ∈ ℤ ∧ K ≠ 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
78 77 anassrs ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ N ≠ 0 ∧ K ∈ ℤ ∧ K ≠ 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
79 45 78 pm2.61dane ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ N ≠ 0 ∧ K ∈ ℤ → M ∥ K ∧ N ∥ K → M lcm N ∥ K
80 79 ex ⊢ M ∈ ℤ ∧ M ≠ 0 ∧ N ∈ ℤ ∧ N ≠ 0 → K ∈ ℤ → M ∥ K ∧ N ∥ K → M lcm N ∥ K
81 80 an4s ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≠ 0 ∧ N ≠ 0 → K ∈ ℤ → M ∥ K ∧ N ∥ K → M lcm N ∥ K
82 28 81 sylan2br ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → K ∈ ℤ → M ∥ K ∧ N ∥ K → M lcm N ∥ K
83 82 impancom ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → ¬ M = 0 ∨ N = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
84 83 3impa ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → ¬ M = 0 ∨ N = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
85 84 3comr ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → ¬ M = 0 ∨ N = 0 → M ∥ K ∧ N ∥ K → M lcm N ∥ K
86 16 27 85 ecase3d ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M ∥ K ∧ N ∥ K → M lcm N ∥ K