Metamath Proof Explorer

Theorem eucalgval2

Description: The value of the step function E for Euclid's Algorithm on an ordered pair. (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 eucalgval2 
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M E N ) = if ( N = 0 , <. M , N >. , <. N , ( M mod 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 simpr 
 |-  ( ( x = M /\ y = N ) -> y = N )
3 2 eqeq1d 
 |-  ( ( x = M /\ y = N ) -> ( y = 0 <-> N = 0 ) )
4 opeq12 
 |-  ( ( x = M /\ y = N ) -> <. x , y >. = <. M , N >. )
5 oveq12 
 |-  ( ( x = M /\ y = N ) -> ( x mod y ) = ( M mod N ) )
6 2 5 opeq12d 
 |-  ( ( x = M /\ y = N ) -> <. y , ( x mod y ) >. = <. N , ( M mod N ) >. )
7 3 4 6 ifbieq12d 
 |-  ( ( x = M /\ y = N ) -> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) = if ( N = 0 , <. M , N >. , <. N , ( M mod N ) >. ) )
8 opex 
 |-  <. M , N >. e. _V
9 opex 
 |-  <. N , ( M mod N ) >. e. _V
10 8 9 ifex 
 |-  if ( N = 0 , <. M , N >. , <. N , ( M mod N ) >. ) e. _V
11 7 1 10 ovmpoa 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M E N ) = if ( N = 0 , <. M , N >. , <. N , ( M mod N ) >. ) )