# Metamath Proof Explorer

## Theorem abs2dif

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

Ref Expression
Assertion abs2dif ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}\right|-\left|{B}\right|\le \left|{A}-{B}\right|$

### Proof

Step Hyp Ref Expression
1 subid1 ${⊢}{A}\in ℂ\to {A}-0={A}$
2 1 fveq2d ${⊢}{A}\in ℂ\to \left|{A}-0\right|=\left|{A}\right|$
3 subid1 ${⊢}{B}\in ℂ\to {B}-0={B}$
4 3 fveq2d ${⊢}{B}\in ℂ\to \left|{B}-0\right|=\left|{B}\right|$
5 2 4 oveqan12d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}-0\right|-\left|{B}-0\right|=\left|{A}\right|-\left|{B}\right|$
6 0cn ${⊢}0\in ℂ$
7 abs3dif ${⊢}\left({A}\in ℂ\wedge 0\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}-0\right|\le \left|{A}-{B}\right|+\left|{B}-0\right|$
8 6 7 mp3an2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}-0\right|\le \left|{A}-{B}\right|+\left|{B}-0\right|$
9 subcl ${⊢}\left({A}\in ℂ\wedge 0\in ℂ\right)\to {A}-0\in ℂ$
10 6 9 mpan2 ${⊢}{A}\in ℂ\to {A}-0\in ℂ$
11 abscl ${⊢}{A}-0\in ℂ\to \left|{A}-0\right|\in ℝ$
12 10 11 syl ${⊢}{A}\in ℂ\to \left|{A}-0\right|\in ℝ$
13 subcl ${⊢}\left({B}\in ℂ\wedge 0\in ℂ\right)\to {B}-0\in ℂ$
14 6 13 mpan2 ${⊢}{B}\in ℂ\to {B}-0\in ℂ$
15 abscl ${⊢}{B}-0\in ℂ\to \left|{B}-0\right|\in ℝ$
16 14 15 syl ${⊢}{B}\in ℂ\to \left|{B}-0\right|\in ℝ$
17 12 16 anim12i ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left|{A}-0\right|\in ℝ\wedge \left|{B}-0\right|\in ℝ\right)$
18 subcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}-{B}\in ℂ$
19 abscl ${⊢}{A}-{B}\in ℂ\to \left|{A}-{B}\right|\in ℝ$
20 18 19 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}-{B}\right|\in ℝ$
21 df-3an ${⊢}\left(\left|{A}-0\right|\in ℝ\wedge \left|{B}-0\right|\in ℝ\wedge \left|{A}-{B}\right|\in ℝ\right)↔\left(\left(\left|{A}-0\right|\in ℝ\wedge \left|{B}-0\right|\in ℝ\right)\wedge \left|{A}-{B}\right|\in ℝ\right)$
22 17 20 21 sylanbrc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left|{A}-0\right|\in ℝ\wedge \left|{B}-0\right|\in ℝ\wedge \left|{A}-{B}\right|\in ℝ\right)$
23 lesubadd ${⊢}\left(\left|{A}-0\right|\in ℝ\wedge \left|{B}-0\right|\in ℝ\wedge \left|{A}-{B}\right|\in ℝ\right)\to \left(\left|{A}-0\right|-\left|{B}-0\right|\le \left|{A}-{B}\right|↔\left|{A}-0\right|\le \left|{A}-{B}\right|+\left|{B}-0\right|\right)$
24 22 23 syl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left(\left|{A}-0\right|-\left|{B}-0\right|\le \left|{A}-{B}\right|↔\left|{A}-0\right|\le \left|{A}-{B}\right|+\left|{B}-0\right|\right)$
25 8 24 mpbird ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}-0\right|-\left|{B}-0\right|\le \left|{A}-{B}\right|$
26 5 25 eqbrtrrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \left|{A}\right|-\left|{B}\right|\le \left|{A}-{B}\right|$