Metamath Proof Explorer

Theorem lcmgcd

Description: The product of two numbers' least common multiple and greatest common divisor is the absolute value of the product of the two numbers. In particular, that absolute valueis the least common multiple of two coprime numbers, for which ( M gcd N ) = 1 .

Multiple methods exist for proving this, and it is often proven either as a consequence of the fundamental theorem of arithmetic 1arith or of Bézout's identity bezout ; see e.g., https://proofwiki.org/wiki/Product_of_GCD_and_LCM and https://math.stackexchange.com/a/470827 . This proof uses the latter to first confirm it for positive integers M and N (the "Second Proof" in the above Stack Exchange page), then shows that implies it for all nonzero integer inputs, then finally uses lcm0val to show it applies when either or both inputs are zero. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion lcmgcd ⊢M∈ℤ∧N∈ℤ→MlcmN⁢MgcdN= M⋅ N

Proof

Step Hyp Ref Expression
1 gcdcl ⊢M∈ℤ∧N∈ℤ→MgcdN∈ℕ0
2 1 nn0cnd ⊢M∈ℤ∧N∈ℤ→MgcdN∈ℂ
3 2 mul02d ⊢M∈ℤ∧N∈ℤ→0⋅MgcdN=0
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 8 adantl ⊢M∈ℤ∧N∈ℤ→0lcmN=0
10 9 oveq1d ⊢M∈ℤ∧N∈ℤ→0lcmN⁢MgcdN=0⋅MgcdN
11 zcn ⊢N∈ℤ→N∈ℂ
12 11 adantl ⊢M∈ℤ∧N∈ℤ→N∈ℂ
13 12 mul02d ⊢M∈ℤ∧N∈ℤ→0⋅ N=0
14 13 abs00bd ⊢M∈ℤ∧N∈ℤ→0⋅ N=0
15 3 10 14 3eqtr4d ⊢M∈ℤ∧N∈ℤ→0lcmN⁢MgcdN=0⋅ N
16 15 adantr ⊢M∈ℤ∧N∈ℤ∧M=0→0lcmN⁢MgcdN=0⋅ N
17 simpr ⊢M∈ℤ∧N∈ℤ∧M=0→M=0
18 17 oveq1d ⊢M∈ℤ∧N∈ℤ∧M=0→MlcmN=0lcmN
19 18 oveq1d ⊢M∈ℤ∧N∈ℤ∧M=0→MlcmN⁢MgcdN=0lcmN⁢MgcdN
20 17 oveq1d ⊢M∈ℤ∧N∈ℤ∧M=0→ M⋅ N=0⋅ N
21 20 fveq2d ⊢M∈ℤ∧N∈ℤ∧M=0→ M⋅ N=0⋅ N
22 16 19 21 3eqtr4d ⊢M∈ℤ∧N∈ℤ∧M=0→MlcmN⁢MgcdN= M⋅ N
23 lcm0val ⊢M∈ℤ→Mlcm0=0
24 23 adantr ⊢M∈ℤ∧N∈ℤ→Mlcm0=0
25 24 oveq1d ⊢M∈ℤ∧N∈ℤ→Mlcm0⁢MgcdN=0⋅MgcdN
26 zcn ⊢M∈ℤ→M∈ℂ
27 26 adantr ⊢M∈ℤ∧N∈ℤ→M∈ℂ
28 27 mul01d ⊢M∈ℤ∧N∈ℤ→ M⋅0=0
29 28 abs00bd ⊢M∈ℤ∧N∈ℤ→ M⋅0=0
30 3 25 29 3eqtr4d ⊢M∈ℤ∧N∈ℤ→Mlcm0⁢MgcdN= M⋅0
31 30 adantr ⊢M∈ℤ∧N∈ℤ∧N=0→Mlcm0⁢MgcdN= M⋅0
32 simpr ⊢M∈ℤ∧N∈ℤ∧N=0→N=0
33 32 oveq2d ⊢M∈ℤ∧N∈ℤ∧N=0→MlcmN=Mlcm0
34 33 oveq1d ⊢M∈ℤ∧N∈ℤ∧N=0→MlcmN⁢MgcdN=Mlcm0⁢MgcdN
35 32 oveq2d ⊢M∈ℤ∧N∈ℤ∧N=0→ M⋅ N= M⋅0
36 35 fveq2d ⊢M∈ℤ∧N∈ℤ∧N=0→ M⋅ N= M⋅0
37 31 34 36 3eqtr4d ⊢M∈ℤ∧N∈ℤ∧N=0→MlcmN⁢MgcdN= M⋅ N
38 22 37 jaodan ⊢M∈ℤ∧N∈ℤ∧M=0∨N=0→MlcmN⁢MgcdN= M⋅ N
39 neanior ⊢M≠0∧N≠0↔¬M=0∨N=0
40 nnabscl ⊢M∈ℤ∧M≠0→M∈ℕ
41 nnabscl ⊢N∈ℤ∧N≠0→N∈ℕ
42 40 41 anim12i ⊢M∈ℤ∧M≠0∧N∈ℤ∧N≠0→M∈ℕ∧N∈ℕ
43 42 an4s ⊢M∈ℤ∧N∈ℤ∧M≠0∧N≠0→M∈ℕ∧N∈ℕ
44 39 43 sylan2br ⊢M∈ℤ∧N∈ℤ∧¬M=0∨N=0→M∈ℕ∧N∈ℕ
45 lcmgcdlem ⊢M∈ℕ∧N∈ℕ→MlcmN⁢MgcdN=M⁢N∧0∈ℕ∧M∥0∧N∥0→MlcmN∥0
46 45 simpld ⊢M∈ℕ∧N∈ℕ→MlcmN⁢MgcdN=M⁢N
47 44 46 syl ⊢M∈ℤ∧N∈ℤ∧¬M=0∨N=0→MlcmN⁢MgcdN=M⁢N
48 lcmabs ⊢M∈ℤ∧N∈ℤ→MlcmN=MlcmN
49 gcdabs ⊢M∈ℤ∧N∈ℤ→MgcdN=MgcdN
50 48 49 oveq12d ⊢M∈ℤ∧N∈ℤ→MlcmN⁢MgcdN=MlcmN⁢MgcdN
51 50 adantr ⊢M∈ℤ∧N∈ℤ∧¬M=0∨N=0→MlcmN⁢MgcdN=MlcmN⁢MgcdN
52 absidm ⊢M∈ℂ→M=M
53 absidm ⊢N∈ℂ→N=N
54 52 53 oveqan12d ⊢M∈ℂ∧N∈ℂ→M⁢N=M⁢N
55 26 11 54 syl2an ⊢M∈ℤ∧N∈ℤ→M⁢N=M⁢N
56 nn0abscl ⊢M∈ℤ→M∈ℕ0
57 56 nn0cnd ⊢M∈ℤ→M∈ℂ
58 57 adantr ⊢M∈ℤ∧N∈ℤ→M∈ℂ
59 nn0abscl ⊢N∈ℤ→N∈ℕ0
60 59 nn0cnd ⊢N∈ℤ→N∈ℂ
61 60 adantl ⊢M∈ℤ∧N∈ℤ→N∈ℂ
62 58 61 absmuld ⊢M∈ℤ∧N∈ℤ→M⁢N=M⁢N
63 27 12 absmuld ⊢M∈ℤ∧N∈ℤ→ M⋅ N=M⁢N
64 55 62 63 3eqtr4d ⊢M∈ℤ∧N∈ℤ→M⁢N= M⋅ N
65 64 adantr ⊢M∈ℤ∧N∈ℤ∧¬M=0∨N=0→M⁢N= M⋅ N
66 47 51 65 3eqtr3d ⊢M∈ℤ∧N∈ℤ∧¬M=0∨N=0→MlcmN⁢MgcdN= M⋅ N
67 38 66 pm2.61dan ⊢M∈ℤ∧N∈ℤ→MlcmN⁢MgcdN= M⋅ N