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

Metamath Proof Explorer

Theorem gcdi

Description: Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014)

Ref Expression
Hypotheses gcdi.1 ⊢ K ∈ ℕ 0
gcdi.2 ⊢ R ∈ ℕ 0
gcdi.3 ⊢ N ∈ ℕ 0
gcdi.5 ⊢ N gcd R = G
gcdi.4 ⊢ K ⋅ N + R = M
Assertion gcdi ⊢ M gcd N = G

Proof

Step Hyp Ref Expression
1 gcdi.1 ⊢ K ∈ ℕ 0
2 gcdi.2 ⊢ R ∈ ℕ 0
3 gcdi.3 ⊢ N ∈ ℕ 0
4 gcdi.5 ⊢ N gcd R = G
5 gcdi.4 ⊢ K ⋅ N + R = M
6 1 3 nn0mulcli ⊢ K ⋅ N ∈ ℕ 0
7 6 nn0cni ⊢ K ⋅ N ∈ ℂ
8 2 nn0cni ⊢ R ∈ ℂ
9 7 8 5 addcomli ⊢ R + K ⋅ N = M
10 9 oveq2i ⊢ N gcd R + K ⋅ N = N gcd M
11 1 nn0zi ⊢ K ∈ ℤ
12 3 nn0zi ⊢ N ∈ ℤ
13 2 nn0zi ⊢ R ∈ ℤ
14 gcdaddm ⊢ K ∈ ℤ ∧ N ∈ ℤ ∧ R ∈ ℤ → N gcd R = N gcd R + K ⋅ N
15 11 12 13 14 mp3an ⊢ N gcd R = N gcd R + K ⋅ N
16 1 3 2 numcl ⊢ K ⋅ N + R ∈ ℕ 0
17 5 16 eqeltrri ⊢ M ∈ ℕ 0
18 17 nn0zi ⊢ M ∈ ℤ
19 gcdcom ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = N gcd M
20 18 12 19 mp2an ⊢ M gcd N = N gcd M
21 10 15 20 3eqtr4i ⊢ N gcd R = M gcd N
22 21 4 eqtr3i ⊢ M gcd N = G