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