Metamath Proof Explorer

Theorem abs2difabs

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

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

Proof

Step Hyp Ref Expression
1 abs2dif ⊢ B ∈ ℂ ∧ A ∈ ℂ → B − A ≤ B − A
2 1 ancoms ⊢ A ∈ ℂ ∧ B ∈ ℂ → B − A ≤ B − A
3 abscl ⊢ A ∈ ℂ → A ∈ ℝ
4 3 recnd ⊢ A ∈ ℂ → A ∈ ℂ
5 abscl ⊢ B ∈ ℂ → B ∈ ℝ
6 5 recnd ⊢ B ∈ ℂ → B ∈ ℂ
7 negsubdi2 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = B − A
8 4 6 7 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B = B − A
9 abssub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B = B − A
10 2 8 9 3brtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B ≤ A − B
11 abs2dif ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ≤ A − B
12 resubcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B ∈ ℝ
13 3 5 12 syl2an ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℝ
14 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
15 abscl ⊢ A − B ∈ ℂ → A − B ∈ ℝ
16 14 15 syl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℝ
17 absle ⊢ A − B ∈ ℝ ∧ A − B ∈ ℝ → A − B ≤ A − B ↔ − A − B ≤ A − B ∧ A − B ≤ A − B
18 13 16 17 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ≤ A − B ↔ − A − B ≤ A − B ∧ A − B ≤ A − B
19 lenegcon1 ⊢ A − B ∈ ℝ ∧ A − B ∈ ℝ → − A − B ≤ A − B ↔ − A − B ≤ A − B
20 13 16 19 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B ≤ A − B ↔ − A − B ≤ A − B
21 20 anbi1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A − B ≤ A − B ∧ A − B ≤ A − B ↔ − A − B ≤ A − B ∧ A − B ≤ A − B
22 18 21 bitr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ≤ A − B ↔ − A − B ≤ A − B ∧ A − B ≤ A − B
23 10 11 22 mpbir2and ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ≤ A − B