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

Metamath Proof Explorer

Theorem subge02

Description: Nonnegative subtraction. (Contributed by NM, 27-Jul-2005)

Ref Expression
Assertion subge02 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ B ↔ A − B ≤ A

Proof

Step Hyp Ref Expression
1 addge01 ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ B ↔ A ≤ A + B
2 lesubadd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → A − B ≤ A ↔ A ≤ A + B
3 2 3anidm13 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B ≤ A ↔ A ≤ A + B
4 1 3 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ B ↔ A − B ≤ A