Metamath Proof Explorer

Theorem algfx

Description: If F reaches a fixed point when the countdown function C reaches 0 , F remains fixed after N steps. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Hypotheses algcvga.1 
|- F : S --> S
algcvga.2 
|- R = seq 0 ( ( F o. 1st ) , ( NN0 X. { A } ) )
algcvga.3 
|- C : S --> NN0
algcvga.4 
|- ( z e. S -> ( ( C ` ( F ` z ) ) =/= 0 -> ( C ` ( F ` z ) ) < ( C ` z ) ) )
algcvga.5 
|- N = ( C ` A )
algfx.6 
|- ( z e. S -> ( ( C ` z ) = 0 -> ( F ` z ) = z ) )
Assertion algfx 
|- ( A e. S -> ( K e. ( ZZ>= ` N ) -> ( R ` K ) = ( R ` N ) ) )

Proof

Step Hyp Ref Expression
1 algcvga.1 
 |-  F : S --> S
2 algcvga.2 
 |-  R = seq 0 ( ( F o. 1st ) , ( NN0 X. { A } ) )
3 algcvga.3 
 |-  C : S --> NN0
4 algcvga.4 
 |-  ( z e. S -> ( ( C ` ( F ` z ) ) =/= 0 -> ( C ` ( F ` z ) ) < ( C ` z ) ) )
5 algcvga.5 
 |-  N = ( C ` A )
6 algfx.6 
 |-  ( z e. S -> ( ( C ` z ) = 0 -> ( F ` z ) = z ) )
7 3 ffvelcdmi 
 |-  ( A e. S -> ( C ` A ) e. NN0 )
8 5 7 eqeltrid 
 |-  ( A e. S -> N e. NN0 )
9 8 nn0zd 
 |-  ( A e. S -> N e. ZZ )
10 uzval 
 |-  ( N e. ZZ -> ( ZZ>= ` N ) = { z e. ZZ | N <_ z } )
11 10 eleq2d 
 |-  ( N e. ZZ -> ( K e. ( ZZ>= ` N ) <-> K e. { z e. ZZ | N <_ z } ) )
12 11 pm5.32i 
 |-  ( ( N e. ZZ /\ K e. ( ZZ>= ` N ) ) <-> ( N e. ZZ /\ K e. { z e. ZZ | N <_ z } ) )
13 fveqeq2 
 |-  ( m = N -> ( ( R ` m ) = ( R ` N ) <-> ( R ` N ) = ( R ` N ) ) )
14 13 imbi2d 
 |-  ( m = N -> ( ( A e. S -> ( R ` m ) = ( R ` N ) ) <-> ( A e. S -> ( R ` N ) = ( R ` N ) ) ) )
15 fveqeq2 
 |-  ( m = k -> ( ( R ` m ) = ( R ` N ) <-> ( R ` k ) = ( R ` N ) ) )
16 15 imbi2d 
 |-  ( m = k -> ( ( A e. S -> ( R ` m ) = ( R ` N ) ) <-> ( A e. S -> ( R ` k ) = ( R ` N ) ) ) )
17 fveqeq2 
 |-  ( m = ( k + 1 ) -> ( ( R ` m ) = ( R ` N ) <-> ( R ` ( k + 1 ) ) = ( R ` N ) ) )
18 17 imbi2d 
 |-  ( m = ( k + 1 ) -> ( ( A e. S -> ( R ` m ) = ( R ` N ) ) <-> ( A e. S -> ( R ` ( k + 1 ) ) = ( R ` N ) ) ) )
19 fveqeq2 
 |-  ( m = K -> ( ( R ` m ) = ( R ` N ) <-> ( R ` K ) = ( R ` N ) ) )
20 19 imbi2d 
 |-  ( m = K -> ( ( A e. S -> ( R ` m ) = ( R ` N ) ) <-> ( A e. S -> ( R ` K ) = ( R ` N ) ) ) )
21 eqidd 
 |-  ( A e. S -> ( R ` N ) = ( R ` N ) )
22 21 a1i 
 |-  ( N e. ZZ -> ( A e. S -> ( R ` N ) = ( R ` N ) ) )
23 10 eleq2d 
 |-  ( N e. ZZ -> ( k e. ( ZZ>= ` N ) <-> k e. { z e. ZZ | N <_ z } ) )
24 23 pm5.32i 
 |-  ( ( N e. ZZ /\ k e. ( ZZ>= ` N ) ) <-> ( N e. ZZ /\ k e. { z e. ZZ | N <_ z } ) )
25 eluznn0 
 |-  ( ( N e. NN0 /\ k e. ( ZZ>= ` N ) ) -> k e. NN0 )
