Theorem 60lcm7e420

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

	Ref	Expression
Assertion	60lcm7e420	⊢ ( ; 6 0 lcm 7 ) = ; ; 4 2 0

Proof

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