Metamath Proof Explorer

Theorem lcm7un

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

Ref Expression
Assertion lcm7un 
|- ( _lcm ` ( 1 ... 7 ) ) = ; ; 4 2 0

Proof

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