Metamath Proof Explorer

Theorem eucalgcvga

Description: Once Euclid's Algorithm halts after N steps, the second element of the state remains 0 . (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 29-May-2014)

Ref Expression
Hypotheses eucalgval.1 
|- E = ( x e. NN0 , y e. NN0 |-> if ( y = 0 , <. x , y >. , <. y , ( x mod y ) >. ) )
eucalg.2 
|- R = seq 0 ( ( E o. 1st ) , ( NN0 X. { A } ) )
eucalgcvga.3 
|- N = ( 2nd ` A )
Assertion eucalgcvga 
|- ( A e. ( NN0 X. NN0 ) -> ( K e. ( ZZ>= ` N ) -> ( 2nd ` ( R ` K ) ) = 0 ) )

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 eucalg.2 
 |-  R = seq 0 ( ( E o. 1st ) , ( NN0 X. { A } ) )
3 eucalgcvga.3 
 |-  N = ( 2nd ` A )
4 xp2nd 
 |-  ( A e. ( NN0 X. NN0 ) -> ( 2nd ` A ) e. NN0 )
5 3 4 eqeltrid 
 |-  ( A e. ( NN0 X. NN0 ) -> N e. NN0 )
6 eluznn0 
 |-  ( ( N e. NN0 /\ K e. ( ZZ>= ` N ) ) -> K e. NN0 )
7 5 6 sylan 
 |-  ( ( A e. ( NN0 X. NN0 ) /\ K e. ( ZZ>= ` N ) ) -> K e. NN0 )
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 0zd 
 |-  ( A e. ( NN0 X. NN0 ) -> 0 e. ZZ )
10 id 
 |-  ( A e. ( NN0 X. NN0 ) -> A e. ( NN0 X. NN0 ) )
11 1 eucalgf 
 |-  E : ( NN0 X. NN0 ) --> ( NN0 X. NN0 )
12 11 a1i 
 |-  ( A e. ( NN0 X. NN0 ) -> E : ( NN0 X. NN0 ) --> ( NN0 X. NN0 ) )
13 8 2 9 10 12 algrf 
 |-  ( A e. ( NN0 X. NN0 ) -> R : NN0 --> ( NN0 X. NN0 ) )
14 13 ffvelrnda 
 |-  ( ( A e. ( NN0 X. NN0 ) /\ K e. NN0 ) -> ( R ` K ) e. ( NN0 X. NN0 ) )
15 7 14 syldan 
 |-  ( ( A e. ( NN0 X. NN0 ) /\ K e. ( ZZ>= ` N ) ) -> ( R ` K ) e. ( NN0 X. NN0 ) )
16 15 fvresd 
 |-  ( ( A e. ( NN0 X. NN0 ) /\ K e. ( ZZ>= ` N ) ) -> ( ( 2nd |` ( NN0 X. NN0 ) ) ` ( R ` K ) ) = ( 2nd ` ( R ` K ) ) )
17 simpl 
 |-  ( ( A e. ( NN0 X. NN0 ) /\ K e. ( ZZ>= ` N ) ) -> A e. ( NN0 X. NN0 ) )
18 fvres 
 |-  ( A e. ( NN0 X. NN0 ) -> ( ( 2nd |` ( NN0 X. NN0 ) ) ` A ) = ( 2nd ` A ) )
19 18 3 eqtr4di 
 |-  ( A e. ( NN0 X. NN0 ) -> ( ( 2nd |` ( NN0 X. NN0 ) ) ` A ) = N )
20 19 fveq2d 
 |-  ( A e. ( NN0 X. NN0 ) -> ( ZZ>= ` ( ( 2nd |` ( NN0 X. NN0 ) ) ` A ) ) = ( ZZ>= ` N ) )
21 20 eleq2d 
 |-  ( A e. ( NN0 X. NN0 ) -> ( K e. ( ZZ>= ` ( ( 2nd |` ( NN0 X. NN0 ) ) ` A ) ) <-> K e. ( ZZ>= ` N ) ) )
22 21 biimpar 
 |-  ( ( A e. ( NN0 X. NN0 ) /\ K e. ( ZZ>= ` N ) ) -> K e. ( ZZ>= ` ( ( 2nd |` ( NN0 X. NN0 ) ) ` A ) ) )
23 f2ndres 
 |-  ( 2nd |` ( NN0 X. NN0 ) ) : ( NN0 X. NN0 ) --> NN0
24 1 eucalglt 
 |-  ( z e. ( NN0 X. NN0 ) -> ( ( 2nd ` ( E ` z ) ) =/= 0 -> ( 2nd ` ( E ` z ) ) < ( 2nd ` z ) ) )
25 11 ffvelrni 
 |-  ( z e. ( NN0 X. NN0 ) -> ( E ` z ) e. ( NN0 X. NN0 ) )
26 25 fvresd 
 |-  ( z e. ( NN0 X. NN0 ) -> ( ( 2nd |` ( NN0 X. NN0 ) ) ` ( E ` z ) ) = ( 2nd ` ( E ` z ) ) )
27 26 neeq1d 
 |-  ( z e. ( NN0 X. NN0 ) -> ( ( ( 2nd |` ( NN0 X. NN0 ) ) ` ( E ` z ) ) =/= 0 <-> ( 2nd ` ( E ` z ) ) =/= 0 ) )
28 fvres 
 |-  ( z e. ( NN0 X. NN0 ) -> ( ( 2nd |` ( NN0 X. NN0 ) ) ` z ) = ( 2nd ` z ) )
29 26 28 breq12d 
 |-  ( z e. ( NN0 X. NN0 ) -> ( ( ( 2nd |` ( NN0 X. NN0 ) ) ` ( E ` z ) ) < ( ( 2nd |` ( NN0 X. NN0 ) ) ` z ) <-> ( 2nd ` ( E ` z ) ) < ( 2nd ` z ) ) )
30 24 27 29 3imtr4d 
 |-  ( z e. ( NN0 X. NN0 ) -> ( ( ( 2nd |` ( NN0 X. NN0 ) ) ` ( E ` z ) ) =/= 0 -> ( ( 2nd |` ( NN0 X. NN0 ) ) ` ( E ` z ) ) < ( ( 2nd |` ( NN0 X. NN0 ) ) ` z ) ) )
31 eqid 
 |-  ( ( 2nd |` ( NN0 X. NN0 ) ) ` A ) = ( ( 2nd |` ( NN0 X. NN0 ) ) ` A )
32 11 2 23 30 31 algcvga 
 |-  ( A e. ( NN0 X. NN0 ) -> ( K e. ( ZZ>= ` ( ( 2nd |` ( NN0 X. NN0 ) ) ` A ) ) -> ( ( 2nd |` ( NN0 X. NN0 ) ) ` ( R ` K ) ) = 0 ) )
33 17 22 32 sylc 
 |-  ( ( A e. ( NN0 X. NN0 ) /\ K e. ( ZZ>= ` N ) ) -> ( ( 2nd |` ( NN0 X. NN0 ) ) ` ( R ` K ) ) = 0 )
34 16 33 eqtr3d 
 |-  ( ( A e. ( NN0 X. NN0 ) /\ K e. ( ZZ>= ` N ) ) -> ( 2nd ` ( R ` K ) ) = 0 )
35 34 ex 
 |-  ( A e. ( NN0 X. NN0 ) -> ( K e. ( ZZ>= ` N ) -> ( 2nd ` ( R ` K ) ) = 0 ) )