Metamath Proof Explorer

Theorem lcmf2a3a4e12

Description: The least common multiple of 2 , 3 and 4 is 12. (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion lcmf2a3a4e12 ⊢ lcm _ ⁡ 2 3 4 = 12

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 3z ⊢ 3 ∈ ℤ
3 4z ⊢ 4 ∈ ℤ
4 lcmftp ⊢ 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 4 ∈ ℤ → lcm _ ⁡ 2 3 4 = 2 lcm 3 lcm 4
5 lcmcom ⊢ 2 ∈ ℤ ∧ 3 ∈ ℤ → 2 lcm 3 = 3 lcm 2
6 5 3adant3 ⊢ 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 4 ∈ ℤ → 2 lcm 3 = 3 lcm 2
7 3lcm2e6woprm ⊢ 3 lcm 2 = 6
8 6 7 eqtrdi ⊢ 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 4 ∈ ℤ → 2 lcm 3 = 6
9 8 oveq1d ⊢ 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 4 ∈ ℤ → 2 lcm 3 lcm 4 = 6 lcm 4
10 6lcm4e12 ⊢ 6 lcm 4 = 12
11 9 10 eqtrdi ⊢ 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 4 ∈ ℤ → 2 lcm 3 lcm 4 = 12
12 4 11 eqtrd ⊢ 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 4 ∈ ℤ → lcm _ ⁡ 2 3 4 = 12
13 1 2 3 12 mp3an ⊢ lcm _ ⁡ 2 3 4 = 12