Metamath Proof Explorer

Theorem climinf

Description: A bounded monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Revised by AV, 15-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 climinf.3 
 |-  Z = ( ZZ>= ` M )
2 climinf.4 
 |-  ( ph -> M e. ZZ )
3 climinf.5 
 |-  ( ph -> F : Z --> RR )
4 climinf.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
5 climinf.7 
 |-  ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )
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 breq2 
 |-  ( y = ( F ` k ) -> ( x <_ y <-> x <_ ( F ` k ) ) )
15 14 ralrn 
 |-  ( F Fn Z -> ( A. y e. ran F x <_ y <-> A. k e. Z x <_ ( F ` k ) ) )
16 15 rexbidv 
 |-  ( F Fn Z -> ( E. x e. RR A. y e. ran F x <_ y <-> E. x e. RR A. k e. Z x <_ ( F ` k ) ) )
17 7 16 syl 
 |-  ( ph -> ( E. x e. RR A. y e. ran F x <_ y <-> E. x e. RR A. k e. Z x <_ ( F ` k ) ) )
18 5 17 mpbird 
 |-  ( ph -> E. x e. RR A. y e. ran F x <_ y )
19 6 13 18 3jca 
 |-  ( ph -> ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F x <_ y ) )
20 19 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F x <_ y ) )
21 infrecl 
 |-  ( ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F x <_ y ) -> inf ( ran F , RR , < ) e. RR )
22 20 21 syl 
 |-  ( ( ph /\ y e. RR+ ) -> inf ( ran F , RR , < ) e. RR )
23 simpr 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR+ )
24 22 23 ltaddrpd 
 |-  ( ( ph /\ y e. RR+ ) -> inf ( ran F , RR , < ) < ( inf ( ran F , RR , < ) + y ) )
25 rpre 
 |-  ( y e. RR+ -> y e. RR )
26 25 adantl 
 |-  ( ( ph /\ y e. RR+ ) -> y e. RR )
27 22 26 readdcld 
 |-  ( ( ph /\ y e. RR+ ) -> ( inf ( ran F , RR , < ) + y ) e. RR )
28 infrglb 
 |-  ( ( ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F x <_ y ) /\ ( inf ( ran F , RR , < ) + y ) e. RR ) -> ( inf ( ran F , RR , < ) < ( inf ( ran F , RR , < ) + y ) <-> E. k e. ran F k < ( inf ( ran F , RR , < ) + y ) ) )
29 20 27 28 syl2anc 
 |-  ( ( ph /\ y e. RR+ ) -> ( inf ( ran F , RR , < ) < ( inf ( ran F , RR , < ) + y ) <-> E. k e. ran F k < ( inf ( ran F , RR , < ) + y ) ) )
30 24 29 mpbid 
 |-  ( ( ph /\ y e. RR+ ) -> E. k e. ran F k < ( inf ( ran F , RR , < ) + y ) )
31 6 sselda 
 |-  ( ( ph /\ k e. ran F ) -> k e. RR )
32 31 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> k e. RR )
33 22 adantr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> inf ( ran F , RR , < ) e. RR )
34 25 ad2antlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> y e. RR )
35 33 34 readdcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> ( inf ( ran F , RR , < ) + y ) e. RR )
36 32 35 34 ltsub1d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> ( k < ( inf ( ran F , RR , < ) + y ) <-> ( k - y ) < ( ( inf ( ran F , RR , < ) + y ) - y ) ) )
37 6 13 18 21 syl3anc 
 |-  ( ph -> inf ( ran F , RR , < ) e. RR )
38 37 recnd 
 |-  ( ph -> inf ( ran F , RR , < ) e. CC )
39 38 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> inf ( ran F , RR , < ) e. CC )
40 34 recnd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> y e. CC )
41 39 40 pncand 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> ( ( inf ( ran F , RR , < ) + y ) - y ) = inf ( ran F , RR , < ) )
42 41 breq2d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> ( ( k - y ) < ( ( inf ( ran F , RR , < ) + y ) - y ) <-> ( k - y ) < inf ( ran F , RR , < ) ) )
43 36 42 bitrd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> ( k < ( inf ( ran F , RR , < ) + y ) <-> ( k - y ) < inf ( ran F , RR , < ) ) )
44 43 biimpd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ k e. ran F ) -> ( k < ( inf ( ran F , RR , < ) + y ) -> ( k - y ) < inf ( ran F , RR , < ) ) )
45 44 reximdva 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. k e. ran F k < ( inf ( ran F , RR , < ) + y ) -> E. k e. ran F ( k - y ) < inf ( ran F , RR , < ) ) )
46 30 45 mpd 
 |-  ( ( ph /\ y e. RR+ ) -> E. k e. ran F ( k - y ) < inf ( ran F , RR , < ) )
