Metamath Proof Explorer

Theorem abs2dif

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

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

Proof

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