Metamath Proof Explorer


Theorem rlimsqz2

Description: Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 3-Feb-2014) (Revised by Mario Carneiro, 20-May-2016)

Ref Expression
Hypotheses rlimsqz.d
|- ( ph -> D e. RR )
rlimsqz.m
|- ( ph -> M e. RR )
rlimsqz.l
|- ( ph -> ( x e. A |-> B ) ~~>r D )
rlimsqz.b
|- ( ( ph /\ x e. A ) -> B e. RR )
rlimsqz.c
|- ( ( ph /\ x e. A ) -> C e. RR )
rlimsqz2.1
|- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ B )
rlimsqz2.2
|- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> D <_ C )
Assertion rlimsqz2
|- ( ph -> ( x e. A |-> C ) ~~>r D )

Proof

Step Hyp Ref Expression
1 rlimsqz.d
 |-  ( ph -> D e. RR )
2 rlimsqz.m
 |-  ( ph -> M e. RR )
3 rlimsqz.l
 |-  ( ph -> ( x e. A |-> B ) ~~>r D )
4 rlimsqz.b
 |-  ( ( ph /\ x e. A ) -> B e. RR )
5 rlimsqz.c
 |-  ( ( ph /\ x e. A ) -> C e. RR )
6 rlimsqz2.1
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ B )
7 rlimsqz2.2
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> D <_ C )
8 1 recnd
 |-  ( ph -> D e. CC )
9 4 recnd
 |-  ( ( ph /\ x e. A ) -> B e. CC )
10 5 recnd
 |-  ( ( ph /\ x e. A ) -> C e. CC )
11 5 adantrr
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C e. RR )
12 4 adantrr
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> B e. RR )
13 1 adantr
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> D e. RR )
14 11 12 13 6 lesub1dd
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( C - D ) <_ ( B - D ) )
15 13 11 7 abssubge0d
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` ( C - D ) ) = ( C - D ) )
16 13 11 12 7 6 letrd
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> D <_ B )
17 13 12 16 abssubge0d
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` ( B - D ) ) = ( B - D ) )
18 14 15 17 3brtr4d
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` ( C - D ) ) <_ ( abs ` ( B - D ) ) )
19 2 8 3 9 10 18 rlimsqzlem
 |-  ( ph -> ( x e. A |-> C ) ~~>r D )