This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem algcvga

Description: The countdown function C remains 0 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 )
Assertion algcvga 
|- ( A e. S -> ( K e. ( ZZ>= ` N ) -> ( C ` ( R ` K ) ) = 0 ) )

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 3 ffvelcdmi 
 |-  ( A e. S -> ( C ` A ) e. NN0 )
7 5 6 eqeltrid 
 |-  ( A e. S -> N e. NN0 )
8 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
9 eluz1 
 |-  ( N e. ZZ -> ( K e. ( ZZ>= ` N ) <-> ( K e. ZZ /\ N <_ K ) ) )
10 2fveq3 
 |-  ( m = N -> ( C ` ( R ` m ) ) = ( C ` ( R ` N ) ) )
11 10 eqeq1d 
 |-  ( m = N -> ( ( C ` ( R ` m ) ) = 0 <-> ( C ` ( R ` N ) ) = 0 ) )
12 11 imbi2d 
 |-  ( m = N -> ( ( A e. S -> ( C ` ( R ` m ) ) = 0 ) <-> ( A e. S -> ( C ` ( R ` N ) ) = 0 ) ) )
13 2fveq3 
 |-  ( m = k -> ( C ` ( R ` m ) ) = ( C ` ( R ` k ) ) )
14 13 eqeq1d 
 |-  ( m = k -> ( ( C ` ( R ` m ) ) = 0 <-> ( C ` ( R ` k ) ) = 0 ) )
15 14 imbi2d 
 |-  ( m = k -> ( ( A e. S -> ( C ` ( R ` m ) ) = 0 ) <-> ( A e. S -> ( C ` ( R ` k ) ) = 0 ) ) )
16 2fveq3 
 |-  ( m = ( k + 1 ) -> ( C ` ( R ` m ) ) = ( C ` ( R ` ( k + 1 ) ) ) )
17 16 eqeq1d 
 |-  ( m = ( k + 1 ) -> ( ( C ` ( R ` m ) ) = 0 <-> ( C ` ( R ` ( k + 1 ) ) ) = 0 ) )
18 17 imbi2d 
 |-  ( m = ( k + 1 ) -> ( ( A e. S -> ( C ` ( R ` m ) ) = 0 ) <-> ( A e. S -> ( C ` ( R ` ( k + 1 ) ) ) = 0 ) ) )
19 2fveq3 
 |-  ( m = K -> ( C ` ( R ` m ) ) = ( C ` ( R ` K ) ) )
20 19 eqeq1d 
 |-  ( m = K -> ( ( C ` ( R ` m ) ) = 0 <-> ( C ` ( R ` K ) ) = 0 ) )
21 20 imbi2d 
 |-  ( m = K -> ( ( A e. S -> ( C ` ( R ` m ) ) = 0 ) <-> ( A e. S -> ( C ` ( R ` K ) ) = 0 ) ) )
22 1 2 3 4 5 algcvg 
 |-  ( A e. S -> ( C ` ( R ` N ) ) = 0 )
23 22 a1i 
 |-  ( N e. ZZ -> ( A e. S -> ( C ` ( R ` N ) ) = 0 ) )
24 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
25 24 adantr 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> 0 <_ N )
26 0re 
 |-  0 e. RR
27 nn0re 
 |-  ( N e. NN0 -> N e. RR )
28 zre 
 |-  ( k e. ZZ -> k e. RR )
29 letr 
 |-  ( ( 0 e. RR /\ N e. RR /\ k e. RR ) -> ( ( 0 <_ N /\ N <_ k ) -> 0 <_ k ) )
30 26 27 28 29 mp3an3an 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( ( 0 <_ N /\ N <_ k ) -> 0 <_ k ) )
31 25 30 mpand 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N <_ k -> 0 <_ k ) )
32 elnn0z 
 |-  ( k e. NN0 <-> ( k e. ZZ /\ 0 <_ k ) )
33 32 simplbi2 
 |-  ( k e. ZZ -> ( 0 <_ k -> k e. NN0 ) )
34 33 adantl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( 0 <_ k -> k e. NN0 ) )
35 31 34 syld 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N <_ k -> k e. NN0 ) )
36 7 35 sylan 
 |-  ( ( A e. S /\ k e. ZZ ) -> ( N <_ k -> k e. NN0 ) )
37 36 impr 
 |-  ( ( A e. S /\ ( k e. ZZ /\ N <_ k ) ) -> k e. NN0 )
38 37 expcom 
 |-  ( ( k e. ZZ /\ N <_ k ) -> ( A e. S -> k e. NN0 ) )
39 38 3adant1 
 |-  ( ( N e. ZZ /\ k e. ZZ /\ N <_ k ) -> ( A e. S -> k e. NN0 ) )
40 39 ancld 
 |-  ( ( N e. ZZ /\ k e. ZZ /\ N <_ k ) -> ( A e. S -> ( A e. S /\ k e. NN0 ) ) )
41 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
42 0zd 
 |-  ( A e. S -> 0 e. ZZ )
43 id 
 |-  ( A e. S -> A e. S )
44 1 a1i 
 |-  ( A e. S -> F : S --> S )
45 41 2 42 43 44 algrf 
 |-  ( A e. S -> R : NN0 --> S )
46 45 ffvelcdmda 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( R ` k ) e. S )
47 2fveq3 
 |-  ( z = ( R ` k ) -> ( C ` ( F ` z ) ) = ( C ` ( F ` ( R ` k ) ) ) )
48 47 neeq1d 
 |-  ( z = ( R ` k ) -> ( ( C ` ( F ` z ) ) =/= 0 <-> ( C ` ( F ` ( R ` k ) ) ) =/= 0 ) )
49 fveq2 
 |-  ( z = ( R ` k ) -> ( C ` z ) = ( C ` ( R ` k ) ) )
50 47 49 breq12d 
 |-  ( z = ( R ` k ) -> ( ( C ` ( F ` z ) ) < ( C ` z ) <-> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) )
51 48 50 imbi12d 
 |-  ( z = ( R ` k ) -> ( ( ( C ` ( F ` z ) ) =/= 0 -> ( C ` ( F ` z ) ) < ( C ` z ) ) <-> ( ( C ` ( F ` ( R ` k ) ) ) =/= 0 -> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) ) )
52 51 4 vtoclga 
 |-  ( ( R ` k ) e. S -> ( ( C ` ( F ` ( R ` k ) ) ) =/= 0 -> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) )
53 1 3 algcvgb 
 |-  ( ( R ` k ) e. S -> ( ( ( C ` ( F ` ( R ` k ) ) ) =/= 0 -> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) <-> ( ( ( C ` ( R ` k ) ) =/= 0 -> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) /\ ( ( C ` ( R ` k ) ) = 0 -> ( C ` ( F ` ( R ` k ) ) ) = 0 ) ) ) )
54 simpr 
 |-  ( ( ( ( C ` ( R ` k ) ) =/= 0 -> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) /\ ( ( C ` ( R ` k ) ) = 0 -> ( C ` ( F ` ( R ` k ) ) ) = 0 ) ) -> ( ( C ` ( R ` k ) ) = 0 -> ( C ` ( F ` ( R ` k ) ) ) = 0 ) )
55 53 54 biimtrdi 
 |-  ( ( R ` k ) e. S -> ( ( ( C ` ( F ` ( R ` k ) ) ) =/= 0 -> ( C ` ( F ` ( R ` k ) ) ) < ( C ` ( R ` k ) ) ) -> ( ( C ` ( R ` k ) ) = 0 -> ( C ` ( F ` ( R ` k ) ) ) = 0 ) ) )
56 52 55 mpd 
 |-  ( ( R ` k ) e. S -> ( ( C ` ( R ` k ) ) = 0 -> ( C ` ( F ` ( R ` k ) ) ) = 0 ) )
57 46 56 syl 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( ( C ` ( R ` k ) ) = 0 -> ( C ` ( F ` ( R ` k ) ) ) = 0 ) )
58 41 2 42 43 44 algrp1 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( R ` ( k + 1 ) ) = ( F ` ( R ` k ) ) )
59 58 fveqeq2d 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( ( C ` ( R ` ( k + 1 ) ) ) = 0 <-> ( C ` ( F ` ( R ` k ) ) ) = 0 ) )
60 57 59 sylibrd 
 |-  ( ( A e. S /\ k e. NN0 ) -> ( ( C ` ( R ` k ) ) = 0 -> ( C ` ( R ` ( k + 1 ) ) ) = 0 ) )
61 40 60 syl6 
 |-  ( ( N e. ZZ /\ k e. ZZ /\ N <_ k ) -> ( A e. S -> ( ( C ` ( R ` k ) ) = 0 -> ( C ` ( R ` ( k + 1 ) ) ) = 0 ) ) )
62 61 a2d 
 |-  ( ( N e. ZZ /\ k e. ZZ /\ N <_ k ) -> ( ( A e. S -> ( C ` ( R ` k ) ) = 0 ) -> ( A e. S -> ( C ` ( R ` ( k + 1 ) ) ) = 0 ) ) )
63 12 15 18 21 23 62 uzind 
 |-  ( ( N e. ZZ /\ K e. ZZ /\ N <_ K ) -> ( A e. S -> ( C ` ( R ` K ) ) = 0 ) )
64 63 3expib 
 |-  ( N e. ZZ -> ( ( K e. ZZ /\ N <_ K ) -> ( A e. S -> ( C ` ( R ` K ) ) = 0 ) ) )
65 9 64 sylbid 
 |-  ( N e. ZZ -> ( K e. ( ZZ>= ` N ) -> ( A e. S -> ( C ` ( R ` K ) ) = 0 ) ) )
66 8 65 syl 
 |-  ( N e. NN0 -> ( K e. ( ZZ>= ` N ) -> ( A e. S -> ( C ` ( R ` K ) ) = 0 ) ) )
67 66 com3r 
 |-  ( A e. S -> ( N e. NN0 -> ( K e. ( ZZ>= ` N ) -> ( C ` ( R ` K ) ) = 0 ) ) )
68 7 67 mpd 
 |-  ( A e. S -> ( K e. ( ZZ>= ` N ) -> ( C ` ( R ` K ) ) = 0 ) )