Metamath Proof Explorer

Theorem climsup

Description: A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of Gleason p. 180. (Contributed by NM, 13-Mar-2005) (Revised by Mario Carneiro, 10-Feb-2014)

Ref Expression
Hypotheses climsup.1 
|- Z = ( ZZ>= ` M )
climsup.2 
|- ( ph -> M e. ZZ )
climsup.3 
|- ( ph -> F : Z --> RR )
climsup.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
climsup.5 
|- ( ph -> E. x e. RR A. k e. Z ( F ` k ) <_ x )
Assertion climsup 
|- ( ph -> F ~~> sup ( ran F , RR , < ) )

Proof

Step Hyp Ref Expression
1 climsup.1 
 |-  Z = ( ZZ>= ` M )
2 climsup.2 
 |-  ( ph -> M e. ZZ )
3 climsup.3 
 |-  ( ph -> F : Z --> RR )
4 climsup.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) <_ ( F ` ( k + 1 ) ) )
5 climsup.5 
 |-  ( ph -> E. x e. RR A. k e. Z ( F ` k ) <_ x )
6 3 frnd 
 |-  ( ph -> ran F C_ RR )
7 3 ffnd 
 |-  ( ph -> F Fn Z )
8 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
9 2 8 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
10 9 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
11 fnfvelrn 
 |-  ( ( F Fn Z /\ M e. Z ) -> ( F ` M ) e. ran F )
12 7 10 11 syl2anc 
 |-  ( ph -> ( F ` M ) e. ran F )
13 12 ne0d 
 |-  ( ph -> ran F =/= (/) )
14 breq1 
 |-  ( y = ( F ` k ) -> ( y <_ x <-> ( F ` k ) <_ x ) )
15 14 ralrn 
 |-  ( F Fn Z -> ( A. y e. ran F y <_ x <-> A. k e. Z ( F ` k ) <_ x ) )
16 15 rexbidv 
 |-  ( F Fn Z -> ( E. x e. RR A. y e. ran F y <_ x <-> E. x e. RR A. k e. Z ( F ` k ) <_ x ) )
17 7 16 syl 
 |-  ( ph -> ( E. x e. RR A. y e. ran F y <_ x <-> E. x e. RR A. k e. Z ( F ` k ) <_ x ) )
18 5 17 mpbird 
 |-  ( ph -> E. x e. RR A. y e. ran F y <_ x )
19 6 13 18 3jca 
 |-  ( ph -> ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F y <_ x ) )
20 suprcl 
 |-  ( ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F y <_ x ) -> sup ( ran F , RR , < ) e. RR )
21 19 20 syl 
 |-  ( ph -> sup ( ran F , RR , < ) e. RR )
22 ltsubrp 
 |-  ( ( sup ( ran F , RR , < ) e. RR /\ y e. RR+ ) -> ( sup ( ran F , RR , < ) - y ) < sup ( ran F , RR , < ) )
23 21 22 sylan 
 |-  ( ( ph /\ y e. RR+ ) -> ( sup ( ran F , RR , < ) - y ) < sup ( ran F , RR , < ) )
24 19 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F y <_ x ) )
25 rpre 
 |-  ( y e. RR+ -> y e. RR )
26 resubcl 
 |-  ( ( sup ( ran F , RR , < ) e. RR /\ y e. RR ) -> ( sup ( ran F , RR , < ) - y ) e. RR )
27 21 25 26 syl2an 
 |-  ( ( ph /\ y e. RR+ ) -> ( sup ( ran F , RR , < ) - y ) e. RR )
28 suprlub 
 |-  ( ( ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F y <_ x ) /\ ( sup ( ran F , RR , < ) - y ) e. RR ) -> ( ( sup ( ran F , RR , < ) - y ) < sup ( ran F , RR , < ) <-> E. k e. ran F ( sup ( ran F , RR , < ) - y ) < k ) )
29 24 27 28 syl2anc 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( sup ( ran F , RR , < ) - y ) < sup ( ran F , RR , < ) <-> E. k e. ran F ( sup ( ran F , RR , < ) - y ) < k ) )
30 23 29 mpbid 
 |-  ( ( ph /\ y e. RR+ ) -> E. k e. ran F ( sup ( ran F , RR , < ) - y ) < k )
31 breq2 
 |-  ( k = ( F ` j ) -> ( ( sup ( ran F , RR , < ) - y ) < k <-> ( sup ( ran F , RR , < ) - y ) < ( F ` j ) ) )
