Metamath Proof Explorer

Theorem lcm3un

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

Ref Expression
Assertion lcm3un 
|- ( _lcm ` ( 1 ... 3 ) ) = 6

Proof

Step Hyp Ref Expression
1 3nn 
 |-  3 e. NN
2 id 
 |-  ( 3 e. NN -> 3 e. NN )
3 2 lcmfunnnd 
 |-  ( 3 e. NN -> ( _lcm ` ( 1 ... 3 ) ) = ( ( _lcm ` ( 1 ... ( 3 - 1 ) ) ) lcm 3 ) )
4 1 3 ax-mp 
 |-  ( _lcm ` ( 1 ... 3 ) ) = ( ( _lcm ` ( 1 ... ( 3 - 1 ) ) ) lcm 3 )
5 3m1e2 
 |-  ( 3 - 1 ) = 2
6 5 oveq2i 
 |-  ( 1 ... ( 3 - 1 ) ) = ( 1 ... 2 )
7 6 fveq2i 
 |-  ( _lcm ` ( 1 ... ( 3 - 1 ) ) ) = ( _lcm ` ( 1 ... 2 ) )
8 lcm2un 
 |-  ( _lcm ` ( 1 ... 2 ) ) = 2
9 7 8 eqtri 
 |-  ( _lcm ` ( 1 ... ( 3 - 1 ) ) ) = 2
10 9 oveq1i 
 |-  ( ( _lcm ` ( 1 ... ( 3 - 1 ) ) ) lcm 3 ) = ( 2 lcm 3 )
11 2z 
 |-  2 e. ZZ
12 3z 
 |-  3 e. ZZ
13 11 12 pm3.2i 
 |-  ( 2 e. ZZ /\ 3 e. ZZ )
14 lcmcom 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ ) -> ( 2 lcm 3 ) = ( 3 lcm 2 ) )
15 13 14 ax-mp 
 |-  ( 2 lcm 3 ) = ( 3 lcm 2 )
16 3lcm2e6 
 |-  ( 3 lcm 2 ) = 6
17 15 16 eqtri 
 |-  ( 2 lcm 3 ) = 6
18 10 17 eqtri 
 |-  ( ( _lcm ` ( 1 ... ( 3 - 1 ) ) ) lcm 3 ) = 6
19 4 18 eqtri 
 |-  ( _lcm ` ( 1 ... 3 ) ) = 6