Theorem eucalg

Description: Euclid's Algorithm computes the greatest common divisor of two nonnegative integers by repeatedly replacing the larger of them with its remainder modulo the smaller until the remainder is 0. Theorem 1.15 in ApostolNT p. 20.

Upon halting, the first member of the final state ( RN ) is equal to the gcd of the values comprising the input state <. M , N >. . This is Metamath 100 proof #69 (greatest common divisor algorithm). (Contributed by Paul Chapman, 31-Mar-2011) (Proof shortened by Mario Carneiro, 29-May-2014)

	Ref	Expression
Hypotheses	eucalgval.1	|- E = ( x e. NN0 , y e. NN0 |-> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) )
	eucalg.2	|- R = seq 0 ( ( E o. 1st ) , ( NN0 X. { A } ) )
	eucalg.3	|- A = <. M , N >.
Assertion	eucalg	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 1st ` ( R ` N ) ) = ( M gcd N ) )

Proof

Step	Hyp	Ref	Expression
1		eucalgval.1	|- E = ( x e. NN0 , y e. NN0 |-> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) )
2		eucalg.2	|- R = seq 0 ( ( E o. 1st ) , ( NN0 X. { A } ) )
3		eucalg.3	|- A = <. M , N >.
4		nn0uz	|- NN0 = ( ZZ>= ` 0 )
5		0zd	|- ( ( M e. NN0 /\ N e. NN0 ) -> 0 e. ZZ )
6		opelxpi	|- ( ( M e. NN0 /\ N e. NN0 ) -> <. M , N >. e. ( NN0 X. NN0 ) )
7	3 6	eqeltrid	|- ( ( M e. NN0 /\ N e. NN0 ) -> A e. ( NN0 X. NN0 ) )
8	1	eucalgf	|- E : ( NN0 X. NN0 ) --> ( NN0 X. NN0 )
9	8	a1i	|- ( ( M e. NN0 /\ N e. NN0 ) -> E : ( NN0 X. NN0 ) --> ( NN0 X. NN0 ) )
10	4 2 5 7 9	algrf	|- ( ( M e. NN0 /\ N e. NN0 ) -> R : NN0 --> ( NN0 X. NN0 ) )
11		ffvelcdm	|- ( ( R : NN0 --> ( NN0 X. NN0 ) /\ N e. NN0 ) -> ( R ` N ) e. ( NN0 X. NN0 ) )
12	10 11	sylancom	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( R ` N ) e. ( NN0 X. NN0 ) )
13		1st2nd2	|- ( ( R ` N ) e. ( NN0 X. NN0 ) -> ( R ` N ) = <. ( 1st ` ( R ` N ) ) , ( 2nd ` ( R ` N ) ) >. )
14	12 13	syl	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( R ` N ) = <. ( 1st ` ( R ` N ) ) , ( 2nd ` ( R ` N ) ) >. )
15	14	fveq2d	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( gcd ` ( R ` N ) ) = ( gcd ` <. ( 1st ` ( R ` N ) ) , ( 2nd ` ( R ` N ) ) >. ) )
16		df-ov	|- ( ( 1st ` ( R ` N ) ) gcd ( 2nd ` ( R ` N ) ) ) = ( gcd ` <. ( 1st ` ( R ` N ) ) , ( 2nd ` ( R ` N ) ) >. )
17	15 16	eqtr4di	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( gcd ` ( R ` N ) ) = ( ( 1st ` ( R ` N ) ) gcd ( 2nd ` ( R ` N ) ) ) )
18	3	fveq2i	|- ( 2nd ` A ) = ( 2nd ` <. M , N >. )
19		op2ndg	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 2nd ` <. M , N >. ) = N )
20	18 19	eqtrid	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 2nd ` A ) = N )
21	20	fveq2d	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( R ` ( 2nd ` A ) ) = ( R ` N ) )
22	21	fveq2d	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 2nd ` ( R ` ( 2nd ` A ) ) ) = ( 2nd ` ( R ` N ) ) )
23		xp2nd	|- ( A e. ( NN0 X. NN0 ) -> ( 2nd ` A ) e. NN0 )
24	23	nn0zd	|- ( A e. ( NN0 X. NN0 ) -> ( 2nd ` A ) e. ZZ )
25		uzid	|- ( ( 2nd ` A ) e. ZZ -> ( 2nd ` A ) e. ( ZZ>= ` ( 2nd ` A ) ) )
26	24 25	syl	|- ( A e. ( NN0 X. NN0 ) -> ( 2nd ` A ) e. ( ZZ>= ` ( 2nd ` A ) ) )
27		eqid	|- ( 2nd ` A ) = ( 2nd ` A )
28	1 2 27	eucalgcvga	|- ( A e. ( NN0 X. NN0 ) -> ( ( 2nd ` A ) e. ( ZZ>= ` ( 2nd ` A ) ) -> ( 2nd ` ( R ` ( 2nd ` A ) ) ) = 0 ) )
29	26 28	mpd	|- ( A e. ( NN0 X. NN0 ) -> ( 2nd ` ( R ` ( 2nd ` A ) ) ) = 0 )
30	7 29	syl	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 2nd ` ( R ` ( 2nd ` A ) ) ) = 0 )
31	22 30	eqtr3d	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 2nd ` ( R ` N ) ) = 0 )
32	31	oveq2d	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 1st ` ( R ` N ) ) gcd ( 2nd ` ( R ` N ) ) ) = ( ( 1st ` ( R ` N ) ) gcd 0 ) )
33		xp1st	|- ( ( R ` N ) e. ( NN0 X. NN0 ) -> ( 1st ` ( R ` N ) ) e. NN0 )
34		nn0gcdid0	|- ( ( 1st ` ( R ` N ) ) e. NN0 -> ( ( 1st ` ( R ` N ) ) gcd 0 ) = ( 1st ` ( R ` N ) ) )
35	12 33 34	3syl	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 1st ` ( R ` N ) ) gcd 0 ) = ( 1st ` ( R ` N ) ) )
36	17 32 35	3eqtrrd	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 1st ` ( R ` N ) ) = ( gcd ` ( R ` N ) ) )
37	1	eucalginv	|- ( z e. ( NN0 X. NN0 ) -> ( gcd ` ( E ` z ) ) = ( gcd ` z ) )
38	8	ffvelcdmi	|- ( z e. ( NN0 X. NN0 ) -> ( E ` z ) e. ( NN0 X. NN0 ) )
39	38	fvresd	|- ( z e. ( NN0 X. NN0 ) -> ( ( gcd |` ( NN0 X. NN0 ) ) ` ( E ` z ) ) = ( gcd ` ( E ` z ) ) )
40		fvres	|- ( z e. ( NN0 X. NN0 ) -> ( ( gcd |` ( NN0 X. NN0 ) ) ` z ) = ( gcd ` z ) )
41	37 39 40	3eqtr4d	|- ( z e. ( NN0 X. NN0 ) -> ( ( gcd |` ( NN0 X. NN0 ) ) ` ( E ` z ) ) = ( ( gcd |` ( NN0 X. NN0 ) ) ` z ) )
42	2 8 41	alginv	|- ( ( A e. ( NN0 X. NN0 ) /\ N e. NN0 ) -> ( ( gcd |` ( NN0 X. NN0 ) ) ` ( R ` N ) ) = ( ( gcd |` ( NN0 X. NN0 ) ) ` ( R ` 0 ) ) )
43	7 42	sylancom	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( gcd |` ( NN0 X. NN0 ) ) ` ( R ` N ) ) = ( ( gcd |` ( NN0 X. NN0 ) ) ` ( R ` 0 ) ) )
44	12	fvresd	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( gcd |` ( NN0 X. NN0 ) ) ` ( R ` N ) ) = ( gcd ` ( R ` N ) ) )
45		0nn0	|- 0 e. NN0
46		ffvelcdm	|- ( ( R : NN0 --> ( NN0 X. NN0 ) /\ 0 e. NN0 ) -> ( R ` 0 ) e. ( NN0 X. NN0 ) )
47	10 45 46	sylancl	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( R ` 0 ) e. ( NN0 X. NN0 ) )
48	47	fvresd	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( gcd |` ( NN0 X. NN0 ) ) ` ( R ` 0 ) ) = ( gcd ` ( R ` 0 ) ) )
49	43 44 48	3eqtr3d	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( gcd ` ( R ` N ) ) = ( gcd ` ( R ` 0 ) ) )
50	4 2 5 7	algr0	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( R ` 0 ) = A )
51	50 3	eqtrdi	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( R ` 0 ) = <. M , N >. )
52	51	fveq2d	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( gcd ` ( R ` 0 ) ) = ( gcd ` <. M , N >. ) )
53		df-ov	|- ( M gcd N ) = ( gcd ` <. M , N >. )
54	52 53	eqtr4di	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( gcd ` ( R ` 0 ) ) = ( M gcd N ) )
55	36 49 54	3eqtrd	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( 1st ` ( R ` N ) ) = ( M gcd N ) )