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 ∈ ℕ
2	1	nnzi	⊢ 6 ∈ ℤ
3		4z	⊢ 4 ∈ ℤ
4		gcdcom	⊢ ( ( 6 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 6 gcd 4 ) = ( 4 gcd 6 ) )
5	2 3 4	mp2an	⊢ ( 6 gcd 4 ) = ( 4 gcd 6 )
6		4cn	⊢ 4 ∈ ℂ
7		2cn	⊢ 2 ∈ ℂ
8		4p2e6	⊢ ( 4 + 2 ) = 6
9	6 7 8	addcomli	⊢ ( 2 + 4 ) = 6
10	9	oveq2i	⊢ ( 4 gcd ( 2 + 4 ) ) = ( 4 gcd 6 )
11		2z	⊢ 2 ∈ ℤ
12		gcdadd	⊢ ( ( 2 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 2 gcd 2 ) = ( 2 gcd ( 2 + 2 ) ) )
13	11 11 12	mp2an	⊢ ( 2 gcd 2 ) = ( 2 gcd ( 2 + 2 ) )
14		2p2e4	⊢ ( 2 + 2 ) = 4
15	14	oveq2i	⊢ ( 2 gcd ( 2 + 2 ) ) = ( 2 gcd 4 )
16		gcdcom	⊢ ( ( 2 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 2 gcd 4 ) = ( 4 gcd 2 ) )
17	11 3 16	mp2an	⊢ ( 2 gcd 4 ) = ( 4 gcd 2 )
18	15 17	eqtri	⊢ ( 2 gcd ( 2 + 2 ) ) = ( 4 gcd 2 )
19	13 18	eqtri	⊢ ( 2 gcd 2 ) = ( 4 gcd 2 )
20		gcdid	⊢ ( 2 ∈ ℤ → ( 2 gcd 2 ) = ( abs ‘ 2 ) )
21	11 20	ax-mp	⊢ ( 2 gcd 2 ) = ( abs ‘ 2 )
22		2re	⊢ 2 ∈ ℝ
23		0le2	⊢ 0 ≤ 2
24		absid	⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( abs ‘ 2 ) = 2 )
25	22 23 24	mp2an	⊢ ( abs ‘ 2 ) = 2
26	21 25	eqtri	⊢ ( 2 gcd 2 ) = 2
27		gcdadd	⊢ ( ( 4 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 4 gcd 2 ) = ( 4 gcd ( 2 + 4 ) ) )
28	3 11 27	mp2an	⊢ ( 4 gcd 2 ) = ( 4 gcd ( 2 + 4 ) )
29	19 26 28	3eqtr3ri	⊢ ( 4 gcd ( 2 + 4 ) ) = 2
30	5 10 29	3eqtr2i	⊢ ( 6 gcd 4 ) = 2