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