Metamath Proof Explorer

Theorem rlimsqz

Description: Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by Mario Carneiro, 18-Sep-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 )
rlimsqz.1 
|- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> B <_ C )
rlimsqz.2 
|- ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ D )
Assertion rlimsqz 
|- ( 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 rlimsqz.1 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> B <_ C )
7 rlimsqz.2 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C <_ D )
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 4 adantrr 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> B e. RR )
12 5 adantrr 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> C e. RR )
13 1 adantr 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> D e. RR )
14 11 12 13 6 lesub2dd 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( D - C ) <_ ( D - B ) )
15 12 13 7 abssuble0d 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` ( C - D ) ) = ( D - C ) )
16 11 12 13 6 7 letrd 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> B <_ D )
17 11 13 16 abssuble0d 
 |-  ( ( ph /\ ( x e. A /\ M <_ x ) ) -> ( abs ` ( B - D ) ) = ( D - B ) )
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 )