Metamath Proof Explorer

Theorem eucalgf

Description: Domain and codomain 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 eucalgf 
|- E : ( NN0 X. NN0 ) --> ( NN0 X. NN0 )

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 nnne0 
 |-  ( y e. NN -> y =/= 0 )
3 2 adantl 
 |-  ( ( x e. NN0 /\ y e. NN ) -> y =/= 0 )
4 3 neneqd 
 |-  ( ( x e. NN0 /\ y e. NN ) -> -. y = 0 )
5 4 iffalsed 
 |-  ( ( x e. NN0 /\ y e. NN ) -> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) = <. y , ( x mod y ) >. )
6 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
7 6 adantl 
 |-  ( ( x e. NN0 /\ y e. NN ) -> y e. NN0 )
8 nn0z 
 |-  ( x e. NN0 -> x e. ZZ )
9 zmodcl 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( x mod y ) e. NN0 )
10 8 9 sylan 
 |-  ( ( x e. NN0 /\ y e. NN ) -> ( x mod y ) e. NN0 )
11 7 10 opelxpd 
 |-  ( ( x e. NN0 /\ y e. NN ) -> <. y , ( x mod y ) >. e. ( NN0 X. NN0 ) )
12 5 11 eqeltrd 
 |-  ( ( x e. NN0 /\ y e. NN ) -> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) e. ( NN0 X. NN0 ) )
13 12 adantlr 
 |-  ( ( ( x e. NN0 /\ y e. NN0 ) /\ y e. NN ) -> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) e. ( NN0 X. NN0 ) )
14 iftrue 
 |-  ( y = 0 -> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) = <. x , y >. )
15 14 adantl 
 |-  ( ( ( x e. NN0 /\ y e. NN0 ) /\ y = 0 ) -> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) = <. x , y >. )
16 opelxpi 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> <. x , y >. e. ( NN0 X. NN0 ) )
17 16 adantr 
 |-  ( ( ( x e. NN0 /\ y e. NN0 ) /\ y = 0 ) -> <. x , y >. e. ( NN0 X. NN0 ) )
18 15 17 eqeltrd 
 |-  ( ( ( x e. NN0 /\ y e. NN0 ) /\ y = 0 ) -> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) e. ( NN0 X. NN0 ) )
19 simpr 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> y e. NN0 )
20 elnn0 
 |-  ( y e. NN0 <-> ( y e. NN \/ y = 0 ) )
21 19 20 sylib 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( y e. NN \/ y = 0 ) )
22 13 18 21 mpjaodan 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) e. ( NN0 X. NN0 ) )
23 22 rgen2 
 |-  A. x e. NN0 A. y e. NN0 if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) e. ( NN0 X. NN0 )
24 1 fmpo 
 |-  ( A. x e. NN0 A. y e. NN0 if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) e. ( NN0 X. NN0 ) <-> E : ( NN0 X. NN0 ) --> ( NN0 X. NN0 ) )
25 23 24 mpbi 
 |-  E : ( NN0 X. NN0 ) --> ( NN0 X. NN0 )