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

Metamath Proof Explorer

Theorem absneg

Description: Absolute value of the negative. (Contributed by NM, 27-Feb-2005)

Ref Expression
Assertion absneg ( 𝐴 ∈ ℂ → ( abs ‘ - 𝐴 ) = ( abs ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cjneg ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ - 𝐴 ) = - ( ∗ ‘ 𝐴 ) )
2 1 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 · ( ∗ ‘ - 𝐴 ) ) = ( - 𝐴 · - ( ∗ ‘ 𝐴 ) ) )
3 cjcl ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
4 mul2neg ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( - 𝐴 · - ( ∗ ‘ 𝐴 ) ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
5 3 4 mpdan ⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 · - ( ∗ ‘ 𝐴 ) ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
6 2 5 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 · ( ∗ ‘ - 𝐴 ) ) = ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
7 6 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( - 𝐴 · ( ∗ ‘ - 𝐴 ) ) ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
8 negcl ⊢ ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
9 absval ⊢ ( - 𝐴 ∈ ℂ → ( abs ‘ - 𝐴 ) = ( √ ‘ ( - 𝐴 · ( ∗ ‘ - 𝐴 ) ) ) )
10 8 9 syl ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ - 𝐴 ) = ( √ ‘ ( - 𝐴 · ( ∗ ‘ - 𝐴 ) ) ) )
11 absval ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
12 7 10 11 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( abs ‘ - 𝐴 ) = ( abs ‘ 𝐴 ) )