Metamath Proof Explorer

Theorem nn0seqcvgd

Description: A strictly-decreasing nonnegative integer sequence with initial term N reaches zero by the N th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Hypotheses nn0seqcvgd.1 
|- ( ph -> F : NN0 --> NN0 )
nn0seqcvgd.2 
|- ( ph -> N = ( F ` 0 ) )
nn0seqcvgd.3 
|- ( ( ph /\ k e. NN0 ) -> ( ( F ` ( k + 1 ) ) =/= 0 -> ( F ` ( k + 1 ) ) < ( F ` k ) ) )
Assertion nn0seqcvgd 
|- ( ph -> ( F ` N ) = 0 )

Proof

Step Hyp Ref Expression
1 nn0seqcvgd.1 
 |-  ( ph -> F : NN0 --> NN0 )
2 nn0seqcvgd.2 
 |-  ( ph -> N = ( F ` 0 ) )
3 nn0seqcvgd.3 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( F ` ( k + 1 ) ) =/= 0 -> ( F ` ( k + 1 ) ) < ( F ` k ) ) )
4 0nn0 
 |-  0 e. NN0
5 ffvelrn 
 |-  ( ( F : NN0 --> NN0 /\ 0 e. NN0 ) -> ( F ` 0 ) e. NN0 )
6 1 4 5 sylancl 
 |-  ( ph -> ( F ` 0 ) e. NN0 )
7 2 6 eqeltrd 
 |-  ( ph -> N e. NN0 )
8 7 nn0red 
 |-  ( ph -> N e. RR )
9 8 leidd 
 |-  ( ph -> N <_ N )
10 fveq2 
 |-  ( m = 0 -> ( F ` m ) = ( F ` 0 ) )
11 oveq2 
 |-  ( m = 0 -> ( N - m ) = ( N - 0 ) )
12 10 11 breq12d 
 |-  ( m = 0 -> ( ( F ` m ) <_ ( N - m ) <-> ( F ` 0 ) <_ ( N - 0 ) ) )
13 12 imbi2d 
 |-  ( m = 0 -> ( ( ph -> ( F ` m ) <_ ( N - m ) ) <-> ( ph -> ( F ` 0 ) <_ ( N - 0 ) ) ) )
14 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
15 oveq2 
 |-  ( m = k -> ( N - m ) = ( N - k ) )
16 14 15 breq12d 
 |-  ( m = k -> ( ( F ` m ) <_ ( N - m ) <-> ( F ` k ) <_ ( N - k ) ) )
17 16 imbi2d 
 |-  ( m = k -> ( ( ph -> ( F ` m ) <_ ( N - m ) ) <-> ( ph -> ( F ` k ) <_ ( N - k ) ) ) )
18 fveq2 
 |-  ( m = ( k + 1 ) -> ( F ` m ) = ( F ` ( k + 1 ) ) )
19 oveq2 
 |-  ( m = ( k + 1 ) -> ( N - m ) = ( N - ( k + 1 ) ) )
20 18 19 breq12d 
 |-  ( m = ( k + 1 ) -> ( ( F ` m ) <_ ( N - m ) <-> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
21 20 imbi2d 
 |-  ( m = ( k + 1 ) -> ( ( ph -> ( F ` m ) <_ ( N - m ) ) <-> ( ph -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) ) )
22 fveq2 
 |-  ( m = N -> ( F ` m ) = ( F ` N ) )
23 oveq2 
 |-  ( m = N -> ( N - m ) = ( N - N ) )
24 22 23 breq12d 
 |-  ( m = N -> ( ( F ` m ) <_ ( N - m ) <-> ( F ` N ) <_ ( N - N ) ) )
25 24 imbi2d 
 |-  ( m = N -> ( ( ph -> ( F ` m ) <_ ( N - m ) ) <-> ( ph -> ( F ` N ) <_ ( N - N ) ) ) )
26 2 9 eqbrtrrd 
 |-  ( ph -> ( F ` 0 ) <_ N )
27 8 recnd 
 |-  ( ph -> N e. CC )
28 27 subid1d 
 |-  ( ph -> ( N - 0 ) = N )
29 26 28 breqtrrd 
 |-  ( ph -> ( F ` 0 ) <_ ( N - 0 ) )
30 29 a1i 
 |-  ( N e. NN0 -> ( ph -> ( F ` 0 ) <_ ( N - 0 ) ) )
31 nn0re 
 |-  ( k e. NN0 -> k e. RR )
32 posdif 
 |-  ( ( k e. RR /\ N e. RR ) -> ( k < N <-> 0 < ( N - k ) ) )
33 31 8 32 syl2anr 
 |-  ( ( ph /\ k e. NN0 ) -> ( k < N <-> 0 < ( N - k ) ) )
34 33 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( F ` ( k + 1 ) ) = 0 ) -> ( k < N <-> 0 < ( N - k ) ) )
35 breq1 
 |-  ( ( F ` ( k + 1 ) ) = 0 -> ( ( F ` ( k + 1 ) ) < ( N - k ) <-> 0 < ( N - k ) ) )
36 35 adantl 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( F ` ( k + 1 ) ) = 0 ) -> ( ( F ` ( k + 1 ) ) < ( N - k ) <-> 0 < ( N - k ) ) )
37 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
38 ffvelrn 
 |-  ( ( F : NN0 --> NN0 /\ ( k + 1 ) e. NN0 ) -> ( F ` ( k + 1 ) ) e. NN0 )
39 1 37 38 syl2an 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` ( k + 1 ) ) e. NN0 )
40 39 nn0zd 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` ( k + 1 ) ) e. ZZ )
41 7 nn0zd 
 |-  ( ph -> N e. ZZ )
