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 ⊢ 𝐾 ∈ ℕ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 𝑁 ) = 𝐺