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\in {\mathbb{N}}_0$$
	gcdi.2	$$⊢R\in {\mathbb{N}}_0$$
	gcdmodi.3	$$⊢N\in \mathbb{N}$$
	gcdmodi.4	$$⊢K\mathrm{mod}N=R\mathrm{mod}N$$
	gcdmodi.5	$$⊢N\gcd R=G$$
Assertion	gcdmodi	$$⊢K\gcd N=G$$

Proof

Step	Hyp	Ref	Expression
1		gcdi.1	$$⊢K\in {\mathbb{N}}_0$$
2		gcdi.2	$$⊢R\in {\mathbb{N}}_0$$
3		gcdmodi.3	$$⊢N\in \mathbb{N}$$
4		gcdmodi.4	$$⊢K\mathrm{mod}N=R\mathrm{mod}N$$
5		gcdmodi.5	$$⊢N\gcd R=G$$
6	4	oveq1i	$$⊢\left(K\mathrm{mod}N\right)\gcd N=\left(R\mathrm{mod}N\right)\gcd N$$
7	1	nn0zi	$$⊢K\in \mathbb{Z}$$
8		modgcd	$$⊢\left(K\in \mathbb{Z}\wedge N\in \mathbb{N}\right)\to \left(K\mathrm{mod}N\right)\gcd N=K\gcd N$$
9	7 3 8	mp2an	$$⊢\left(K\mathrm{mod}N\right)\gcd N=K\gcd N$$
10	2	nn0zi	$$⊢R\in \mathbb{Z}$$
11		modgcd	$$⊢\left(R\in \mathbb{Z}\wedge N\in \mathbb{N}\right)\to \left(R\mathrm{mod}N\right)\gcd N=R\gcd N$$
12	10 3 11	mp2an	$$⊢\left(R\mathrm{mod}N\right)\gcd N=R\gcd N$$
13	6 9 12	3eqtr3i	$$⊢K\gcd N=R\gcd N$$
14	3	nnzi	$$⊢N\in \mathbb{Z}$$
15		gcdcom	$$⊢\left(R\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to 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$$