Theorem 6gcd4e2

Description: The greatest common divisor of six and four is two. To calculate this gcd, a simple form of Euclid's algorithm is used: ( 6 gcd 4 ) = ( ( 4 + 2 ) gcd 4 ) = ( 2 gcd 4 ) and ( 2 gcd 4 ) = ( 2 gcd ( 2 + 2 ) ) = ( 2 gcd 2 ) = 2 . (Contributed by AV, 27-Aug-2020)

	Ref	Expression
Assertion	6gcd4e2	$$⊢6\gcd 4=2$$

Proof

Step	Hyp	Ref	Expression
1		6nn	$$⊢6\in \mathbb{N}$$
2	1	nnzi	$$⊢6\in \mathbb{Z}$$
3		4z	$$⊢4\in \mathbb{Z}$$
4		gcdcom	$$⊢\left(6\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to 6\gcd 4=4\gcd 6$$
5	2 3 4	mp2an	$$⊢6\gcd 4=4\gcd 6$$
6		4cn	$$⊢4\in ℂ$$
7		2cn	$$⊢2\in ℂ$$
8		4p2e6	$$⊢4+2=6$$
9	6 7 8	addcomli	$$⊢2+4=6$$
10	9	oveq2i	$$⊢4\gcd \left(2+4\right)=4\gcd 6$$
11		2z	$$⊢2\in \mathbb{Z}$$
12		gcdadd	$$⊢\left(2\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 2\gcd 2=2\gcd \left(2+2\right)$$
13	11 11 12	mp2an	$$⊢2\gcd 2=2\gcd \left(2+2\right)$$
14		2p2e4	$$⊢2+2=4$$
15	14	oveq2i	$$⊢2\gcd \left(2+2\right)=2\gcd 4$$
16		gcdcom	$$⊢\left(2\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to 2\gcd 4=4\gcd 2$$
17	11 3 16	mp2an	$$⊢2\gcd 4=4\gcd 2$$
18	15 17	eqtri	$$⊢2\gcd \left(2+2\right)=4\gcd 2$$
19	13 18	eqtri	$$⊢2\gcd 2=4\gcd 2$$
20		gcdid	$$⊢2\in \mathbb{Z}\to 2\gcd 2=\left|2\right|$$
21	11 20	ax-mp	$$⊢2\gcd 2=\left|2\right|$$
22		2re	$$⊢2\in ℝ$$
23		0le2	$$⊢0\le 2$$
24		absid	$$⊢\left(2\in ℝ\wedge 0\le 2\right)\to \left|2\right|=2$$
25	22 23 24	mp2an	$$⊢\left|2\right|=2$$
26	21 25	eqtri	$$⊢2\gcd 2=2$$
27		gcdadd	$$⊢\left(4\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 4\gcd 2=4\gcd \left(2+4\right)$$
28	3 11 27	mp2an	$$⊢4\gcd 2=4\gcd \left(2+4\right)$$
29	19 26 28	3eqtr3ri	$$⊢4\gcd \left(2+4\right)=2$$
30	5 10 29	3eqtr2i	$$⊢6\gcd 4=2$$