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 = 60

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 = 12
10 9 oveq1i lcm _ 1 4 lcm 5 = 12 lcm 5
11 8 10 eqtri lcm _ 1 5 1 lcm 5 = 12 lcm 5
12 12lcm5e60 12 lcm 5 = 60
13 4 11 12 3eqtri lcm _ 1 5 = 60