32 31 rexrn 
 |-  ( F Fn Z -> ( E. k e. ran F ( sup ( ran F , RR , < ) - y ) < k <-> E. j e. Z ( sup ( ran F , RR , < ) - y ) < ( F ` j ) ) )
33 7 32 syl 
 |-  ( ph -> ( E. k e. ran F ( sup ( ran F , RR , < ) - y ) < k <-> E. j e. Z ( sup ( ran F , RR , < ) - y ) < ( F ` j ) ) )
34 33 biimpa 
 |-  ( ( ph /\ E. k e. ran F ( sup ( ran F , RR , < ) - y ) < k ) -> E. j e. Z ( sup ( ran F , RR , < ) - y ) < ( F ` j ) )
35 30 34 syldan 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z ( sup ( ran F , RR , < ) - y ) < ( F ` j ) )
36 ffvelrn 
 |-  ( ( F : Z --> RR /\ j e. Z ) -> ( F ` j ) e. RR )
37 3 36 sylan 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR )
38 37 ad2ant2r 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` j ) e. RR )
39 3 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> F : Z --> RR )
40 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
41 ffvelrn 
 |-  ( ( F : Z --> RR /\ k e. Z ) -> ( F ` k ) e. RR )
42 39 40 41 syl2an 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. RR )
43 21 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> sup ( ran F , RR , < ) e. RR )
44 simprr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> k e. ( ZZ>= ` j ) )
45 fzssuz 
 |-  ( j ... k ) C_ ( ZZ>= ` j )
46 uzss 
 |-  ( j e. ( ZZ>= ` M ) -> ( ZZ>= ` j ) C_ ( ZZ>= ` M ) )
47 46 1 sseqtrrdi 
 |-  ( j e. ( ZZ>= ` M ) -> ( ZZ>= ` j ) C_ Z )
48 47 1 eleq2s 
 |-  ( j e. Z -> ( ZZ>= ` j ) C_ Z )
49 48 ad2antrl 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ZZ>= ` j ) C_ Z )
50 45 49 sstrid 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( j ... k ) C_ Z )
51 ffvelrn 
 |-  ( ( F : Z --> RR /\ n e. Z ) -> ( F ` n ) e. RR )
52 51 ralrimiva 
 |-  ( F : Z --> RR -> A. n e. Z ( F ` n ) e. RR )
53 3 52 syl 
 |-  ( ph -> A. n e. Z ( F ` n ) e. RR )
54 53 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> A. n e. Z ( F ` n ) e. RR )
55 ssralv 
 |-  ( ( j ... k ) C_ Z -> ( A. n e. Z ( F ` n ) e. RR -> A. n e. ( j ... k ) ( F ` n ) e. RR ) )
56 50 54 55 sylc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> A. n e. ( j ... k ) ( F ` n ) e. RR )
57 56 r19.21bi 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) /\ n e. ( j ... k ) ) -> ( F ` n ) e. RR )
58 fzssuz 
 |-  ( j ... ( k - 1 ) ) C_ ( ZZ>= ` j )
59 58 49 sstrid 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( j ... ( k - 1 ) ) C_ Z )
60 59 sselda 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) /\ n e. ( j ... ( k - 1 ) ) ) -> n e. Z )
61 4 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) <_ ( F ` ( k + 1 ) ) )
62 61 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> A. k e. Z ( F ` k ) <_ ( F ` ( k + 1 ) ) )
63 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
64 fvoveq1 
 |-  ( k = n -> ( F ` ( k + 1 ) ) = ( F ` ( n + 1 ) ) )
65 63 64 breq12d 
 |-  ( k = n -> ( ( F ` k ) <_ ( F ` ( k + 1 ) ) <-> ( F ` n ) <_ ( F ` ( n + 1 ) ) ) )
66 65 rspccva 
 |-  ( ( A. k e. Z ( F ` k ) <_ ( F ` ( k + 1 ) ) /\ n e. Z ) -> ( F ` n ) <_ ( F ` ( n + 1 ) ) )
