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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( abs ‘ ( 𝑀 · 𝑁 ) ) )

Proof

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 ‘ ( 𝑀 · 𝑁 ) ) )