Metamath Proof Explorer

Theorem abs2difabs

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

Ref Expression
Assertion abs2difabs ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( ( abs ‘ 𝐴 ) − ( abs ‘ 𝐵 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝐵 ) ) )

Proof

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