Description: Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | lcm4un | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4nn | |
|
2 | id | |
|
3 | 2 | lcmfunnnd | |
4 | 1 3 | ax-mp | |
5 | 4m1e3 | |
|
6 | 5 | oveq2i | |
7 | 6 | fveq2i | |
8 | lcm3un | |
|
9 | 7 8 | eqtri | |
10 | 9 | oveq1i | |
11 | 6lcm4e12 | |
|
12 | 4 10 11 | 3eqtri | |