Description: The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | 12lcm5e60 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn0 | ||
2 | 2nn | ||
3 | 1 2 | decnncl | |
4 | 5nn | ||
5 | 1nn | ||
6 | 6nn | ||
7 | 6 | decnncl2 | |
8 | 12gcd5e1 | ||
9 | 6nn0 | ||
10 | 0nn0 | ||
11 | 9 10 | deccl | |
12 | 11 | nn0cni | |
13 | 12 | mulid2i | |
14 | 5nn0 | ||
15 | 2nn0 | ||
16 | eqid | ||
17 | 5cn | ||
18 | 17 | mulid2i | |
19 | 18 | oveq1i | |
20 | 5p1e6 | ||
21 | 19 20 | eqtri | |
22 | 2cn | ||
23 | 5t2e10 | ||
24 | 17 22 23 | mulcomli | |
25 | 14 1 15 16 10 1 21 24 | decmul1c | |
26 | 3 4 5 7 8 13 25 | lcmeprodgcdi |