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