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 ∈ ℕ
2		4nn	⊢ 4 ∈ ℕ
3		5nn0	⊢ 5 ∈ ℕ0
4		2nn	⊢ 2 ∈ ℕ
5	3 4	decnncl	⊢ ; 5 2 ∈ ℕ
6	5	nnzi	⊢ ; 5 2 ∈ ℤ
7	1 2 6	gcdaddmzz2nncomi	⊢ ( 8 gcd 4 ) = ( 8 gcd ( ( ; 5 2 · 8 ) + 4 ) )
8		4nn0	⊢ 4 ∈ ℕ0
9		1nn0	⊢ 1 ∈ ℕ0
10	8 9	deccl	⊢ ; 4 1 ∈ ℕ0
11		6nn0	⊢ 6 ∈ ℕ0
12		0nn0	⊢ 0 ∈ ℕ0
13		eqid	⊢ ; ; 4 1 6 = ; ; 4 1 6
14	8	dec0h	⊢ 4 = ; 0 4
15		1p1e2	⊢ ( 1 + 1 ) = 2
16	10	nn0cni	⊢ ; 4 1 ∈ ℂ
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 ∈ ℕ0
22		2nn0	⊢ 2 ∈ ℕ0
23		eqid	⊢ ; 5 2 = ; 5 2
24		0p1e1	⊢ ( 0 + 1 ) = 1
25		8t5e40	⊢ ( 8 · 5 ) = ; 4 0
26	8 12 24 25	decsuc	⊢ ( ( 8 · 5 ) + 1 ) = ; 4 1
27		8t2e16	⊢ ( 8 · 2 ) = ; 1 6
28	21 3 22 23 11 9 26 27	decmul2c	⊢ ( 8 · ; 5 2 ) = ; ; 4 1 6
29	1 5	mulcomnni	⊢ ( 8 · ; 5 2 ) = ( ; 5 2 · 8 )
30	28 29	eqtr3i	⊢ ; ; 4 1 6 = ( ; 5 2 · 8 )
31	30	oveq1i	⊢ ( ; ; 4 1 6 + 4 ) = ( ( ; 5 2 · 8 ) + 4 )
32	20 31	eqtr3i	⊢ ; ; 4 2 0 = ( ( ; 5 2 · 8 ) + 4 )
33	32	oveq2i	⊢ ( 8 gcd ; ; 4 2 0 ) = ( 8 gcd ( ( ; 5 2 · 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 · 2 ) = 8
37	36	oveq2i	⊢ ( 4 gcd ( 4 · 2 ) ) = ( 4 gcd 8 )
38	2 4	gcdmultiplei	⊢ ( 4 gcd ( 4 · 2 ) ) = 4
39	37 38	eqtr3i	⊢ ( 4 gcd 8 ) = 4
40	35 39	eqtri	⊢ ( 8 gcd 4 ) = 4
41	8 4	decnncl	⊢ ; 4 2 ∈ ℕ
42	41	decnncl2	⊢ ; ; 4 2 0 ∈ ℕ
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