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 } ) = 1 2

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 ) = 1 2
11 9 10 eqtrdi ⊢ ( ( 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 4 ∈ ℤ ) → ( ( 2 lcm 3 ) lcm 4 ) = 1 2 )
12 4 11 eqtrd ⊢ ( ( 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 4 ∈ ℤ ) → ( lcm ‘ { 2 , 3 , 4 } ) = 1 2 )
13 1 2 3 12 mp3an ⊢ ( lcm ‘ { 2 , 3 , 4 } ) = 1 2