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

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 )