Metamath Proof Explorer

Theorem abs2dif

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

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

Proof

Step Hyp Ref Expression
1 subid1 ⊢A∈ℂ→A−0=A
2 1 fveq2d ⊢A∈ℂ→A−0=A
3 subid1 ⊢B∈ℂ→B−0=B
4 3 fveq2d ⊢B∈ℂ→B−0=B
5 2 4 oveqan12d ⊢A∈ℂ∧B∈ℂ→A−0−B−0=A−B
6 0cn ⊢0∈ℂ
7 abs3dif ⊢A∈ℂ∧0∈ℂ∧B∈ℂ→A−0≤A−B+B−0
8 6 7 mp3an2 ⊢A∈ℂ∧B∈ℂ→A−0≤A−B+B−0
9 subcl ⊢A∈ℂ∧0∈ℂ→A−0∈ℂ
10 6 9 mpan2 ⊢A∈ℂ→A−0∈ℂ
11 abscl ⊢A−0∈ℂ→A−0∈ℝ
12 10 11 syl ⊢A∈ℂ→A−0∈ℝ
13 subcl ⊢B∈ℂ∧0∈ℂ→B−0∈ℂ
14 6 13 mpan2 ⊢B∈ℂ→B−0∈ℂ
15 abscl ⊢B−0∈ℂ→B−0∈ℝ
16 14 15 syl ⊢B∈ℂ→B−0∈ℝ
17 12 16 anim12i ⊢A∈ℂ∧B∈ℂ→A−0∈ℝ∧B−0∈ℝ
18 subcl ⊢A∈ℂ∧B∈ℂ→A−B∈ℂ
19 abscl ⊢A−B∈ℂ→A−B∈ℝ
20 18 19 syl ⊢A∈ℂ∧B∈ℂ→A−B∈ℝ
21 df-3an ⊢A−0∈ℝ∧B−0∈ℝ∧A−B∈ℝ↔A−0∈ℝ∧B−0∈ℝ∧A−B∈ℝ
22 17 20 21 sylanbrc ⊢A∈ℂ∧B∈ℂ→A−0∈ℝ∧B−0∈ℝ∧A−B∈ℝ
23 lesubadd ⊢A−0∈ℝ∧B−0∈ℝ∧A−B∈ℝ→A−0−B−0≤A−B↔A−0≤A−B+B−0
24 22 23 syl ⊢A∈ℂ∧B∈ℂ→A−0−B−0≤A−B↔A−0≤A−B+B−0
25 8 24 mpbird ⊢A∈ℂ∧B∈ℂ→A−0−B−0≤A−B
26 5 25 eqbrtrrd ⊢A∈ℂ∧B∈ℂ→A−B≤A−B