Theorem 3lcm2e6

Description: The least common multiple of three and two is six. The operands are unequal primes and thus coprime, so the result is (the absolute value of) their product. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 27-Aug-2020)

	Ref	Expression
Assertion	3lcm2e6	⊢ ( 3 lcm 2 ) = 6

Proof

Step	Hyp	Ref	Expression
1		2re	⊢ 2 ∈ ℝ
2		2lt3	⊢ 2 < 3
3	1 2	gtneii	⊢ 3 ≠ 2
4		3prm	⊢ 3 ∈ ℙ
5		2prm	⊢ 2 ∈ ℙ
6		prmrp	⊢ ( ( 3 ∈ ℙ ∧ 2 ∈ ℙ ) → ( ( 3 gcd 2 ) = 1 ↔ 3 ≠ 2 ) )
7	4 5 6	mp2an	⊢ ( ( 3 gcd 2 ) = 1 ↔ 3 ≠ 2 )
8	3 7	mpbir	⊢ ( 3 gcd 2 ) = 1
9	8	oveq2i	⊢ ( ( 3 lcm 2 ) · ( 3 gcd 2 ) ) = ( ( 3 lcm 2 ) · 1 )
10		3nn	⊢ 3 ∈ ℕ
11		2nn	⊢ 2 ∈ ℕ
12		lcmgcdnn	⊢ ( ( 3 ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( 3 lcm 2 ) · ( 3 gcd 2 ) ) = ( 3 · 2 ) )
13	10 11 12	mp2an	⊢ ( ( 3 lcm 2 ) · ( 3 gcd 2 ) ) = ( 3 · 2 )
14	10	nnzi	⊢ 3 ∈ ℤ
15	11	nnzi	⊢ 2 ∈ ℤ
16		lcmcl	⊢ ( ( 3 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 3 lcm 2 ) ∈ ℕ0 )
17	14 15 16	mp2an	⊢ ( 3 lcm 2 ) ∈ ℕ0
18	17	nn0cni	⊢ ( 3 lcm 2 ) ∈ ℂ
19	18	mulid1i	⊢ ( ( 3 lcm 2 ) · 1 ) = ( 3 lcm 2 )
20	9 13 19	3eqtr3ri	⊢ ( 3 lcm 2 ) = ( 3 · 2 )
21		3t2e6	⊢ ( 3 · 2 ) = 6
22	20 21	eqtri	⊢ ( 3 lcm 2 ) = 6