42 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
43 zsubcl 
 |-  ( ( N e. ZZ /\ k e. ZZ ) -> ( N - k ) e. ZZ )
44 41 42 43 syl2an 
 |-  ( ( ph /\ k e. NN0 ) -> ( N - k ) e. ZZ )
45 zltlem1 
 |-  ( ( ( F ` ( k + 1 ) ) e. ZZ /\ ( N - k ) e. ZZ ) -> ( ( F ` ( k + 1 ) ) < ( N - k ) <-> ( F ` ( k + 1 ) ) <_ ( ( N - k ) - 1 ) ) )
46 40 44 45 syl2anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( F ` ( k + 1 ) ) < ( N - k ) <-> ( F ` ( k + 1 ) ) <_ ( ( N - k ) - 1 ) ) )
47 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
48 ax-1cn 
 |-  1 e. CC
49 subsub4 
 |-  ( ( N e. CC /\ k e. CC /\ 1 e. CC ) -> ( ( N - k ) - 1 ) = ( N - ( k + 1 ) ) )
50 48 49 mp3an3 
 |-  ( ( N e. CC /\ k e. CC ) -> ( ( N - k ) - 1 ) = ( N - ( k + 1 ) ) )
51 27 47 50 syl2an 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( N - k ) - 1 ) = ( N - ( k + 1 ) ) )
52 51 breq2d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( F ` ( k + 1 ) ) <_ ( ( N - k ) - 1 ) <-> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
53 46 52 bitrd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( F ` ( k + 1 ) ) < ( N - k ) <-> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
54 53 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( F ` ( k + 1 ) ) = 0 ) -> ( ( F ` ( k + 1 ) ) < ( N - k ) <-> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
55 34 36 54 3bitr2d 
 |-  ( ( ( ph /\ k e. NN0 ) /\ ( F ` ( k + 1 ) ) = 0 ) -> ( k < N <-> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
56 55 biimpa 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ ( F ` ( k + 1 ) ) = 0 ) /\ k < N ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) )
57 56 an32s 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ k < N ) /\ ( F ` ( k + 1 ) ) = 0 ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) )
58 57 a1d 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ k < N ) /\ ( F ` ( k + 1 ) ) = 0 ) -> ( ( F ` k ) <_ ( N - k ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
59 39 nn0red 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` ( k + 1 ) ) e. RR )
60 1 ffvelrnda 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. NN0 )
61 60 nn0red 
 |-  ( ( ph /\ k e. NN0 ) -> ( F ` k ) e. RR )
