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 ⊢ 𝐾 ∈ ℕ0
gcdi.2 ⊢ 𝑅 ∈ ℕ0
gcdmodi.3 ⊢ 𝑁 ∈ ℕ
gcdmodi.4 ⊢ ( 𝐾 mod 𝑁 ) = ( 𝑅 mod 𝑁 )
gcdmodi.5 ⊢ ( 𝑁 gcd 𝑅 ) = 𝐺
Assertion gcdmodi ( 𝐾 gcd 𝑁 ) = 𝐺

Proof

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