Metamath Proof Explorer


Theorem lcm1un

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

Ref Expression
Assertion lcm1un
|- ( _lcm ` ( 1 ... 1 ) ) = 1

Proof

Step Hyp Ref Expression
1 1nn
 |-  1 e. NN
2 id
 |-  ( 1 e. NN -> 1 e. NN )
3 2 lcmfunnnd
 |-  ( 1 e. NN -> ( _lcm ` ( 1 ... 1 ) ) = ( ( _lcm ` ( 1 ... ( 1 - 1 ) ) ) lcm 1 ) )
4 1 3 ax-mp
 |-  ( _lcm ` ( 1 ... 1 ) ) = ( ( _lcm ` ( 1 ... ( 1 - 1 ) ) ) lcm 1 )
5 1m1e0
 |-  ( 1 - 1 ) = 0
6 5 oveq2i
 |-  ( 1 ... ( 1 - 1 ) ) = ( 1 ... 0 )
7 fz10
 |-  ( 1 ... 0 ) = (/)
8 6 7 eqtri
 |-  ( 1 ... ( 1 - 1 ) ) = (/)
9 8 fveq2i
 |-  ( _lcm ` ( 1 ... ( 1 - 1 ) ) ) = ( _lcm ` (/) )
10 lcmf0
 |-  ( _lcm ` (/) ) = 1
11 9 10 eqtri
 |-  ( _lcm ` ( 1 ... ( 1 - 1 ) ) ) = 1
12 11 oveq1i
 |-  ( ( _lcm ` ( 1 ... ( 1 - 1 ) ) ) lcm 1 ) = ( 1 lcm 1 )
13 1z
 |-  1 e. ZZ
14 lcmid
 |-  ( 1 e. ZZ -> ( 1 lcm 1 ) = ( abs ` 1 ) )
15 13 14 ax-mp
 |-  ( 1 lcm 1 ) = ( abs ` 1 )
16 abs1
 |-  ( abs ` 1 ) = 1
17 15 16 eqtri
 |-  ( 1 lcm 1 ) = 1
18 12 17 eqtri
 |-  ( ( _lcm ` ( 1 ... ( 1 - 1 ) ) ) lcm 1 ) = 1
19 4 18 eqtri
 |-  ( _lcm ` ( 1 ... 1 ) ) = 1