Metamath Proof Explorer

Theorem eucalginv

Description: The invariant of the step function E for Euclid's Algorithm is the gcd operator applied to the state. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 29-May-2014)

Ref Expression
Hypothesis eucalgval.1 
|- E = ( x e. NN0 , y e. NN0 |-> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) )
Assertion eucalginv 
|- ( X e. ( NN0 X. NN0 ) -> ( gcd ` ( E ` X ) ) = ( gcd ` 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 1 eucalgval 
 |-  ( X e. ( NN0 X. NN0 ) -> ( E ` X ) = if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) )
3 2 fveq2d 
 |-  ( X e. ( NN0 X. NN0 ) -> ( gcd ` ( E ` X ) ) = ( gcd ` if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) ) )
4 1st2nd2 
 |-  ( X e. ( NN0 X. NN0 ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
5 4 adantr 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
6 5 fveq2d 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( mod ` X ) = ( mod ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
7 df-ov 
 |-  ( ( 1st ` X ) mod ( 2nd ` X ) ) = ( mod ` <. ( 1st ` X ) , ( 2nd ` X ) >. )
8 6 7 eqtr4di 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( mod ` X ) = ( ( 1st ` X ) mod ( 2nd ` X ) ) )
9 8 oveq2d 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( ( 2nd ` X ) gcd ( mod ` X ) ) = ( ( 2nd ` X ) gcd ( ( 1st ` X ) mod ( 2nd ` X ) ) ) )
10 nnz 
 |-  ( ( 2nd ` X ) e. NN -> ( 2nd ` X ) e. ZZ )
11 xp1st 
 |-  ( X e. ( NN0 X. NN0 ) -> ( 1st ` X ) e. NN0 )
12 11 adantr 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( 1st ` X ) e. NN0 )
13 12 nn0zd 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( 1st ` X ) e. ZZ )
14 zmodcl 
 |-  ( ( ( 1st ` X ) e. ZZ /\ ( 2nd ` X ) e. NN ) -> ( ( 1st ` X ) mod ( 2nd ` X ) ) e. NN0 )
15 13 14 sylancom 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( ( 1st ` X ) mod ( 2nd ` X ) ) e. NN0 )
16 15 nn0zd 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( ( 1st ` X ) mod ( 2nd ` X ) ) e. ZZ )
17 gcdcom 
 |-  ( ( ( 2nd ` X ) e. ZZ /\ ( ( 1st ` X ) mod ( 2nd ` X ) ) e. ZZ ) -> ( ( 2nd ` X ) gcd ( ( 1st ` X ) mod ( 2nd ` X ) ) ) = ( ( ( 1st ` X ) mod ( 2nd ` X ) ) gcd ( 2nd ` X ) ) )
18 10 16 17 syl2an2 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( ( 2nd ` X ) gcd ( ( 1st ` X ) mod ( 2nd ` X ) ) ) = ( ( ( 1st ` X ) mod ( 2nd ` X ) ) gcd ( 2nd ` X ) ) )
19 modgcd 
 |-  ( ( ( 1st ` X ) e. ZZ /\ ( 2nd ` X ) e. NN ) -> ( ( ( 1st ` X ) mod ( 2nd ` X ) ) gcd ( 2nd ` X ) ) = ( ( 1st ` X ) gcd ( 2nd ` X ) ) )
20 13 19 sylancom 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( ( ( 1st ` X ) mod ( 2nd ` X ) ) gcd ( 2nd ` X ) ) = ( ( 1st ` X ) gcd ( 2nd ` X ) ) )
21 9 18 20 3eqtrd 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( ( 2nd ` X ) gcd ( mod ` X ) ) = ( ( 1st ` X ) gcd ( 2nd ` X ) ) )
22 nnne0 
 |-  ( ( 2nd ` X ) e. NN -> ( 2nd ` X ) =/= 0 )
23 22 adantl 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( 2nd ` X ) =/= 0 )
24 23 neneqd 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> -. ( 2nd ` X ) = 0 )
25 24 iffalsed 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) = <. ( 2nd ` X ) , ( mod ` X ) >. )
26 25 fveq2d 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( gcd ` if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) ) = ( gcd ` <. ( 2nd ` X ) , ( mod ` X ) >. ) )
27 df-ov 
 |-  ( ( 2nd ` X ) gcd ( mod ` X ) ) = ( gcd ` <. ( 2nd ` X ) , ( mod ` X ) >. )
28 26 27 eqtr4di 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( gcd ` if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) ) = ( ( 2nd ` X ) gcd ( mod ` X ) ) )
29 5 fveq2d 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( gcd ` X ) = ( gcd ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
30 df-ov 
 |-  ( ( 1st ` X ) gcd ( 2nd ` X ) ) = ( gcd ` <. ( 1st ` X ) , ( 2nd ` X ) >. )
31 29 30 eqtr4di 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( gcd ` X ) = ( ( 1st ` X ) gcd ( 2nd ` X ) ) )
32 21 28 31 3eqtr4d 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) e. NN ) -> ( gcd ` if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) ) = ( gcd ` X ) )
33 iftrue 
 |-  ( ( 2nd ` X ) = 0 -> if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) = X )
34 33 fveq2d 
 |-  ( ( 2nd ` X ) = 0 -> ( gcd ` if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) ) = ( gcd ` X ) )
35 34 adantl 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` X ) = 0 ) -> ( gcd ` if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) ) = ( gcd ` X ) )
36 xp2nd 
 |-  ( X e. ( NN0 X. NN0 ) -> ( 2nd ` X ) e. NN0 )
37 elnn0 
 |-  ( ( 2nd ` X ) e. NN0 <-> ( ( 2nd ` X ) e. NN \/ ( 2nd ` X ) = 0 ) )
38 36 37 sylib 
 |-  ( X e. ( NN0 X. NN0 ) -> ( ( 2nd ` X ) e. NN \/ ( 2nd ` X ) = 0 ) )
39 32 35 38 mpjaodan 
 |-  ( X e. ( NN0 X. NN0 ) -> ( gcd ` if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) ) = ( gcd ` X ) )
40 3 39 eqtrd 
 |-  ( X e. ( NN0 X. NN0 ) -> ( gcd ` ( E ` X ) ) = ( gcd ` X ) )