67 62 66 sylan 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) /\ n e. Z ) -> ( F ` n ) <_ ( F ` ( n + 1 ) ) )
68 60 67 syldan 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) /\ n e. ( j ... ( k - 1 ) ) ) -> ( F ` n ) <_ ( F ` ( n + 1 ) ) )
69 44 57 68 monoord 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` j ) <_ ( F ` k ) )
70 38 42 43 69 lesub2dd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( sup ( ran F , RR , < ) - ( F ` k ) ) <_ ( sup ( ran F , RR , < ) - ( F ` j ) ) )
71 43 42 resubcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( sup ( ran F , RR , < ) - ( F ` k ) ) e. RR )
72 43 38 resubcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( sup ( ran F , RR , < ) - ( F ` j ) ) e. RR )
73 25 ad2antlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> y e. RR )
74 lelttr 
 |-  ( ( ( sup ( ran F , RR , < ) - ( F ` k ) ) e. RR /\ ( sup ( ran F , RR , < ) - ( F ` j ) ) e. RR /\ y e. RR ) -> ( ( ( sup ( ran F , RR , < ) - ( F ` k ) ) <_ ( sup ( ran F , RR , < ) - ( F ` j ) ) /\ ( sup ( ran F , RR , < ) - ( F ` j ) ) < y ) -> ( sup ( ran F , RR , < ) - ( F ` k ) ) < y ) )
75 71 72 73 74 syl3anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( sup ( ran F , RR , < ) - ( F ` k ) ) <_ ( sup ( ran F , RR , < ) - ( F ` j ) ) /\ ( sup ( ran F , RR , < ) - ( F ` j ) ) < y ) -> ( sup ( ran F , RR , < ) - ( F ` k ) ) < y ) )
76 70 75 mpand 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( sup ( ran F , RR , < ) - ( F ` j ) ) < y -> ( sup ( ran F , RR , < ) - ( F ` k ) ) < y ) )
77 ltsub23 
 |-  ( ( sup ( ran F , RR , < ) e. RR /\ y e. RR /\ ( F ` j ) e. RR ) -> ( ( sup ( ran F , RR , < ) - y ) < ( F ` j ) <-> ( sup ( ran F , RR , < ) - ( F ` j ) ) < y ) )
78 43 73 38 77 syl3anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( sup ( ran F , RR , < ) - y ) < ( F ` j ) <-> ( sup ( ran F , RR , < ) - ( F ` j ) ) < y ) )
79 19 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F y <_ x ) )
80 7 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> F Fn Z )
81 fnfvelrn 
 |-  ( ( F Fn Z /\ k e. Z ) -> ( F ` k ) e. ran F )
82 80 40 81 syl2an 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. ran F )
83 suprub 
 |-  ( ( ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F y <_ x ) /\ ( F ` k ) e. ran F ) -> ( F ` k ) <_ sup ( ran F , RR , < ) )
84 79 82 83 syl2anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) <_ sup ( ran F , RR , < ) )
85 42 43 84 abssuble0d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( F ` k ) - sup ( ran F , RR , < ) ) ) = ( sup ( ran F , RR , < ) - ( F ` k ) ) )
86 85 breq1d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( F ` k ) - sup ( ran F , RR , < ) ) ) < y <-> ( sup ( ran F , RR , < ) - ( F ` k ) ) < y ) )
87 76 78 86 3imtr4d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( sup ( ran F , RR , < ) - y ) < ( F ` j ) -> ( abs ` ( ( F ` k ) - sup ( ran F , RR , < ) ) ) < y ) )
88 87 anassrs 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( sup ( ran F , RR , < ) - y ) < ( F ` j ) -> ( abs ` ( ( F ` k ) - sup ( ran F , RR , < ) ) ) < y ) )
89 88 ralrimdva 
 |-  ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) -> ( ( sup ( ran F , RR , < ) - y ) < ( F ` j ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - sup ( ran F , RR , < ) ) ) < y ) )
90 89 reximdva 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. j e. Z ( sup ( ran F , RR , < ) - y ) < ( F ` j ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - sup ( ran F , RR , < ) ) ) < y ) )
91 35 90 mpd 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - sup ( ran F , RR , < ) ) ) < y )
92 91 ralrimiva 
 |-  ( ph -> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - sup ( ran F , RR , < ) ) ) < y )
93 1 fvexi 
 |-  Z e. _V
94 fex 
 |-  ( ( F : Z --> RR /\ Z e. _V ) -> F e. _V )
95 3 93 94 sylancl 
 |-  ( ph -> F e. _V )
96 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
97 21 recnd 
 |-  ( ph -> sup ( ran F , RR , < ) e. CC )
98 3 41 sylan 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
99 98 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
100 1 2 95 96 97 99 clim2c 
 |-  ( ph -> ( F ~~> sup ( ran F , RR , < ) <-> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - sup ( ran F , RR , < ) ) ) < y ) )
101 92 100 mpbird 
 |-  ( ph -> F ~~> sup ( ran F , RR , < ) )