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

Proof

Step Hyp Ref Expression
1 gcdi.1 
 |-  K e. NN0
2 gcdi.2 
 |-  R e. NN0
3 gcdmodi.3 
 |-  N e. NN
4 gcdmodi.4 
 |-  ( K mod N ) = ( R mod N )
5 gcdmodi.5 
 |-  ( N gcd R ) = G
6 4 oveq1i 
 |-  ( ( K mod N ) gcd N ) = ( ( R mod N ) gcd N )
7 1 nn0zi 
 |-  K e. ZZ
8 modgcd 
 |-  ( ( K e. ZZ /\ N e. NN ) -> ( ( K mod N ) gcd N ) = ( K gcd N ) )
9 7 3 8 mp2an 
 |-  ( ( K mod N ) gcd N ) = ( K gcd N )
10 2 nn0zi 
 |-  R e. ZZ
11 modgcd 
 |-  ( ( R e. ZZ /\ N e. NN ) -> ( ( R mod N ) gcd N ) = ( R gcd N ) )
12 10 3 11 mp2an 
 |-  ( ( R mod N ) gcd N ) = ( R gcd N )
13 6 9 12 3eqtr3i 
 |-  ( K gcd N ) = ( R gcd N )
14 3 nnzi 
 |-  N e. ZZ
15 gcdcom 
 |-  ( ( R e. ZZ /\ N e. ZZ ) -> ( R gcd N ) = ( N gcd R ) )
16 10 14 15 mp2an 
 |-  ( R gcd N ) = ( N gcd R )
17 13 16 5 3eqtri 
 |-  ( K gcd N ) = G