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 e. NN
2	1	decnncl2	|- ; 6 0 e. NN
3		7nn	|- 7 e. NN
4		1nn	|- 1 e. NN
5		4nn0	|- 4 e. NN0
6		2nn	|- 2 e. NN
7	5 6	decnncl	|- ; 4 2 e. NN
8	7	decnncl2	|- ; ; 4 2 0 e. NN
9		60gcd7e1	|- ( ; 6 0 gcd 7 ) = 1
10		2nn0	|- 2 e. NN0
11	5 10	deccl	|- ; 4 2 e. NN0
12		0nn0	|- 0 e. NN0
13	11 12	deccl	|- ; ; 4 2 0 e. NN0
14	13	nn0cni	|- ; ; 4 2 0 e. CC
15	14	mulid2i	|- ( 1 x. ; ; 4 2 0 ) = ; ; 4 2 0
16		7nn0	|- 7 e. NN0
17		6nn0	|- 6 e. NN0
18		eqid	|- ; 6 0 = ; 6 0
19		7cn	|- 7 e. CC
20		6cn	|- 6 e. CC
21		7t6e42	|- ( 7 x. 6 ) = ; 4 2
22	19 20 21	mulcomli	|- ( 6 x. 7 ) = ; 4 2
23		2cn	|- 2 e. CC
24	23	addid1i	|- ( 2 + 0 ) = 2
25	5 10 12 22 24	decaddi	|- ( ( 6 x. 7 ) + 0 ) = ; 4 2
26		0cn	|- 0 e. CC
27	19	mul01i	|- ( 7 x. 0 ) = 0
28	12	dec0h	|- 0 = ; 0 0
29	28	eqcomi	|- ; 0 0 = 0
30	27 29	eqtr4i	|- ( 7 x. 0 ) = ; 0 0
31	19 26 30	mulcomli	|- ( 0 x. 7 ) = ; 0 0
32	16 17 12 18 12 12 25 31	decmul1c	|- ( ; 6 0 x. 7 ) = ; ; 4 2 0
33	2 3 4 8 9 15 32	lcmeprodgcdi	|- ( ; 6 0 lcm 7 ) = ; ; 4 2 0