Metamath Proof Explorer

Theorem climinf3

Description: A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 climinf3.1 
 |-  F/ k ph
2 climinf3.2 
 |-  F/_ k F
3 climinf3.3 
 |-  ( ph -> M e. ZZ )
4 climinf3.4 
 |-  Z = ( ZZ>= ` M )
5 climinf3.5 
 |-  ( ph -> F : Z --> RR )
6 climinf3.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
7 climinf3.7 
 |-  ( ph -> F e. dom ~~> )
8 5 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
9 8 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
10 1 9 ralrimia 
 |-  ( ph -> A. k e. Z ( F ` k ) e. CC )
11 2 4 climbddf 
 |-  ( ( M e. ZZ /\ F e. dom ~~> /\ A. k e. Z ( F ` k ) e. CC ) -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x )
12 3 7 10 11 syl3anc 
 |-  ( ph -> E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x )
13 renegcl 
 |-  ( x e. RR -> -u x e. RR )
14 13 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. Z ( abs ` ( F ` k ) ) <_ x ) -> -u x e. RR )
15 nfv 
 |-  F/ k x e. RR
16 1 15 nfan 
 |-  F/ k ( ph /\ x e. RR )
17 nfra1 
 |-  F/ k A. k e. Z ( abs ` ( F ` k ) ) <_ x
18 16 17 nfan 
 |-  F/ k ( ( ph /\ x e. RR ) /\ A. k e. Z ( abs ` ( F ` k ) ) <_ x )
19 simpll 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. k e. Z ( abs ` ( F ` k ) ) <_ x ) /\ k e. Z ) -> ( ph /\ x e. RR ) )
20 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. k e. Z ( abs ` ( F ` k ) ) <_ x ) /\ k e. Z ) -> k e. Z )
21 rspa 
 |-  ( ( A. k e. Z ( abs ` ( F ` k ) ) <_ x /\ k e. Z ) -> ( abs ` ( F ` k ) ) <_ x )
22 21 adantll 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. k e. Z ( abs ` ( F ` k ) ) <_ x ) /\ k e. Z ) -> ( abs ` ( F ` k ) ) <_ x )
23 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. Z ) /\ ( abs ` ( F ` k ) ) <_ x ) -> ( abs ` ( F ` k ) ) <_ x )
24 8 ad4ant13 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. Z ) /\ ( abs ` ( F ` k ) ) <_ x ) -> ( F ` k ) e. RR )
25 simpllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. Z ) /\ ( abs ` ( F ` k ) ) <_ x ) -> x e. RR )
26 24 25 absled 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. Z ) /\ ( abs ` ( F ` k ) ) <_ x ) -> ( ( abs ` ( F ` k ) ) <_ x <-> ( -u x <_ ( F ` k ) /\ ( F ` k ) <_ x ) ) )
27 23 26 mpbid 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. Z ) /\ ( abs ` ( F ` k ) ) <_ x ) -> ( -u x <_ ( F ` k ) /\ ( F ` k ) <_ x ) )
28 27 simpld 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. Z ) /\ ( abs ` ( F ` k ) ) <_ x ) -> -u x <_ ( F ` k ) )
29 19 20 22 28 syl21anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. k e. Z ( abs ` ( F ` k ) ) <_ x ) /\ k e. Z ) -> -u x <_ ( F ` k ) )
30 29 ex 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. Z ( abs ` ( F ` k ) ) <_ x ) -> ( k e. Z -> -u x <_ ( F ` k ) ) )
31 18 30 ralrimi 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. Z ( abs ` ( F ` k ) ) <_ x ) -> A. k e. Z -u x <_ ( F ` k ) )
32 breq1 
 |-  ( y = -u x -> ( y <_ ( F ` k ) <-> -u x <_ ( F ` k ) ) )
33 32 ralbidv 
 |-  ( y = -u x -> ( A. k e. Z y <_ ( F ` k ) <-> A. k e. Z -u x <_ ( F ` k ) ) )
34 33 rspcev 
 |-  ( ( -u x e. RR /\ A. k e. Z -u x <_ ( F ` k ) ) -> E. y e. RR A. k e. Z y <_ ( F ` k ) )
35 14 31 34 syl2anc 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. Z ( abs ` ( F ` k ) ) <_ x ) -> E. y e. RR A. k e. Z y <_ ( F ` k ) )
36 35 rexlimdva2 
 |-  ( ph -> ( E. x e. RR A. k e. Z ( abs ` ( F ` k ) ) <_ x -> E. y e. RR A. k e. Z y <_ ( F ` k ) ) )
37 12 36 mpd 
 |-  ( ph -> E. y e. RR A. k e. Z y <_ ( F ` k ) )
38 1 2 4 3 5 6 37 climinf2 
 |-  ( ph -> F ~~> inf ( ran F , RR* , < ) )