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 
|- K e. NN0
gcdi.2 
|- R e. NN0
gcdi.3 
|- N e. NN0
gcdi.5 
|- ( N gcd R ) = G
gcdi.4 
|- ( ( K x. N ) + R ) = M
Assertion gcdi 
|- ( M gcd N ) = G

Proof

Step Hyp Ref Expression
1 gcdi.1 
 |-  K e. NN0
2 gcdi.2 
 |-  R e. NN0
3 gcdi.3 
 |-  N e. NN0
4 gcdi.5 
 |-  ( N gcd R ) = G
5 gcdi.4 
 |-  ( ( K x. N ) + R ) = M
6 1 3 nn0mulcli 
 |-  ( K x. N ) e. NN0
7 6 nn0cni 
 |-  ( K x. N ) e. CC
8 2 nn0cni 
 |-  R e. CC
9 7 8 5 addcomli 
 |-  ( R + ( K x. N ) ) = M
10 9 oveq2i 
 |-  ( N gcd ( R + ( K x. N ) ) ) = ( N gcd M )
11 1 nn0zi 
 |-  K e. ZZ
12 3 nn0zi 
 |-  N e. ZZ
13 2 nn0zi 
 |-  R e. ZZ
14 gcdaddm 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ R e. ZZ ) -> ( N gcd R ) = ( N gcd ( R + ( K x. N ) ) ) )
15 11 12 13 14 mp3an 
 |-  ( N gcd R ) = ( N gcd ( R + ( K x. N ) ) )
16 1 3 2 numcl 
 |-  ( ( K x. N ) + R ) e. NN0
17 5 16 eqeltrri 
 |-  M e. NN0
18 17 nn0zi 
 |-  M e. ZZ
19 gcdcom 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( N gcd M ) )
20 18 12 19 mp2an 
 |-  ( M gcd N ) = ( N gcd M )
21 10 15 20 3eqtr4i 
 |-  ( N gcd R ) = ( M gcd N )
22 21 4 eqtr3i 
 |-  ( M gcd N ) = G