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