Description: Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | absltd.1 | |- ( ph -> A e. RR ) |
|
absltd.2 | |- ( ph -> B e. RR ) |
||
Assertion | absled | |- ( ph -> ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | absltd.1 | |- ( ph -> A e. RR ) |
|
2 | absltd.2 | |- ( ph -> B e. RR ) |
|
3 | absle | |- ( ( A e. RR /\ B e. RR ) -> ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) ) ) |
|
4 | 1 2 3 | syl2anc | |- ( ph -> ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) ) ) |