Metamath Proof Explorer

Theorem climub

Description: The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 10-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 
|- Z = ( ZZ>= ` M )
climub.2 
|- ( ph -> N e. Z )
climub.3 
|- ( ph -> F ~~> A )
climub.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
climub.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
Assertion climub 
|- ( ph -> ( F ` N ) <_ A )

Proof

Step Hyp Ref Expression
1 clim2ser.1 
 |-  Z = ( ZZ>= ` M )
2 climub.2 
 |-  ( ph -> N e. Z )
3 climub.3 
 |-  ( ph -> F ~~> A )
4 climub.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
5 climub.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
6 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
7 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
8 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
9 7 8 syl 
 |-  ( ph -> N e. ZZ )
10 fveq2 
 |-  ( k = N -> ( F ` k ) = ( F ` N ) )
11 10 eleq1d 
 |-  ( k = N -> ( ( F ` k ) e. RR <-> ( F ` N ) e. RR ) )
12 11 imbi2d 
 |-  ( k = N -> ( ( ph -> ( F ` k ) e. RR ) <-> ( ph -> ( F ` N ) e. RR ) ) )
13 4 expcom 
 |-  ( k e. Z -> ( ph -> ( F ` k ) e. RR ) )
14 12 13 vtoclga 
 |-  ( N e. Z -> ( ph -> ( F ` N ) e. RR ) )
15 2 14 mpcom 
 |-  ( ph -> ( F ` N ) e. RR )
16 1 uztrn2 
 |-  ( ( N e. Z /\ j e. ( ZZ>= ` N ) ) -> j e. Z )
17 2 16 sylan 
 |-  ( ( ph /\ j e. ( ZZ>= ` N ) ) -> j e. Z )
18 fveq2 
 |-  ( k = j -> ( F ` k ) = ( F ` j ) )
19 18 eleq1d 
 |-  ( k = j -> ( ( F ` k ) e. RR <-> ( F ` j ) e. RR ) )
20 19 imbi2d 
 |-  ( k = j -> ( ( ph -> ( F ` k ) e. RR ) <-> ( ph -> ( F ` j ) e. RR ) ) )
21 20 13 vtoclga 
 |-  ( j e. Z -> ( ph -> ( F ` j ) e. RR ) )
22 21 impcom 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR )
23 17 22 syldan 
 |-  ( ( ph /\ j e. ( ZZ>= ` N ) ) -> ( F ` j ) e. RR )
24 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` N ) ) -> j e. ( ZZ>= ` N ) )
25 elfzuz 
 |-  ( k e. ( N ... j ) -> k e. ( ZZ>= ` N ) )
26 1 uztrn2 
 |-  ( ( N e. Z /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
27 2 26 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
28 27 4 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) e. RR )
29 25 28 sylan2 
 |-  ( ( ph /\ k e. ( N ... j ) ) -> ( F ` k ) e. RR )
30 29 adantlr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( N ... j ) ) -> ( F ` k ) e. RR )
31 elfzuz 
 |-  ( k e. ( N ... ( j - 1 ) ) -> k e. ( ZZ>= ` N ) )
32 27 5 syldan 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
33 31 32 sylan2 
 |-  ( ( ph /\ k e. ( N ... ( j - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
34 33 adantlr 
 |-  ( ( ( ph /\ j e. ( ZZ>= ` N ) ) /\ k e. ( N ... ( j - 1 ) ) ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
35 24 30 34 monoord 
 |-  ( ( ph /\ j e. ( ZZ>= ` N ) ) -> ( F ` N ) <_ ( F ` j ) )
36 6 9 15 3 23 35 climlec2 
 |-  ( ph -> ( F ` N ) <_ A )