Metamath Proof Explorer


Theorem 60lcm7e420

Description: The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Assertion 60lcm7e420 60 lcm 7 = 420

Proof

Step Hyp Ref Expression
1 6nn 6
2 1 decnncl2 60
3 7nn 7
4 1nn 1
5 4nn0 4 0
6 2nn 2
7 5 6 decnncl 42
8 7 decnncl2 420
9 60gcd7e1 60 gcd 7 = 1
10 2nn0 2 0
11 5 10 deccl 42 0
12 0nn0 0 0
13 11 12 deccl 420 0
14 13 nn0cni 420
15 14 mulid2i 1 420 = 420
16 7nn0 7 0
17 6nn0 6 0
18 eqid 60 = 60
19 7cn 7
20 6cn 6
21 7t6e42 7 6 = 42
22 19 20 21 mulcomli 6 7 = 42
23 2cn 2
24 23 addid1i 2 + 0 = 2
25 5 10 12 22 24 decaddi 6 7 + 0 = 42
26 0cn 0
27 19 mul01i 7 0 = 0
28 12 dec0h 0 = 00
29 28 eqcomi 00 = 0
30 27 29 eqtr4i 7 0 = 00
31 19 26 30 mulcomli 0 7 = 00
32 16 17 12 18 12 12 25 31 decmul1c 60 7 = 420
33 2 3 4 8 9 15 32 lcmeprodgcdi 60 lcm 7 = 420