Metamath Proof Explorer

Theorem climinf2mpt

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

Ref Expression
Hypotheses climinf2mpt.p 
|- F/ k ph
climinf2mpt.j 
|- F/ j ph
climinf2mpt.m 
|- ( ph -> M e. ZZ )
climinf2mpt.z 
|- Z = ( ZZ>= ` M )
climinf2mpt.b 
|- ( ( ph /\ k e. Z ) -> B e. RR )
climinf2mpt.c 
|- ( k = j -> B = C )
climinf2mpt.l 
|- ( ( ph /\ k e. Z /\ j = ( k + 1 ) ) -> C <_ B )
climinf2mpt.e 
|- ( ph -> ( k e. Z |-> B ) e. dom ~~> )
Assertion climinf2mpt 
|- ( ph -> ( k e. Z |-> B ) ~~> inf ( ran ( k e. Z |-> B ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 climinf2mpt.p 
 |-  F/ k ph
2 climinf2mpt.j 
 |-  F/ j ph
3 climinf2mpt.m 
 |-  ( ph -> M e. ZZ )
4 climinf2mpt.z 
 |-  Z = ( ZZ>= ` M )
5 climinf2mpt.b 
 |-  ( ( ph /\ k e. Z ) -> B e. RR )
6 climinf2mpt.c 
 |-  ( k = j -> B = C )
7 climinf2mpt.l 
 |-  ( ( ph /\ k e. Z /\ j = ( k + 1 ) ) -> C <_ B )
8 climinf2mpt.e 
 |-  ( ph -> ( k e. Z |-> B ) e. dom ~~> )
9 nfv 
 |-  F/ i ph
10 nfcv 
 |-  F/_ i ( k e. Z |-> B )
11 1 5 fmptd2f 
 |-  ( ph -> ( k e. Z |-> B ) : Z --> RR )
12 nfv 
 |-  F/ k i e. Z
13 1 12 nfan 
 |-  F/ k ( ph /\ i e. Z )
14 nfv 
 |-  F/ k [_ ( i + 1 ) / j ]_ C <_ [_ i / j ]_ C
15 13 14 nfim 
 |-  F/ k ( ( ph /\ i e. Z ) -> [_ ( i + 1 ) / j ]_ C <_ [_ i / j ]_ C )
16 eleq1 
 |-  ( k = i -> ( k e. Z <-> i e. Z ) )
17 16 anbi2d 
 |-  ( k = i -> ( ( ph /\ k e. Z ) <-> ( ph /\ i e. Z ) ) )
18 oveq1 
 |-  ( k = i -> ( k + 1 ) = ( i + 1 ) )
19 18 csbeq1d 
 |-  ( k = i -> [_ ( k + 1 ) / j ]_ C = [_ ( i + 1 ) / j ]_ C )
20 eqidd 
 |-  ( k = i -> B = B )
21 csbcow 
 |-  [_ k / j ]_ [_ j / k ]_ B = [_ k / k ]_ B
22 csbid 
 |-  [_ k / k ]_ B = B
23 21 22 eqtr2i 
 |-  B = [_ k / j ]_ [_ j / k ]_ B
24 nfcv 
 |-  F/_ j B
25 nfcv 
 |-  F/_ k C
26 24 25 6 cbvcsbw 
 |-  [_ j / k ]_ B = [_ j / j ]_ C
27 csbid 
 |-  [_ j / j ]_ C = C
28 26 27 eqtri 
 |-  [_ j / k ]_ B = C
29 28 csbeq2i 
 |-  [_ k / j ]_ [_ j / k ]_ B = [_ k / j ]_ C
30 23 29 eqtri 
 |-  B = [_ k / j ]_ C
31 30 a1i 
 |-  ( k = i -> B = [_ k / j ]_ C )
32 csbeq1 
 |-  ( k = i -> [_ k / j ]_ C = [_ i / j ]_ C )
33 20 31 32 3eqtrd 
 |-  ( k = i -> B = [_ i / j ]_ C )
