Theorem 420gcd8e4

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

	Ref	Expression
Assertion	420gcd8e4	$$⊢420\gcd 8=4$$

Proof

Step	Hyp	Ref	Expression
1		8nn	$$⊢8\in \mathbb{N}$$
2		4nn	$$⊢4\in \mathbb{N}$$
3		5nn0	$$⊢5\in {\mathbb{N}}_0$$
4		2nn	$$⊢2\in \mathbb{N}$$
5	3 4	decnncl	$$⊢52\in \mathbb{N}$$
6	5	nnzi	$$⊢52\in \mathbb{Z}$$
7	1 2 6	gcdaddmzz2nncomi	$$⊢8\gcd 4=8\gcd \left(52\cdot 8+4\right)$$
8		4nn0	$$⊢4\in {\mathbb{N}}_0$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10	8 9	deccl	$$⊢41\in {\mathbb{N}}_0$$
11		6nn0	$$⊢6\in {\mathbb{N}}_0$$
12		0nn0	$$⊢0\in {\mathbb{N}}_0$$
13		eqid	$$⊢416=416$$
14	8	dec0h	$$⊢4=04$$
15		1p1e2	$$⊢1+1=2$$
16	10	nn0cni	$$⊢41\in ℂ$$
17	16	addid1i	$$⊢41+0=41$$
18	8 9 15 17	decsuc	$$⊢41+0+1=42$$
19		6p4e10	$$⊢6+4=10$$
20	10 11 12 8 13 14 18 19	decaddc2	$$⊢416+4=420$$
21		8nn0	$$⊢8\in {\mathbb{N}}_0$$
22		2nn0	$$⊢2\in {\mathbb{N}}_0$$
23		eqid	$$⊢52=52$$
24		0p1e1	$$⊢0+1=1$$
25		8t5e40	$$⊢8\cdot 5=40$$
26	8 12 24 25	decsuc	$$⊢8\cdot 5+1=41$$
27		8t2e16	$$⊢8\cdot 2=16$$
28	21 3 22 23 11 9 26 27	decmul2c	$$⊢8\cdot 52=416$$
29	1 5	mulcomnni	$$⊢8\cdot 52=52\cdot 8$$
30	28 29	eqtr3i	$$⊢416=52\cdot 8$$
31	30	oveq1i	$$⊢416+4=52\cdot 8+4$$
32	20 31	eqtr3i	$$⊢420=52\cdot 8+4$$
33	32	oveq2i	$$⊢8\gcd 420=8\gcd \left(52\cdot 8+4\right)$$
34	7 33	eqtr4i	$$⊢8\gcd 4=8\gcd 420$$
35	1 2	gcdcomnni	$$⊢8\gcd 4=4\gcd 8$$
36		4t2e8	$$⊢4\cdot 2=8$$
37	36	oveq2i	$$⊢4\gcd 4\cdot 2=4\gcd 8$$
38	2 4	gcdmultiplei	$$⊢4\gcd 4\cdot 2=4$$
39	37 38	eqtr3i	$$⊢4\gcd 8=4$$
40	35 39	eqtri	$$⊢8\gcd 4=4$$
41	8 4	decnncl	$$⊢42\in \mathbb{N}$$
42	41	decnncl2	$$⊢420\in \mathbb{N}$$
43	1 42	gcdcomnni	$$⊢8\gcd 420=420\gcd 8$$
44	34 40 43	3eqtr3ri	$$⊢420\gcd 8=4$$