This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climinf2lem

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

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

Proof

Step Hyp Ref Expression
1 climinf2lem.1 
 |-  Z = ( ZZ>= ` M )
2 climinf2lem.2 
 |-  ( ph -> M e. ZZ )
3 climinf2lem.3 
 |-  ( ph -> F : Z --> RR )
4 climinf2lem.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` ( k + 1 ) ) <_ ( F ` k ) )
5 climinf2lem.5 
 |-  ( ph -> E. x e. RR A. k e. Z x <_ ( F ` k ) )
6 1 2 3 4 5 climinf 
 |-  ( ph -> F ~~> inf ( ran F , RR , < ) )
7 3 frnd 
 |-  ( ph -> ran F C_ RR )
8 3 ffnd 
 |-  ( ph -> F Fn Z )
9 2 1 uzidd2 
 |-  ( ph -> M e. Z )
10 fnfvelrn 
 |-  ( ( F Fn Z /\ M e. Z ) -> ( F ` M ) e. ran F )
11 8 9 10 syl2anc 
 |-  ( ph -> ( F ` M ) e. ran F )
12 11 ne0d 
 |-  ( ph -> ran F =/= (/) )
13 simpr 
 |-  ( ( ph /\ y e. ran F ) -> y e. ran F )
14 fvelrnb 
 |-  ( F Fn Z -> ( y e. ran F <-> E. k e. Z ( F ` k ) = y ) )
15 8 14 syl 
 |-  ( ph -> ( y e. ran F <-> E. k e. Z ( F ` k ) = y ) )
16 15 adantr 
 |-  ( ( ph /\ y e. ran F ) -> ( y e. ran F <-> E. k e. Z ( F ` k ) = y ) )
17 13 16 mpbid 
 |-  ( ( ph /\ y e. ran F ) -> E. k e. Z ( F ` k ) = y )
18 17 adantlr 
 |-  ( ( ( ph /\ A. k e. Z x <_ ( F ` k ) ) /\ y e. ran F ) -> E. k e. Z ( F ` k ) = y )
19 nfv 
 |-  F/ k ph
20 nfra1 
 |-  F/ k A. k e. Z x <_ ( F ` k )
21 19 20 nfan 
 |-  F/ k ( ph /\ A. k e. Z x <_ ( F ` k ) )
22 nfv 
 |-  F/ k x <_ y
23 rspa 
 |-  ( ( A. k e. Z x <_ ( F ` k ) /\ k e. Z ) -> x <_ ( F ` k ) )
24 simpl 
 |-  ( ( x <_ ( F ` k ) /\ ( F ` k ) = y ) -> x <_ ( F ` k ) )
25 simpr 
 |-  ( ( x <_ ( F ` k ) /\ ( F ` k ) = y ) -> ( F ` k ) = y )
26 24 25 breqtrd 
 |-  ( ( x <_ ( F ` k ) /\ ( F ` k ) = y ) -> x <_ y )
27 26 ex 
 |-  ( x <_ ( F ` k ) -> ( ( F ` k ) = y -> x <_ y ) )
28 23 27 syl 
 |-  ( ( A. k e. Z x <_ ( F ` k ) /\ k e. Z ) -> ( ( F ` k ) = y -> x <_ y ) )
29 28 ex 
 |-  ( A. k e. Z x <_ ( F ` k ) -> ( k e. Z -> ( ( F ` k ) = y -> x <_ y ) ) )
30 29 adantl 
 |-  ( ( ph /\ A. k e. Z x <_ ( F ` k ) ) -> ( k e. Z -> ( ( F ` k ) = y -> x <_ y ) ) )
31 21 22 30 rexlimd 
 |-  ( ( ph /\ A. k e. Z x <_ ( F ` k ) ) -> ( E. k e. Z ( F ` k ) = y -> x <_ y ) )
32 31 adantr 
 |-  ( ( ( ph /\ A. k e. Z x <_ ( F ` k ) ) /\ y e. ran F ) -> ( E. k e. Z ( F ` k ) = y -> x <_ y ) )
33 18 32 mpd 
 |-  ( ( ( ph /\ A. k e. Z x <_ ( F ` k ) ) /\ y e. ran F ) -> x <_ y )
34 33 ralrimiva 
 |-  ( ( ph /\ A. k e. Z x <_ ( F ` k ) ) -> A. y e. ran F x <_ y )
35 34 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ A. k e. Z x <_ ( F ` k ) ) -> A. y e. ran F x <_ y )
36 35 ex 
 |-  ( ( ph /\ x e. RR ) -> ( A. k e. Z x <_ ( F ` k ) -> A. y e. ran F x <_ y ) )
37 36 reximdva 
 |-  ( ph -> ( E. x e. RR A. k e. Z x <_ ( F ` k ) -> E. x e. RR A. y e. ran F x <_ y ) )
38 5 37 mpd 
 |-  ( ph -> E. x e. RR A. y e. ran F x <_ y )
39 infxrre 
 |-  ( ( ran F C_ RR /\ ran F =/= (/) /\ E. x e. RR A. y e. ran F x <_ y ) -> inf ( ran F , RR* , < ) = inf ( ran F , RR , < ) )
40 7 12 38 39 syl3anc 
 |-  ( ph -> inf ( ran F , RR* , < ) = inf ( ran F , RR , < ) )
41 6 40 breqtrrd 
 |-  ( ph -> F ~~> inf ( ran F , RR* , < ) )