34 19 33 breq12d 
 |-  ( k = i -> ( [_ ( k + 1 ) / j ]_ C <_ B <-> [_ ( i + 1 ) / j ]_ C <_ [_ i / j ]_ C ) )
35 17 34 imbi12d 
 |-  ( k = i -> ( ( ( ph /\ k e. Z ) -> [_ ( k + 1 ) / j ]_ C <_ B ) <-> ( ( ph /\ i e. Z ) -> [_ ( i + 1 ) / j ]_ C <_ [_ i / j ]_ C ) ) )
36 simpl 
 |-  ( ( ph /\ k e. Z ) -> ph )
37 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
38 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( k + 1 ) = ( k + 1 ) )
39 nfv 
 |-  F/ j k e. Z
40 nfv 
 |-  F/ j ( k + 1 ) = ( k + 1 )
41 2 39 40 nf3an 
 |-  F/ j ( ph /\ k e. Z /\ ( k + 1 ) = ( k + 1 ) )
42 nfcsb1v 
 |-  F/_ j [_ ( k + 1 ) / j ]_ C
43 nfcv 
 |-  F/_ j <_
44 42 43 24 nfbr 
 |-  F/ j [_ ( k + 1 ) / j ]_ C <_ B
45 41 44 nfim 
 |-  F/ j ( ( ph /\ k e. Z /\ ( k + 1 ) = ( k + 1 ) ) -> [_ ( k + 1 ) / j ]_ C <_ B )
46 ovex 
 |-  ( k + 1 ) e. _V
47 eqeq1 
 |-  ( j = ( k + 1 ) -> ( j = ( k + 1 ) <-> ( k + 1 ) = ( k + 1 ) ) )
48 47 3anbi3d 
 |-  ( j = ( k + 1 ) -> ( ( ph /\ k e. Z /\ j = ( k + 1 ) ) <-> ( ph /\ k e. Z /\ ( k + 1 ) = ( k + 1 ) ) ) )
49 csbeq1a 
 |-  ( j = ( k + 1 ) -> C = [_ ( k + 1 ) / j ]_ C )
50 49 breq1d 
 |-  ( j = ( k + 1 ) -> ( C <_ B <-> [_ ( k + 1 ) / j ]_ C <_ B ) )
51 48 50 imbi12d 
 |-  ( j = ( k + 1 ) -> ( ( ( ph /\ k e. Z /\ j = ( k + 1 ) ) -> C <_ B ) <-> ( ( ph /\ k e. Z /\ ( k + 1 ) = ( k + 1 ) ) -> [_ ( k + 1 ) / j ]_ C <_ B ) ) )
52 45 46 51 7 vtoclf 
 |-  ( ( ph /\ k e. Z /\ ( k + 1 ) = ( k + 1 ) ) -> [_ ( k + 1 ) / j ]_ C <_ B )
53 36 37 38 52 syl3anc 
 |-  ( ( ph /\ k e. Z ) -> [_ ( k + 1 ) / j ]_ C <_ B )
54 15 35 53 chvarfv 
 |-  ( ( ph /\ i e. Z ) -> [_ ( i + 1 ) / j ]_ C <_ [_ i / j ]_ C )
55 24 25 6 cbvcsbw 
 |-  [_ ( i + 1 ) / k ]_ B = [_ ( i + 1 ) / j ]_ C
56 55 a1i 
 |-  ( ( ph /\ i e. Z ) -> [_ ( i + 1 ) / k ]_ B = [_ ( i + 1 ) / j ]_ C )
57 eqidd 
 |-  ( ( ph /\ i e. Z ) -> [_ i / j ]_ C = [_ i / j ]_ C )
58 56 57 breq12d 
 |-  ( ( ph /\ i e. Z ) -> ( [_ ( i + 1 ) / k ]_ B <_ [_ i / j ]_ C <-> [_ ( i + 1 ) / j ]_ C <_ [_ i / j ]_ C ) )
59 54 58 mpbird 
 |-  ( ( ph /\ i e. Z ) -> [_ ( i + 1 ) / k ]_ B <_ [_ i / j ]_ C )
