Metamath Proof Explorer


Theorem lcm4un

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

Ref Expression
Assertion lcm4un lcm _ 1 4 = 12

Proof

Step Hyp Ref Expression
1 4nn 4
2 id 4 4
3 2 lcmfunnnd 4 lcm _ 1 4 = lcm _ 1 4 1 lcm 4
4 1 3 ax-mp lcm _ 1 4 = lcm _ 1 4 1 lcm 4
5 4m1e3 4 1 = 3
6 5 oveq2i 1 4 1 = 1 3
7 6 fveq2i lcm _ 1 4 1 = lcm _ 1 3
8 lcm3un lcm _ 1 3 = 6
9 7 8 eqtri lcm _ 1 4 1 = 6
10 9 oveq1i lcm _ 1 4 1 lcm 4 = 6 lcm 4
11 6lcm4e12 6 lcm 4 = 12
12 4 10 11 3eqtri lcm _ 1 4 = 12