Metamath Proof Explorer


Theorem lcm5un

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

Ref Expression
Assertion lcm5un ( lcm ‘ ( 1 ... 5 ) ) = 6 0

Proof

Step Hyp Ref Expression
1 5nn 5 ∈ ℕ
2 1 a1i ( 5 ∈ ℕ → 5 ∈ ℕ )
3 2 lcmfunnnd ( 5 ∈ ℕ → ( lcm ‘ ( 1 ... 5 ) ) = ( ( lcm ‘ ( 1 ... ( 5 − 1 ) ) ) lcm 5 ) )
4 1 3 ax-mp ( lcm ‘ ( 1 ... 5 ) ) = ( ( lcm ‘ ( 1 ... ( 5 − 1 ) ) ) lcm 5 )
5 5m1e4 ( 5 − 1 ) = 4
6 5 oveq2i ( 1 ... ( 5 − 1 ) ) = ( 1 ... 4 )
7 6 fveq2i ( lcm ‘ ( 1 ... ( 5 − 1 ) ) ) = ( lcm ‘ ( 1 ... 4 ) )
8 7 oveq1i ( ( lcm ‘ ( 1 ... ( 5 − 1 ) ) ) lcm 5 ) = ( ( lcm ‘ ( 1 ... 4 ) ) lcm 5 )
9 lcm4un ( lcm ‘ ( 1 ... 4 ) ) = 1 2
10 9 oveq1i ( ( lcm ‘ ( 1 ... 4 ) ) lcm 5 ) = ( 1 2 lcm 5 )
11 8 10 eqtri ( ( lcm ‘ ( 1 ... ( 5 − 1 ) ) ) lcm 5 ) = ( 1 2 lcm 5 )
12 12lcm5e60 ( 1 2 lcm 5 ) = 6 0
13 4 11 12 3eqtri ( lcm ‘ ( 1 ... 5 ) ) = 6 0