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 e. ZZ
2 3z 
 |-  3 e. ZZ
3 4z 
 |-  4 e. ZZ
4 lcmftp 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ /\ 4 e. ZZ ) -> ( _lcm ` { 2 , 3 , 4 } ) = ( ( 2 lcm 3 ) lcm 4 ) )
5 lcmcom 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ ) -> ( 2 lcm 3 ) = ( 3 lcm 2 ) )
6 5 3adant3 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ /\ 4 e. ZZ ) -> ( 2 lcm 3 ) = ( 3 lcm 2 ) )
7 3lcm2e6woprm 
 |-  ( 3 lcm 2 ) = 6
8 6 7 eqtrdi 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ /\ 4 e. ZZ ) -> ( 2 lcm 3 ) = 6 )
9 8 oveq1d 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ /\ 4 e. ZZ ) -> ( ( 2 lcm 3 ) lcm 4 ) = ( 6 lcm 4 ) )
10 6lcm4e12 
 |-  ( 6 lcm 4 ) = ; 1 2
11 9 10 eqtrdi 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ /\ 4 e. ZZ ) -> ( ( 2 lcm 3 ) lcm 4 ) = ; 1 2 )
12 4 11 eqtrd 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ /\ 4 e. ZZ ) -> ( _lcm ` { 2 , 3 , 4 } ) = ; 1 2 )
13 1 2 3 12 mp3an 
 |-  ( _lcm ` { 2 , 3 , 4 } ) = ; 1 2