60 4 peano2uzs 
 |-  ( i e. Z -> ( i + 1 ) e. Z )
61 60 adantl 
 |-  ( ( ph /\ i e. Z ) -> ( i + 1 ) e. Z )
62 nfv 
 |-  F/ k ( i + 1 ) e. Z
63 1 62 nfan 
 |-  F/ k ( ph /\ ( i + 1 ) e. Z )
64 nfcv 
 |-  F/_ k ( i + 1 )
65 64 nfcsb1 
 |-  F/_ k [_ ( i + 1 ) / k ]_ B
66 65 nfel1 
 |-  F/ k [_ ( i + 1 ) / k ]_ B e. RR
67 63 66 nfim 
 |-  F/ k ( ( ph /\ ( i + 1 ) e. Z ) -> [_ ( i + 1 ) / k ]_ B e. RR )
68 ovex 
 |-  ( i + 1 ) e. _V
69 eleq1 
 |-  ( k = ( i + 1 ) -> ( k e. Z <-> ( i + 1 ) e. Z ) )
70 69 anbi2d 
 |-  ( k = ( i + 1 ) -> ( ( ph /\ k e. Z ) <-> ( ph /\ ( i + 1 ) e. Z ) ) )
71 csbeq1a 
 |-  ( k = ( i + 1 ) -> B = [_ ( i + 1 ) / k ]_ B )
72 71 eleq1d 
 |-  ( k = ( i + 1 ) -> ( B e. RR <-> [_ ( i + 1 ) / k ]_ B e. RR ) )
73 70 72 imbi12d 
 |-  ( k = ( i + 1 ) -> ( ( ( ph /\ k e. Z ) -> B e. RR ) <-> ( ( ph /\ ( i + 1 ) e. Z ) -> [_ ( i + 1 ) / k ]_ B e. RR ) ) )
74 67 68 73 5 vtoclf 
 |-  ( ( ph /\ ( i + 1 ) e. Z ) -> [_ ( i + 1 ) / k ]_ B e. RR )
75 60 74 sylan2 
 |-  ( ( ph /\ i e. Z ) -> [_ ( i + 1 ) / k ]_ B e. RR )
76 eqid 
 |-  ( k e. Z |-> B ) = ( k e. Z |-> B )
77 64 65 71 76 fvmptf 
 |-  ( ( ( i + 1 ) e. Z /\ [_ ( i + 1 ) / k ]_ B e. RR ) -> ( ( k e. Z |-> B ) ` ( i + 1 ) ) = [_ ( i + 1 ) / k ]_ B )
78 61 75 77 syl2anc 
 |-  ( ( ph /\ i e. Z ) -> ( ( k e. Z |-> B ) ` ( i + 1 ) ) = [_ ( i + 1 ) / k ]_ B )
79 simpr 
 |-  ( ( ph /\ i e. Z ) -> i e. Z )
80 nfv 
 |-  F/ j i e. Z
81 2 80 nfan 
 |-  F/ j ( ph /\ i e. Z )
82 nfcsb1v 
 |-  F/_ j [_ i / j ]_ C
83 nfcv 
 |-  F/_ j RR
84 82 83 nfel 
 |-  F/ j [_ i / j ]_ C e. RR
85 81 84 nfim 
 |-  F/ j ( ( ph /\ i e. Z ) -> [_ i / j ]_ C e. RR )
86 eleq1 
 |-  ( j = i -> ( j e. Z <-> i e. Z ) )
87 86 anbi2d 
 |-  ( j = i -> ( ( ph /\ j e. Z ) <-> ( ph /\ i e. Z ) ) )
88 csbeq1a 
 |-  ( j = i -> C = [_ i / j ]_ C )
89 88 eleq1d 
 |-  ( j = i -> ( C e. RR <-> [_ i / j ]_ C e. RR ) )
90 87 89 imbi12d 
 |-  ( j = i -> ( ( ( ph /\ j e. Z ) -> C e. RR ) <-> ( ( ph /\ i e. Z ) -> [_ i / j ]_ C e. RR ) ) )
