Theorem 60lcm7e420

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

	Ref	Expression
Assertion	60lcm7e420	$$⊢60\mathrm{lcm}7=420$$

Proof

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