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∥MlcmN∧N∥MlcmN

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→MlcmN=0lcmN
4 0z ⊢0∈ℤ
5 lcmcom ⊢N∈ℤ∧0∈ℤ→Nlcm0=0lcmN
6 4 5 mpan2 ⊢N∈ℤ→Nlcm0=0lcmN
7 lcm0val ⊢N∈ℤ→Nlcm0=0
8 6 7 eqtr3d ⊢N∈ℤ→0lcmN=0
9 3 8 sylan9eqr ⊢N∈ℤ∧M=0→MlcmN=0
10 9 adantll ⊢M∈ℤ∧N∈ℤ∧M=0→MlcmN=0
11 oveq2 ⊢N=0→MlcmN=Mlcm0
12 lcm0val ⊢M∈ℤ→Mlcm0=0
13 11 12 sylan9eqr ⊢M∈ℤ∧N=0→MlcmN=0
14 13 adantlr ⊢M∈ℤ∧N∈ℤ∧N=0→MlcmN=0
15 10 14 jaodan ⊢M∈ℤ∧N∈ℤ∧M=0∨N=0→MlcmN=0
16 2 15 breqtrrd ⊢M∈ℤ∧N∈ℤ∧M=0∨N=0→M∥MlcmN
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∥MlcmN
20 16 19 jca ⊢M∈ℤ∧N∈ℤ∧M=0∨N=0→M∥MlcmN∧N∥MlcmN
21 lcmcllem ⊢M∈ℤ∧N∈ℤ∧¬M=0∨N=0→MlcmN∈n∈ℕ|M∥n∧N∥n
22 lcmn0cl ⊢M∈ℤ∧N∈ℤ∧¬M=0∨N=0→MlcmN∈ℕ
23 breq2 ⊢n=MlcmN→M∥n↔M∥MlcmN
24 breq2 ⊢n=MlcmN→N∥n↔N∥MlcmN
25 23 24 anbi12d ⊢n=MlcmN→M∥n∧N∥n↔M∥MlcmN∧N∥MlcmN
26 25 elrab3 ⊢MlcmN∈ℕ→MlcmN∈n∈ℕ|M∥n∧N∥n↔M∥MlcmN∧N∥MlcmN
27 22 26 syl ⊢M∈ℤ∧N∈ℤ∧¬M=0∨N=0→MlcmN∈n∈ℕ|M∥n∧N∥n↔M∥MlcmN∧N∥MlcmN
28 21 27 mpbid ⊢M∈ℤ∧N∈ℤ∧¬M=0∨N=0→M∥MlcmN∧N∥MlcmN
29 20 28 pm2.61dan ⊢M∈ℤ∧N∈ℤ→M∥MlcmN∧N∥MlcmN