Theorem gcdi

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

	Ref	Expression
Hypotheses	gcdi.1	⊢ 𝐾 ∈ ℕ0
	gcdi.2	⊢ 𝑅 ∈ ℕ0
	gcdi.3	⊢ 𝑁 ∈ ℕ0
	gcdi.5	⊢ ( 𝑁 gcd 𝑅 ) = 𝐺
	gcdi.4	⊢ ( ( 𝐾 · 𝑁 ) + 𝑅 ) = 𝑀
Assertion	gcdi	⊢ ( 𝑀 gcd 𝑁 ) = 𝐺

Proof

Step	Hyp	Ref	Expression
1		gcdi.1	⊢ 𝐾 ∈ ℕ0
2		gcdi.2	⊢ 𝑅 ∈ ℕ0
3		gcdi.3	⊢ 𝑁 ∈ ℕ0
4		gcdi.5	⊢ ( 𝑁 gcd 𝑅 ) = 𝐺
5		gcdi.4	⊢ ( ( 𝐾 · 𝑁 ) + 𝑅 ) = 𝑀
6	1 3	nn0mulcli	⊢ ( 𝐾 · 𝑁 ) ∈ ℕ0
7	6	nn0cni	⊢ ( 𝐾 · 𝑁 ) ∈ ℂ
8	2	nn0cni	⊢ 𝑅 ∈ ℂ
9	7 8 5	addcomli	⊢ ( 𝑅 + ( 𝐾 · 𝑁 ) ) = 𝑀
10	9	oveq2i	⊢ ( 𝑁 gcd ( 𝑅 + ( 𝐾 · 𝑁 ) ) ) = ( 𝑁 gcd 𝑀 )
11	1	nn0zi	⊢ 𝐾 ∈ ℤ
12	3	nn0zi	⊢ 𝑁 ∈ ℤ
13	2	nn0zi	⊢ 𝑅 ∈ ℤ
14		gcdaddm	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ) → ( 𝑁 gcd 𝑅 ) = ( 𝑁 gcd ( 𝑅 + ( 𝐾 · 𝑁 ) ) ) )
15	11 12 13 14	mp3an	⊢ ( 𝑁 gcd 𝑅 ) = ( 𝑁 gcd ( 𝑅 + ( 𝐾 · 𝑁 ) ) )
16	1 3 2	numcl	⊢ ( ( 𝐾 · 𝑁 ) + 𝑅 ) ∈ ℕ0
17	5 16	eqeltrri	⊢ 𝑀 ∈ ℕ0
18	17	nn0zi	⊢ 𝑀 ∈ ℤ
19		gcdcom	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( 𝑁 gcd 𝑀 ) )
20	18 12 19	mp2an	⊢ ( 𝑀 gcd 𝑁 ) = ( 𝑁 gcd 𝑀 )
21	10 15 20	3eqtr4i	⊢ ( 𝑁 gcd 𝑅 ) = ( 𝑀 gcd 𝑁 )
22	21 4	eqtr3i	⊢ ( 𝑀 gcd 𝑁 ) = 𝐺