Description: The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | 420lcm8e840 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4nn0 | ||
2 | 2nn | ||
3 | 1 2 | decnncl | |
4 | 3 | decnncl2 | |
5 | 8nn | ||
6 | 4nn | ||
7 | 8nn0 | ||
8 | 7 6 | decnncl | |
9 | 8 | decnncl2 | |
10 | 420gcd8e4 | ||
11 | eqid | ||
12 | 4 5 | mulcomnni | |
13 | 4t2e8 | ||
14 | 13 | oveq1i | |
15 | 12 14 | eqtr4i | |
16 | 6 2 4 | mulassnni | |
17 | 15 16 | eqtri | |
18 | 2 | nnnn0i | |
19 | 3 | nnnn0i | |
20 | 0nn0 | ||
21 | eqid | ||
22 | eqid | ||
23 | 4cn | ||
24 | 2cn | ||
25 | 23 24 13 | mulcomli | |
26 | 25 | oveq1i | |
27 | 8cn | ||
28 | 27 | addid1i | |
29 | 26 28 | eqtri | |
30 | 2t2e4 | ||
31 | 1 | dec0h | |
32 | 31 | eqcomi | |
33 | 30 32 | eqtr4i | |
34 | 18 1 18 22 1 20 29 33 | decmul2c | |
35 | 23 | addid1i | |
36 | 7 1 20 34 35 | decaddi | |
37 | 2t0e0 | ||
38 | 20 | dec0h | |
39 | 38 | eqcomi | |
40 | 37 39 | eqtr4i | |
41 | 18 19 20 21 20 20 36 40 | decmul2c | |
42 | 41 | oveq2i | |
43 | 17 42 | eqtri | |
44 | 4 5 6 9 10 11 43 | lcmeprodgcdi |