Metamath Proof Explorer


Theorem abslti

Description: Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005)

Ref Expression
Hypotheses sqrtthi.1
|- A e. RR
sqr11.1
|- B e. RR
Assertion abslti
|- ( ( abs ` A ) < B <-> ( -u B < A /\ A < B ) )

Proof

Step Hyp Ref Expression
1 sqrtthi.1
 |-  A e. RR
2 sqr11.1
 |-  B e. RR
3 abslt
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( abs ` A ) < B <-> ( -u B < A /\ A < B ) ) )
4 1 2 3 mp2an
 |-  ( ( abs ` A ) < B <-> ( -u B < A /\ A < B ) )