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