Metamath Proof Explorer

Theorem lcm4un

Description: Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Assertion lcm4un 
|- ( _lcm ` ( 1 ... 4 ) ) = ; 1 2

Proof

Step Hyp Ref Expression
1 4nn 
 |-  4 e. NN
2 id 
 |-  ( 4 e. NN -> 4 e. NN )
3 2 lcmfunnnd 
 |-  ( 4 e. NN -> ( _lcm ` ( 1 ... 4 ) ) = ( ( _lcm ` ( 1 ... ( 4 - 1 ) ) ) lcm 4 ) )
4 1 3 ax-mp 
 |-  ( _lcm ` ( 1 ... 4 ) ) = ( ( _lcm ` ( 1 ... ( 4 - 1 ) ) ) lcm 4 )
5 4m1e3 
 |-  ( 4 - 1 ) = 3
6 5 oveq2i 
 |-  ( 1 ... ( 4 - 1 ) ) = ( 1 ... 3 )
7 6 fveq2i 
 |-  ( _lcm ` ( 1 ... ( 4 - 1 ) ) ) = ( _lcm ` ( 1 ... 3 ) )
8 lcm3un 
 |-  ( _lcm ` ( 1 ... 3 ) ) = 6
9 7 8 eqtri 
 |-  ( _lcm ` ( 1 ... ( 4 - 1 ) ) ) = 6
10 9 oveq1i 
 |-  ( ( _lcm ` ( 1 ... ( 4 - 1 ) ) ) lcm 4 ) = ( 6 lcm 4 )
11 6lcm4e12 
 |-  ( 6 lcm 4 ) = ; 1 2
12 4 10 11 3eqtri 
 |-  ( _lcm ` ( 1 ... 4 ) ) = ; 1 2