Description: The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | 60lcm7e420 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 6nn | ||
2 | 1 | decnncl2 | |
3 | 7nn | ||
4 | 1nn | ||
5 | 4nn0 | ||
6 | 2nn | ||
7 | 5 6 | decnncl | |
8 | 7 | decnncl2 | |
9 | 60gcd7e1 | ||
10 | 2nn0 | ||
11 | 5 10 | deccl | |
12 | 0nn0 | ||
13 | 11 12 | deccl | |
14 | 13 | nn0cni | |
15 | 14 | mulid2i | |
16 | 7nn0 | ||
17 | 6nn0 | ||
18 | eqid | ||
19 | 7cn | ||
20 | 6cn | ||
21 | 7t6e42 | ||
22 | 19 20 21 | mulcomli | |
23 | 2cn | ||
24 | 23 | addid1i | |
25 | 5 10 12 22 24 | decaddi | |
26 | 0cn | ||
27 | 19 | mul01i | |
28 | 12 | dec0h | |
29 | 28 | eqcomi | |
30 | 27 29 | eqtr4i | |
31 | 19 26 30 | mulcomli | |
32 | 16 17 12 18 12 12 25 31 | decmul1c | |
33 | 2 3 4 8 9 15 32 | lcmeprodgcdi |