Metamath Proof Explorer


Theorem abs2difi

Description: Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007)

Ref Expression
Hypotheses abs2difi.1 ⊢ A ∈ ℂ
abs2difi.2 ⊢ B ∈ ℂ
Assertion abs2difi ⊢ A − B ≤ A − B

Proof

Step Hyp Ref Expression
1 abs2difi.1 ⊢ A ∈ ℂ
2 abs2difi.2 ⊢ B ∈ ℂ
3 abs2dif ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ≤ A − B
4 1 2 3 mp2an ⊢ A − B ≤ A − B