91 nfv 
 |-  F/ k j e. Z
92 1 91 nfan 
 |-  F/ k ( ph /\ j e. Z )
93 nfv 
 |-  F/ k C e. RR
94 92 93 nfim 
 |-  F/ k ( ( ph /\ j e. Z ) -> C e. RR )
95 eleq1 
 |-  ( k = j -> ( k e. Z <-> j e. Z ) )
96 95 anbi2d 
 |-  ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
97 6 eleq1d 
 |-  ( k = j -> ( B e. RR <-> C e. RR ) )
98 96 97 imbi12d 
 |-  ( k = j -> ( ( ( ph /\ k e. Z ) -> B e. RR ) <-> ( ( ph /\ j e. Z ) -> C e. RR ) ) )
99 94 98 5 chvarfv 
 |-  ( ( ph /\ j e. Z ) -> C e. RR )
100 85 90 99 chvarfv 
 |-  ( ( ph /\ i e. Z ) -> [_ i / j ]_ C e. RR )
101 nfcv 
 |-  F/_ k i
102 nfcv 
 |-  F/_ k [_ i / j ]_ C
103 101 102 33 76 fvmptf 
 |-  ( ( i e. Z /\ [_ i / j ]_ C e. RR ) -> ( ( k e. Z |-> B ) ` i ) = [_ i / j ]_ C )
104 79 100 103 syl2anc 
 |-  ( ( ph /\ i e. Z ) -> ( ( k e. Z |-> B ) ` i ) = [_ i / j ]_ C )
105 78 104 breq12d 
 |-  ( ( ph /\ i e. Z ) -> ( ( ( k e. Z |-> B ) ` ( i + 1 ) ) <_ ( ( k e. Z |-> B ) ` i ) <-> [_ ( i + 1 ) / k ]_ B <_ [_ i / j ]_ C ) )
106 59 105 mpbird 
 |-  ( ( ph /\ i e. Z ) -> ( ( k e. Z |-> B ) ` ( i + 1 ) ) <_ ( ( k e. Z |-> B ) ` i ) )
107 104 100 eqeltrd 
 |-  ( ( ph /\ i e. Z ) -> ( ( k e. Z |-> B ) ` i ) e. RR )
108 107 recnd 
 |-  ( ( ph /\ i e. Z ) -> ( ( k e. Z |-> B ) ` i ) e. CC )
109 108 ralrimiva 
 |-  ( ph -> A. i e. Z ( ( k e. Z |-> B ) ` i ) e. CC )
110 10 4 climbddf 
 |-  ( ( M e. ZZ /\ ( k e. Z |-> B ) e. dom ~~> /\ A. i e. Z ( ( k e. Z |-> B ) ` i ) e. CC ) -> E. x e. RR A. i e. Z ( abs ` ( ( k e. Z |-> B ) ` i ) ) <_ x )
111 3 8 109 110 syl3anc 
 |-  ( ph -> E. x e. RR A. i e. Z ( abs ` ( ( k e. Z |-> B ) ` i ) ) <_ x )
112 9 107 rexabsle2 
 |-  ( ph -> ( E. x e. RR A. i e. Z ( abs ` ( ( k e. Z |-> B ) ` i ) ) <_ x <-> ( E. x e. RR A. i e. Z ( ( k e. Z |-> B ) ` i ) <_ x /\ E. x e. RR A. i e. Z x <_ ( ( k e. Z |-> B ) ` i ) ) ) )
113 111 112 mpbid 
 |-  ( ph -> ( E. x e. RR A. i e. Z ( ( k e. Z |-> B ) ` i ) <_ x /\ E. x e. RR A. i e. Z x <_ ( ( k e. Z |-> B ) ` i ) ) )
114 113 simprd 
 |-  ( ph -> E. x e. RR A. i e. Z x <_ ( ( k e. Z |-> B ) ` i ) )
115 9 10 4 3 11 106 114 climinf2 
 |-  ( ph -> ( k e. Z |-> B ) ~~> inf ( ran ( k e. Z |-> B ) , RR* , < ) )