Metamath Proof Explorer


Theorem 12lcm5e60

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

Ref Expression
Assertion 12lcm5e60 12 lcm 5 = 60

Proof

Step Hyp Ref Expression
1 1nn0 1 0
2 2nn 2
3 1 2 decnncl 12
4 5nn 5
5 1nn 1
6 6nn 6
7 6 decnncl2 60
8 12gcd5e1 12 gcd 5 = 1
9 6nn0 6 0
10 0nn0 0 0
11 9 10 deccl 60 0
12 11 nn0cni 60
13 12 mulid2i 1 60 = 60
14 5nn0 5 0
15 2nn0 2 0
16 eqid 12 = 12
17 5cn 5
18 17 mulid2i 1 5 = 5
19 18 oveq1i 1 5 + 1 = 5 + 1
20 5p1e6 5 + 1 = 6
21 19 20 eqtri 1 5 + 1 = 6
22 2cn 2
23 5t2e10 5 2 = 10
24 17 22 23 mulcomli 2 5 = 10
25 14 1 15 16 10 1 21 24 decmul1c 12 5 = 60
26 3 4 5 7 8 13 25 lcmeprodgcdi 12 lcm 5 = 60