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_14=12

Proof

Step Hyp Ref Expression
1 4nn 4
2 id 44
3 2 lcmfunnnd 4lcm_14=lcm_141lcm4
4 1 3 ax-mp lcm_14=lcm_141lcm4
5 4m1e3 41=3
6 5 oveq2i 141=13
7 6 fveq2i lcm_141=lcm_13
8 lcm3un lcm_13=6
9 7 8 eqtri lcm_141=6
10 9 oveq1i lcm_141lcm4=6lcm4
11 6lcm4e12 6lcm4=12
12 4 10 11 3eqtri lcm_14=12