Metamath Proof Explorer


Theorem eucalgval

Description: Euclid's Algorithm eucalg 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.

The value of the step function E for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 28-May-2014)

Ref Expression
Hypothesis eucalgval.1
|- E = ( x e. NN0 , y e. NN0 |-> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) )
Assertion eucalgval
|- ( X e. ( NN0 X. NN0 ) -> ( E ` X ) = if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) )

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 df-ov
 |-  ( ( 1st ` X ) E ( 2nd ` X ) ) = ( E ` <. ( 1st ` X ) , ( 2nd ` X ) >. )
3 xp1st
 |-  ( X e. ( NN0 X. NN0 ) -> ( 1st ` X ) e. NN0 )
4 xp2nd
 |-  ( X e. ( NN0 X. NN0 ) -> ( 2nd ` X ) e. NN0 )
5 1 eucalgval2
 |-  ( ( ( 1st ` X ) e. NN0 /\ ( 2nd ` X ) e. NN0 ) -> ( ( 1st ` X ) E ( 2nd ` X ) ) = if ( ( 2nd ` X ) = 0 , <. ( 1st ` X ) , ( 2nd ` X ) >. , <. ( 2nd ` X ) , ( ( 1st ` X ) mod ( 2nd ` X ) ) >. ) )
6 3 4 5 syl2anc
 |-  ( X e. ( NN0 X. NN0 ) -> ( ( 1st ` X ) E ( 2nd ` X ) ) = if ( ( 2nd ` X ) = 0 , <. ( 1st ` X ) , ( 2nd ` X ) >. , <. ( 2nd ` X ) , ( ( 1st ` X ) mod ( 2nd ` X ) ) >. ) )
7 2 6 eqtr3id
 |-  ( X e. ( NN0 X. NN0 ) -> ( E ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) = if ( ( 2nd ` X ) = 0 , <. ( 1st ` X ) , ( 2nd ` X ) >. , <. ( 2nd ` X ) , ( ( 1st ` X ) mod ( 2nd ` X ) ) >. ) )
8 1st2nd2
 |-  ( X e. ( NN0 X. NN0 ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
9 8 fveq2d
 |-  ( X e. ( NN0 X. NN0 ) -> ( E ` X ) = ( E ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
10 8 fveq2d
 |-  ( X e. ( NN0 X. NN0 ) -> ( mod ` X ) = ( mod ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
11 df-ov
 |-  ( ( 1st ` X ) mod ( 2nd ` X ) ) = ( mod ` <. ( 1st ` X ) , ( 2nd ` X ) >. )
12 10 11 eqtr4di
 |-  ( X e. ( NN0 X. NN0 ) -> ( mod ` X ) = ( ( 1st ` X ) mod ( 2nd ` X ) ) )
13 12 opeq2d
 |-  ( X e. ( NN0 X. NN0 ) -> <. ( 2nd ` X ) , ( mod ` X ) >. = <. ( 2nd ` X ) , ( ( 1st ` X ) mod ( 2nd ` X ) ) >. )
14 8 13 ifeq12d
 |-  ( X e. ( NN0 X. NN0 ) -> if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) = if ( ( 2nd ` X ) = 0 , <. ( 1st ` X ) , ( 2nd ` X ) >. , <. ( 2nd ` X ) , ( ( 1st ` X ) mod ( 2nd ` X ) ) >. ) )
15 7 9 14 3eqtr4d
 |-  ( X e. ( NN0 X. NN0 ) -> ( E ` X ) = if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) )