Metamath Proof Explorer

Theorem abs2dif2

Description: Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Assertion abs2dif2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ≤ A + B

Proof

Step Hyp Ref Expression
1 negcl ⊢ B ∈ ℂ → − B ∈ ℂ
2 abstri ⊢ A ∈ ℂ ∧ − B ∈ ℂ → A + − B ≤ A + − B
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B ≤ A + − B
4 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
5 4 fveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
6 absneg ⊢ B ∈ ℂ → − B = B
7 6 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ → − B = B
8 7 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A + B
9 3 5 8 3brtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ≤ A + B