Theorem 420gcd8e4

Description: The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Assertion	420gcd8e4	|- ( ; ; 4 2 0 gcd 8 ) = 4

Proof

Step	Hyp	Ref	Expression
1		8nn	|- 8 e. NN
2		4nn	|- 4 e. NN
3		5nn0	|- 5 e. NN0
4		2nn	|- 2 e. NN
5	3 4	decnncl	|- ; 5 2 e. NN
6	5	nnzi	|- ; 5 2 e. ZZ
7	1 2 6	gcdaddmzz2nncomi	|- ( 8 gcd 4 ) = ( 8 gcd ( ( ; 5 2 x. 8 ) + 4 ) )
8		4nn0	|- 4 e. NN0
9		1nn0	|- 1 e. NN0
10	8 9	deccl	|- ; 4 1 e. NN0
11		6nn0	|- 6 e. NN0
12		0nn0	|- 0 e. NN0
13		eqid	|- ; ; 4 1 6 = ; ; 4 1 6
14	8	dec0h	|- 4 = ; 0 4
15		1p1e2	|- ( 1 + 1 ) = 2
16	10	nn0cni	|- ; 4 1 e. CC
17	16	addid1i	|- ( ; 4 1 + 0 ) = ; 4 1
18	8 9 15 17	decsuc	|- ( ( ; 4 1 + 0 ) + 1 ) = ; 4 2
19		6p4e10	|- ( 6 + 4 ) = ; 1 0
20	10 11 12 8 13 14 18 19	decaddc2	|- ( ; ; 4 1 6 + 4 ) = ; ; 4 2 0
21		8nn0	|- 8 e. NN0
22		2nn0	|- 2 e. NN0
23		eqid	|- ; 5 2 = ; 5 2
24		0p1e1	|- ( 0 + 1 ) = 1
25		8t5e40	|- ( 8 x. 5 ) = ; 4 0
26	8 12 24 25	decsuc	|- ( ( 8 x. 5 ) + 1 ) = ; 4 1
27		8t2e16	|- ( 8 x. 2 ) = ; 1 6
28	21 3 22 23 11 9 26 27	decmul2c	|- ( 8 x. ; 5 2 ) = ; ; 4 1 6
29	1 5	mulcomnni	|- ( 8 x. ; 5 2 ) = ( ; 5 2 x. 8 )
30	28 29	eqtr3i	|- ; ; 4 1 6 = ( ; 5 2 x. 8 )
31	30	oveq1i	|- ( ; ; 4 1 6 + 4 ) = ( ( ; 5 2 x. 8 ) + 4 )
32	20 31	eqtr3i	|- ; ; 4 2 0 = ( ( ; 5 2 x. 8 ) + 4 )
33	32	oveq2i	|- ( 8 gcd ; ; 4 2 0 ) = ( 8 gcd ( ( ; 5 2 x. 8 ) + 4 ) )
34	7 33	eqtr4i	|- ( 8 gcd 4 ) = ( 8 gcd ; ; 4 2 0 )
35	1 2	gcdcomnni	|- ( 8 gcd 4 ) = ( 4 gcd 8 )
36		4t2e8	|- ( 4 x. 2 ) = 8
37	36	oveq2i	|- ( 4 gcd ( 4 x. 2 ) ) = ( 4 gcd 8 )
38	2 4	gcdmultiplei	|- ( 4 gcd ( 4 x. 2 ) ) = 4
39	37 38	eqtr3i	|- ( 4 gcd 8 ) = 4
40	35 39	eqtri	|- ( 8 gcd 4 ) = 4
41	8 4	decnncl	|- ; 4 2 e. NN
42	41	decnncl2	|- ; ; 4 2 0 e. NN
43	1 42	gcdcomnni	|- ( 8 gcd ; ; 4 2 0 ) = ( ; ; 4 2 0 gcd 8 )
44	34 40 43	3eqtr3ri	|- ( ; ; 4 2 0 gcd 8 ) = 4