Metamath Proof Explorer

Theorem subge0

Description: Nonnegative subtraction. (Contributed by NM, 14-Mar-2005) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 0red ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ∈ ℝ
2 simpr ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ∈ ℝ
3 simpl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ
4 leaddsub ⊢ 0 ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → 0 + B ≤ A ↔ 0 ≤ A − B
5 1 2 3 4 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 + B ≤ A ↔ 0 ≤ A − B
6 2 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ → B ∈ ℂ
7 6 addlidd ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 + B = B
8 7 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 + B ≤ A ↔ B ≤ A
9 5 8 bitr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A − B ↔ B ≤ A