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

Metamath Proof Explorer

Theorem abslei

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

Ref Expression
Hypotheses sqrtthi.1 ⊢ 𝐴 ∈ ℝ
sqr11.1 ⊢ 𝐵 ∈ ℝ
Assertion abslei ( ( abs ‘ 𝐴 ) ≤ 𝐵 ↔ ( - 𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sqrtthi.1 ⊢ 𝐴 ∈ ℝ
2 sqr11.1 ⊢ 𝐵 ∈ ℝ
3 absle ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ 𝐴 ) ≤ 𝐵 ↔ ( - 𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
4 1 2 3 mp2an ⊢ ( ( abs ‘ 𝐴 ) ≤ 𝐵 ↔ ( - 𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) )