Theorem gcdi

Description: Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014)

	Ref	Expression
Hypotheses	gcdi.1	$$⊢K\in {\mathbb{N}}_0$$
	gcdi.2	$$⊢R\in {\mathbb{N}}_0$$
	gcdi.3	$$⊢N\in {\mathbb{N}}_0$$
	gcdi.5	$$⊢N\gcd R=G$$
	gcdi.4	$$⊢K\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+R=M$$
Assertion	gcdi	$$⊢M\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		gcdi.3	$$⊢N\in {\mathbb{N}}_0$$
4		gcdi.5	$$⊢N\gcd R=G$$
5		gcdi.4	$$⊢K\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+R=M$$
6	1 3	nn0mulcli	$$⊢K\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in {\mathbb{N}}_0$$
7	6	nn0cni	$$⊢K\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
8	2	nn0cni	$$⊢R\in ℂ$$
9	7 8 5	addcomli	$$⊢R+K\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=M$$
10	9	oveq2i	$$⊢N\gcd \left(R+K\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)=N\gcd M$$
11	1	nn0zi	$$⊢K\in \mathbb{Z}$$
12	3	nn0zi	$$⊢N\in \mathbb{Z}$$
13	2	nn0zi	$$⊢R\in \mathbb{Z}$$
14		gcdaddm	$$⊢\left(K\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge R\in \mathbb{Z}\right)\to N\gcd R=N\gcd \left(R+K\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
15	11 12 13 14	mp3an	$$⊢N\gcd R=N\gcd \left(R+K\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
16	1 3 2	numcl	$$⊢K\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}+R\in {\mathbb{N}}_0$$
17	5 16	eqeltrri	$$⊢M\in {\mathbb{N}}_0$$
18	17	nn0zi	$$⊢M\in \mathbb{Z}$$
19		gcdcom	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to 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$$