62 44 zred 
 |-  ( ( ph /\ k e. NN0 ) -> ( N - k ) e. RR )
63 ltletr 
 |-  ( ( ( F ` ( k + 1 ) ) e. RR /\ ( F ` k ) e. RR /\ ( N - k ) e. RR ) -> ( ( ( F ` ( k + 1 ) ) < ( F ` k ) /\ ( F ` k ) <_ ( N - k ) ) -> ( F ` ( k + 1 ) ) < ( N - k ) ) )
64 59 61 62 63 syl3anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( F ` ( k + 1 ) ) < ( F ` k ) /\ ( F ` k ) <_ ( N - k ) ) -> ( F ` ( k + 1 ) ) < ( N - k ) ) )
65 64 53 sylibd 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( F ` ( k + 1 ) ) < ( F ` k ) /\ ( F ` k ) <_ ( N - k ) ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
66 3 65 syland 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( F ` ( k + 1 ) ) =/= 0 /\ ( F ` k ) <_ ( N - k ) ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
67 66 adantr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k < N ) -> ( ( ( F ` ( k + 1 ) ) =/= 0 /\ ( F ` k ) <_ ( N - k ) ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
68 67 expdimp 
 |-  ( ( ( ( ph /\ k e. NN0 ) /\ k < N ) /\ ( F ` ( k + 1 ) ) =/= 0 ) -> ( ( F ` k ) <_ ( N - k ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
69 58 68 pm2.61dane 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k < N ) -> ( ( F ` k ) <_ ( N - k ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
70 69 anasss 
 |-  ( ( ph /\ ( k e. NN0 /\ k < N ) ) -> ( ( F ` k ) <_ ( N - k ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) )
71 70 expcom 
 |-  ( ( k e. NN0 /\ k < N ) -> ( ph -> ( ( F ` k ) <_ ( N - k ) -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) ) )
72 71 a2d 
 |-  ( ( k e. NN0 /\ k < N ) -> ( ( ph -> ( F ` k ) <_ ( N - k ) ) -> ( ph -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) ) )
73 72 3adant1 
 |-  ( ( N e. NN0 /\ k e. NN0 /\ k < N ) -> ( ( ph -> ( F ` k ) <_ ( N - k ) ) -> ( ph -> ( F ` ( k + 1 ) ) <_ ( N - ( k + 1 ) ) ) ) )
74 13 17 21 25 30 73 fnn0ind 
 |-  ( ( N e. NN0 /\ N e. NN0 /\ N <_ N ) -> ( ph -> ( F ` N ) <_ ( N - N ) ) )
75 7 7 9 74 syl3anc 
 |-  ( ph -> ( ph -> ( F ` N ) <_ ( N - N ) ) )
76 75 pm2.43i 
 |-  ( ph -> ( F ` N ) <_ ( N - N ) )
77 27 subidd 
 |-  ( ph -> ( N - N ) = 0 )
78 76 77 breqtrd 
 |-  ( ph -> ( F ` N ) <_ 0 )
79 1 7 ffvelrnd 
 |-  ( ph -> ( F ` N ) e. NN0 )
80 79 nn0ge0d 
 |-  ( ph -> 0 <_ ( F ` N ) )
81 79 nn0red 
 |-  ( ph -> ( F ` N ) e. RR )
82 0re 
 |-  0 e. RR
83 letri3 
 |-  ( ( ( F ` N ) e. RR /\ 0 e. RR ) -> ( ( F ` N ) = 0 <-> ( ( F ` N ) <_ 0 /\ 0 <_ ( F ` N ) ) ) )
84 81 82 83 sylancl 
 |-  ( ph -> ( ( F ` N ) = 0 <-> ( ( F ` N ) <_ 0 /\ 0 <_ ( F ` N ) ) ) )
85 78 80 84 mpbir2and 
 |-  ( ph -> ( F ` N ) = 0 )