26 8 25 sylan 
 |-  ( ( A e. S /\ k e. ( ZZ>= ` N ) ) -> k e. NN0 )
27 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
28 0zd 
 |-  ( A e. S -> 0 e. ZZ )
29 id 
 |-  ( A e. S -> A e. S )
30 1 a1i 
 |-  ( A e. S -> F : S --> S )
31 27 2 28 29 30 algrp1 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( R ` ( k + 1 ) ) = ( F ` ( R ` k ) ) )
32 26 31 syldan 
 |-  ( ( A e. S /\ k e. ( ZZ>= ` N ) ) -> ( R ` ( k + 1 ) ) = ( F ` ( R ` k ) ) )
33 27 2 28 29 30 algrf 
 |-  ( A e. S -> R : NN0 --> S )
34 33 ffvelcdmda 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( R ` k ) e. S )
35 26 34 syldan 
 |-  ( ( A e. S /\ k e. ( ZZ>= ` N ) ) -> ( R ` k ) e. S )
36 1 2 3 4 5 algcvga 
 |-  ( A e. S -> ( k e. ( ZZ>= ` N ) -> ( C ` ( R ` k ) ) = 0 ) )
37 36 imp 
 |-  ( ( A e. S /\ k e. ( ZZ>= ` N ) ) -> ( C ` ( R ` k ) ) = 0 )
38 fveqeq2 
 |-  ( z = ( R ` k ) -> ( ( C ` z ) = 0 <-> ( C ` ( R ` k ) ) = 0 ) )
39 fveq2 
 |-  ( z = ( R ` k ) -> ( F ` z ) = ( F ` ( R ` k ) ) )
40 id 
 |-  ( z = ( R ` k ) -> z = ( R ` k ) )
41 39 40 eqeq12d 
 |-  ( z = ( R ` k ) -> ( ( F ` z ) = z <-> ( F ` ( R ` k ) ) = ( R ` k ) ) )
42 38 41 imbi12d 
 |-  ( z = ( R ` k ) -> ( ( ( C ` z ) = 0 -> ( F ` z ) = z ) <-> ( ( C ` ( R ` k ) ) = 0 -> ( F ` ( R ` k ) ) = ( R ` k ) ) ) )
43 42 6 vtoclga 
 |-  ( ( R ` k ) e. S -> ( ( C ` ( R ` k ) ) = 0 -> ( F ` ( R ` k ) ) = ( R ` k ) ) )
44 35 37 43 sylc 
 |-  ( ( A e. S /\ k e. ( ZZ>= ` N ) ) -> ( F ` ( R ` k ) ) = ( R ` k ) )
45 32 44 eqtrd 
 |-  ( ( A e. S /\ k e. ( ZZ>= ` N ) ) -> ( R ` ( k + 1 ) ) = ( R ` k ) )
46 45 eqeq1d 
 |-  ( ( A e. S /\ k e. ( ZZ>= ` N ) ) -> ( ( R ` ( k + 1 ) ) = ( R ` N ) <-> ( R ` k ) = ( R ` N ) ) )
47 46 biimprd 
 |-  ( ( A e. S /\ k e. ( ZZ>= ` N ) ) -> ( ( R ` k ) = ( R ` N ) -> ( R ` ( k + 1 ) ) = ( R ` N ) ) )
48 47 expcom 
 |-  ( k e. ( ZZ>= ` N ) -> ( A e. S -> ( ( R ` k ) = ( R ` N ) -> ( R ` ( k + 1 ) ) = ( R ` N ) ) ) )
49 48 adantl 
 |-  ( ( N e. ZZ /\ k e. ( ZZ>= ` N ) ) -> ( A e. S -> ( ( R ` k ) = ( R ` N ) -> ( R ` ( k + 1 ) ) = ( R ` N ) ) ) )
50 24 49 sylbir 
 |-  ( ( N e. ZZ /\ k e. { z e. ZZ | N <_ z } ) -> ( A e. S -> ( ( R ` k ) = ( R ` N ) -> ( R ` ( k + 1 ) ) = ( R ` N ) ) ) )
51 50 a2d 
 |-  ( ( N e. ZZ /\ k e. { z e. ZZ | N <_ z } ) -> ( ( A e. S -> ( R ` k ) = ( R ` N ) ) -> ( A e. S -> ( R ` ( k + 1 ) ) = ( R ` N ) ) ) )
52 14 16 18 20 22 51 uzind3 
 |-  ( ( N e. ZZ /\ K e. { z e. ZZ | N <_ z } ) -> ( A e. S -> ( R ` K ) = ( R ` N ) ) )
53 12 52 sylbi 
 |-  ( ( N e. ZZ /\ K e. ( ZZ>= ` N ) ) -> ( A e. S -> ( R ` K ) = ( R ` N ) ) )
54 53 ex 
 |-  ( N e. ZZ -> ( K e. ( ZZ>= ` N ) -> ( A e. S -> ( R ` K ) = ( R ` N ) ) ) )
55 54 com3r 
 |-  ( A e. S -> ( N e. ZZ -> ( K e. ( ZZ>= ` N ) -> ( R ` K ) = ( R ` N ) ) ) )
56 9 55 mpd 
 |-  ( A e. S -> ( K e. ( ZZ>= ` N ) -> ( R ` K ) = ( R ` N ) ) )