Metamath Proof Explorer

Theorem dvdslcm

Description: The lcm of two integers is divisible by each of them. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion dvdslcm ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M lcm N ∧ N ∥ M lcm N

Proof

Step Hyp Ref Expression
1 dvds0 ⊢ M ∈ ℤ → M ∥ 0
2 1 ad2antrr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 ∨ N = 0 → M ∥ 0
3 oveq1 ⊢ M = 0 → M lcm N = 0 lcm N
4 0z ⊢ 0 ∈ ℤ
5 lcmcom ⊢ N ∈ ℤ ∧ 0 ∈ ℤ → N lcm 0 = 0 lcm N
6 4 5 mpan2 ⊢ N ∈ ℤ → N lcm 0 = 0 lcm N
7 lcm0val ⊢ N ∈ ℤ → N lcm 0 = 0
8 6 7 eqtr3d ⊢ N ∈ ℤ → 0 lcm N = 0
9 3 8 sylan9eqr ⊢ N ∈ ℤ ∧ M = 0 → M lcm N = 0
10 9 adantll ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 → M lcm N = 0
11 oveq2 ⊢ N = 0 → M lcm N = M lcm 0
12 lcm0val ⊢ M ∈ ℤ → M lcm 0 = 0
13 11 12 sylan9eqr ⊢ M ∈ ℤ ∧ N = 0 → M lcm N = 0
14 13 adantlr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ N = 0 → M lcm N = 0
15 10 14 jaodan ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 ∨ N = 0 → M lcm N = 0
16 2 15 breqtrrd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 ∨ N = 0 → M ∥ M lcm N
17 dvds0 ⊢ N ∈ ℤ → N ∥ 0
18 17 ad2antlr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 ∨ N = 0 → N ∥ 0
19 18 15 breqtrrd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 ∨ N = 0 → N ∥ M lcm N
20 16 19 jca ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 ∨ N = 0 → M ∥ M lcm N ∧ N ∥ M lcm N
21 lcmcllem ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N ∈ n ∈ ℕ | M ∥ n ∧ N ∥ n
22 lcmn0cl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N ∈ ℕ
23 breq2 ⊢ n = M lcm N → M ∥ n ↔ M ∥ M lcm N
24 breq2 ⊢ n = M lcm N → N ∥ n ↔ N ∥ M lcm N
25 23 24 anbi12d ⊢ n = M lcm N → M ∥ n ∧ N ∥ n ↔ M ∥ M lcm N ∧ N ∥ M lcm N
26 25 elrab3 ⊢ M lcm N ∈ ℕ → M lcm N ∈ n ∈ ℕ | M ∥ n ∧ N ∥ n ↔ M ∥ M lcm N ∧ N ∥ M lcm N
27 22 26 syl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N ∈ n ∈ ℕ | M ∥ n ∧ N ∥ n ↔ M ∥ M lcm N ∧ N ∥ M lcm N
28 21 27 mpbid ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ M lcm N ∧ N ∥ M lcm N
29 20 28 pm2.61dan ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ∥ M lcm N ∧ N ∥ M lcm N