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

Metamath Proof Explorer

Theorem gcdmodi

Description: Calculate a GCD via Euclid's algorithm. Theorem 5.6 in ApostolNT p. 109. (Contributed by Mario Carneiro, 19-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 gcdi.1 ⊢ K ∈ ℕ 0
2 gcdi.2 ⊢ R ∈ ℕ 0
3 gcdmodi.3 ⊢ N ∈ ℕ
4 gcdmodi.4 ⊢ K mod N = R mod N
5 gcdmodi.5 ⊢ N gcd R = G
6 4 oveq1i ⊢ K mod N gcd N = R mod N gcd N
7 1 nn0zi ⊢ K ∈ ℤ
8 modgcd ⊢ K ∈ ℤ ∧ N ∈ ℕ → K mod N gcd N = K gcd N
9 7 3 8 mp2an ⊢ K mod N gcd N = K gcd N
10 2 nn0zi ⊢ R ∈ ℤ
11 modgcd ⊢ R ∈ ℤ ∧ N ∈ ℕ → R mod N gcd N = R gcd N
12 10 3 11 mp2an ⊢ R mod N gcd N = R gcd N
13 6 9 12 3eqtr3i ⊢ K gcd N = R gcd N
14 3 nnzi ⊢ N ∈ ℤ
15 gcdcom ⊢ R ∈ ℤ ∧ N ∈ ℤ → R gcd N = N gcd R
16 10 14 15 mp2an ⊢ R gcd N = N gcd R
17 13 16 5 3eqtri ⊢ K gcd N = G