47 oveq1 
 |-  ( k = ( F ` j ) -> ( k - y ) = ( ( F ` j ) - y ) )
48 47 breq1d 
 |-  ( k = ( F ` j ) -> ( ( k - y ) < inf ( ran F , RR , < ) <-> ( ( F ` j ) - y ) < inf ( ran F , RR , < ) ) )
49 48 rexrn 
 |-  ( F Fn Z -> ( E. k e. ran F ( k - y ) < inf ( ran F , RR , < ) <-> E. j e. Z ( ( F ` j ) - y ) < inf ( ran F , RR , < ) ) )
50 7 49 syl 
 |-  ( ph -> ( E. k e. ran F ( k - y ) < inf ( ran F , RR , < ) <-> E. j e. Z ( ( F ` j ) - y ) < inf ( ran F , RR , < ) ) )
51 50 biimpa 
 |-  ( ( ph /\ E. k e. ran F ( k - y ) < inf ( ran F , RR , < ) ) -> E. j e. Z ( ( F ` j ) - y ) < inf ( ran F , RR , < ) )
52 46 51 syldan 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z ( ( F ` j ) - y ) < inf ( ran F , RR , < ) )
53 3 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> F : Z --> RR )
54 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
55 ffvelcdm 
 |-  ( ( F : Z --> RR /\ k e. Z ) -> ( F ` k ) e. RR )
56 53 54 55 syl2an 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. RR )
57 simpl 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> j e. Z )
58 ffvelcdm 
 |-  ( ( F : Z --> RR /\ j e. Z ) -> ( F ` j ) e. RR )
59 53 57 58 syl2an 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` j ) e. RR )
60 37 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> inf ( ran F , RR , < ) e. RR )
61 simprr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> k e. ( ZZ>= ` j ) )
62 fzssuz 
 |-  ( j ... k ) C_ ( ZZ>= ` j )
63 uzss 
 |-  ( j e. ( ZZ>= ` M ) -> ( ZZ>= ` j ) C_ ( ZZ>= ` M ) )
64 63 1 sseqtrrdi 
 |-  ( j e. ( ZZ>= ` M ) -> ( ZZ>= ` j ) C_ Z )
65 64 1 eleq2s 
 |-  ( j e. Z -> ( ZZ>= ` j ) C_ Z )
66 65 ad2antrl 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ZZ>= ` j ) C_ Z )
67 62 66 sstrid 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( j ... k ) C_ Z )
68 ffvelcdm 
 |-  ( ( F : Z --> RR /\ n e. Z ) -> ( F ` n ) e. RR )
69 68 ralrimiva 
 |-  ( F : Z --> RR -> A. n e. Z ( F ` n ) e. RR )
70 3 69 syl 
 |-  ( ph -> A. n e. Z ( F ` n ) e. RR )
71 70 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> A. n e. Z ( F ` n ) e. RR )
72 ssralv 
 |-  ( ( j ... k ) C_ Z -> ( A. n e. Z ( F ` n ) e. RR -> A. n e. ( j ... k ) ( F ` n ) e. RR ) )
