Metamath Proof Explorer

Theorem eucalglt

Description: The second member of the state decreases with each iteration of the step function E for Euclid's Algorithm. (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 eucalglt 
|- ( X e. ( NN0 X. NN0 ) -> ( ( 2nd ` ( E ` X ) ) =/= 0 -> ( 2nd ` ( E ` X ) ) < ( 2nd ` 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 adantr 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( E ` X ) = if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) )
4 simpr 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 2nd ` ( E ` X ) ) =/= 0 )
5 iftrue 
 |-  ( ( 2nd ` X ) = 0 -> if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) = X )
6 5 eqeq2d 
 |-  ( ( 2nd ` X ) = 0 -> ( ( E ` X ) = if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) <-> ( E ` X ) = X ) )
7 fveq2 
 |-  ( ( E ` X ) = X -> ( 2nd ` ( E ` X ) ) = ( 2nd ` X ) )
8 6 7 biimtrdi 
 |-  ( ( 2nd ` X ) = 0 -> ( ( E ` X ) = if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) -> ( 2nd ` ( E ` X ) ) = ( 2nd ` X ) ) )
9 eqeq2 
 |-  ( ( 2nd ` X ) = 0 -> ( ( 2nd ` ( E ` X ) ) = ( 2nd ` X ) <-> ( 2nd ` ( E ` X ) ) = 0 ) )
10 8 9 sylibd 
 |-  ( ( 2nd ` X ) = 0 -> ( ( E ` X ) = if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) -> ( 2nd ` ( E ` X ) ) = 0 ) )
11 3 10 syl5com 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( ( 2nd ` X ) = 0 -> ( 2nd ` ( E ` X ) ) = 0 ) )
12 11 necon3ad 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( ( 2nd ` ( E ` X ) ) =/= 0 -> -. ( 2nd ` X ) = 0 ) )
13 4 12 mpd 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> -. ( 2nd ` X ) = 0 )
14 13 iffalsed 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> if ( ( 2nd ` X ) = 0 , X , <. ( 2nd ` X ) , ( mod ` X ) >. ) = <. ( 2nd ` X ) , ( mod ` X ) >. )
15 3 14 eqtrd 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( E ` X ) = <. ( 2nd ` X ) , ( mod ` X ) >. )
16 15 fveq2d 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 2nd ` ( E ` X ) ) = ( 2nd ` <. ( 2nd ` X ) , ( mod ` X ) >. ) )
17 fvex 
 |-  ( 2nd ` X ) e. _V
18 fvex 
 |-  ( mod ` X ) e. _V
19 17 18 op2nd 
 |-  ( 2nd ` <. ( 2nd ` X ) , ( mod ` X ) >. ) = ( mod ` X )
20 16 19 eqtrdi 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 2nd ` ( E ` X ) ) = ( mod ` X ) )
21 1st2nd2 
 |-  ( X e. ( NN0 X. NN0 ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
22 21 adantr 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> X = <. ( 1st ` X ) , ( 2nd ` X ) >. )
23 22 fveq2d 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( mod ` X ) = ( mod ` <. ( 1st ` X ) , ( 2nd ` X ) >. ) )
24 df-ov 
 |-  ( ( 1st ` X ) mod ( 2nd ` X ) ) = ( mod ` <. ( 1st ` X ) , ( 2nd ` X ) >. )
25 23 24 eqtr4di 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( mod ` X ) = ( ( 1st ` X ) mod ( 2nd ` X ) ) )
26 20 25 eqtrd 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 2nd ` ( E ` X ) ) = ( ( 1st ` X ) mod ( 2nd ` X ) ) )
27 xp1st 
 |-  ( X e. ( NN0 X. NN0 ) -> ( 1st ` X ) e. NN0 )
28 27 adantr 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 1st ` X ) e. NN0 )
29 28 nn0red 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 1st ` X ) e. RR )
30 xp2nd 
 |-  ( X e. ( NN0 X. NN0 ) -> ( 2nd ` X ) e. NN0 )
31 30 adantr 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 2nd ` X ) e. NN0 )
32 elnn0 
 |-  ( ( 2nd ` X ) e. NN0 <-> ( ( 2nd ` X ) e. NN \/ ( 2nd ` X ) = 0 ) )
33 31 32 sylib 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( ( 2nd ` X ) e. NN \/ ( 2nd ` X ) = 0 ) )
34 33 ord 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( -. ( 2nd ` X ) e. NN -> ( 2nd ` X ) = 0 ) )
35 13 34 mt3d 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 2nd ` X ) e. NN )
36 35 nnrpd 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 2nd ` X ) e. RR+ )
37 modlt 
 |-  ( ( ( 1st ` X ) e. RR /\ ( 2nd ` X ) e. RR+ ) -> ( ( 1st ` X ) mod ( 2nd ` X ) ) < ( 2nd ` X ) )
38 29 36 37 syl2anc 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( ( 1st ` X ) mod ( 2nd ` X ) ) < ( 2nd ` X ) )
39 26 38 eqbrtrd 
 |-  ( ( X e. ( NN0 X. NN0 ) /\ ( 2nd ` ( E ` X ) ) =/= 0 ) -> ( 2nd ` ( E ` X ) ) < ( 2nd ` X ) )
40 39 ex 
 |-  ( X e. ( NN0 X. NN0 ) -> ( ( 2nd ` ( E ` X ) ) =/= 0 -> ( 2nd ` ( E ` X ) ) < ( 2nd ` X ) ) )