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 ) |