73 67 71 72 sylc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> A. n e. ( j ... k ) ( F ` n ) e. RR )
74 73 r19.21bi 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) /\ n e. ( j ... k ) ) -> ( F ` n ) e. RR )
75 fzssuz 
 |-  ( j ... ( k - 1 ) ) C_ ( ZZ>= ` j )
76 75 66 sstrid 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( j ... ( k - 1 ) ) C_ Z )
77 76 sselda 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) /\ n e. ( j ... ( k - 1 ) ) ) -> n e. Z )
78 4 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` ( k + 1 ) ) <_ ( F ` k ) )
79 78 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> A. k e. Z ( F ` ( k + 1 ) ) <_ ( F ` k ) )
80 fvoveq1 
 |-  ( k = n -> ( F ` ( k + 1 ) ) = ( F ` ( n + 1 ) ) )
81 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
82 80 81 breq12d 
 |-  ( k = n -> ( ( F ` ( k + 1 ) ) <_ ( F ` k ) <-> ( F ` ( n + 1 ) ) <_ ( F ` n ) ) )
83 82 rspccva 
 |-  ( ( A. k e. Z ( F ` ( k + 1 ) ) <_ ( F ` k ) /\ n e. Z ) -> ( F ` ( n + 1 ) ) <_ ( F ` n ) )
84 79 83 sylan 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) /\ n e. Z ) -> ( F ` ( n + 1 ) ) <_ ( F ` n ) )
85 77 84 syldan 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) /\ n e. ( j ... ( k - 1 ) ) ) -> ( F ` ( n + 1 ) ) <_ ( F ` n ) )
86 61 74 85 monoord2 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) <_ ( F ` j ) )
87 56 59 60 86 lesub1dd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( F ` k ) - inf ( ran F , RR , < ) ) <_ ( ( F ` j ) - inf ( ran F , RR , < ) ) )
88 56 60 resubcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( F ` k ) - inf ( ran F , RR , < ) ) e. RR )
89 59 60 resubcld 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( F ` j ) - inf ( ran F , RR , < ) ) e. RR )
90 25 ad2antlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> y e. RR )
91 lelttr 
 |-  ( ( ( ( F ` k ) - inf ( ran F , RR , < ) ) e. RR /\ ( ( F ` j ) - inf ( ran F , RR , < ) ) e. RR /\ y e. RR ) -> ( ( ( ( F ` k ) - inf ( ran F , RR , < ) ) <_ ( ( F ` j ) - inf ( ran F , RR , < ) ) /\ ( ( F ` j ) - inf ( ran F , RR , < ) ) < y ) -> ( ( F ` k ) - inf ( ran F , RR , < ) ) < y ) )
92 88 89 90 91 syl3anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( ( F ` k ) - inf ( ran F , RR , < ) ) <_ ( ( F ` j ) - inf ( ran F , RR , < ) ) /\ ( ( F ` j ) - inf ( ran F , RR , < ) ) < y ) -> ( ( F ` k ) - inf ( ran F , RR , < ) ) < y ) )
93 87 92 mpand 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( F ` j ) - inf ( ran F , RR , < ) ) < y -> ( ( F ` k ) - inf ( ran F , RR , < ) ) < y ) )
94 ltsub23 
 |-  ( ( ( F ` j ) e. RR /\ y e. RR /\ inf ( ran F , RR , < ) e. RR ) -> ( ( ( F ` j ) - y ) < inf ( ran F , RR , < ) <-> ( ( F ` j ) - inf ( ran F , RR , < ) ) < y ) )
95 59 90 60 94 syl3anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( F ` j ) - y ) < inf ( ran F , RR , < ) <-> ( ( F ` j ) - inf ( ran F , RR , < ) ) < y ) )
96 6 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ran F C_ RR )
97 7 adantr 
 |-  ( ( ph /\ y e. RR+ ) -> F Fn Z )
98 fnfvelrn 
 |-  ( ( F Fn Z /\ k e. Z ) -> ( F ` k ) e. ran F )
99 97 54 98 syl2an 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. ran F )
100 96 99 sseldd 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( F ` k ) e. RR )
101 18 ad2antrr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> E. x e. RR A. y e. ran F x <_ y )
102 infrelb 
 |-  ( ( ran F C_ RR /\ E. x e. RR A. y e. ran F x <_ y /\ ( F ` k ) e. ran F ) -> inf ( ran F , RR , < ) <_ ( F ` k ) )
103 96 101 99 102 syl3anc 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> inf ( ran F , RR , < ) <_ ( F ` k ) )
104 60 100 103 abssubge0d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( abs ` ( ( F ` k ) - inf ( ran F , RR , < ) ) ) = ( ( F ` k ) - inf ( ran F , RR , < ) ) )
105 104 breq1d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( abs ` ( ( F ` k ) - inf ( ran F , RR , < ) ) ) < y <-> ( ( F ` k ) - inf ( ran F , RR , < ) ) < y ) )
106 93 95 105 3imtr4d 
 |-  ( ( ( ph /\ y e. RR+ ) /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( ( ( F ` j ) - y ) < inf ( ran F , RR , < ) -> ( abs ` ( ( F ` k ) - inf ( ran F , RR , < ) ) ) < y ) )
107 106 anassrs 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( F ` j ) - y ) < inf ( ran F , RR , < ) -> ( abs ` ( ( F ` k ) - inf ( ran F , RR , < ) ) ) < y ) )
108 107 ralrimdva 
 |-  ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) -> ( ( ( F ` j ) - y ) < inf ( ran F , RR , < ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - inf ( ran F , RR , < ) ) ) < y ) )
109 108 reximdva 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. j e. Z ( ( F ` j ) - y ) < inf ( ran F , RR , < ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - inf ( ran F , RR , < ) ) ) < y ) )
110 52 109 mpd 
 |-  ( ( ph /\ y e. RR+ ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - inf ( ran F , RR , < ) ) ) < y )
111 110 ralrimiva 
 |-  ( ph -> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - inf ( ran F , RR , < ) ) ) < y )
112 1 fvexi 
 |-  Z e. _V
113 fex 
 |-  ( ( F : Z --> RR /\ Z e. _V ) -> F e. _V )
114 3 112 113 sylancl 
 |-  ( ph -> F e. _V )
115 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
116 3 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
117 116 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
118 1 2 114 115 38 117 clim2c 
 |-  ( ph -> ( F ~~> inf ( ran F , RR , < ) <-> A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - inf ( ran F , RR , < ) ) ) < y ) )
119 111 118 mpbird 
 |-  ( ph -> F ~~> inf ( ran F , RR , < ) )