This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abs2dif2

Description: Difference of absolute values. (Contributed by Mario Carneiro, 14-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 negcl ⊢ ( 𝐵 ∈ ℂ → - 𝐵 ∈ ℂ )
2 abstri ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 + - 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) + ( abs ‘ - 𝐵 ) ) )
3 1 2 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 + - 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) + ( abs ‘ - 𝐵 ) ) )
4 negsub ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
5 4 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 + - 𝐵 ) ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )
6 absneg ⊢ ( 𝐵 ∈ ℂ → ( abs ‘ - 𝐵 ) = ( abs ‘ 𝐵 ) )
7 6 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ - 𝐵 ) = ( abs ‘ 𝐵 ) )
8 7 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ‘ 𝐴 ) + ( abs ‘ - 𝐵 ) ) = ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) )
9 3 5 8 3brtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( abs ‘ ( 𝐴 − 𝐵 ) ) ≤ ( ( abs ‘ 𝐴 ) + ( abs ‘ 𝐵 ) ) )