Metamath Proof Explorer

Theorem abssubge0

Description: Absolute value of a nonnegative difference. (Contributed by NM, 14-Feb-2008)

Ref Expression
Assertion abssubge0 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B − A = B − A

Proof

Step Hyp Ref Expression
1 resubcl ⊢ B ∈ ℝ ∧ A ∈ ℝ → B − A ∈ ℝ
2 1 3adant3 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ A ≤ B → B − A ∈ ℝ
3 subge0 ⊢ B ∈ ℝ ∧ A ∈ ℝ → 0 ≤ B − A ↔ A ≤ B
4 3 biimp3ar ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ A ≤ B → 0 ≤ B − A
5 absid ⊢ B − A ∈ ℝ ∧ 0 ≤ B − A → B − A = B − A
6 2 4 5 syl2anc ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ A ≤ B → B − A = B − A
7 6 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A ≤ B → B − A = B − A