This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = 2
21 11 20 ax-mp ⊢ 2 gcd 2 = 2
22 2re ⊢ 2 ∈ ℝ
23 0le2 ⊢ 0 ≤ 2
24 absid ⊢ 2 ∈ ℝ ∧ 0 ≤ 2 → 2 = 2
25 22 23 24 mp2an ⊢ 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