This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mulridi ⊢ 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