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 𝑁 ) = 𝐺