absneg

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

		Ref	Expression
	Assertion	absneg	$⊢ A \in ℂ \to \|- A\| = \|A\|$

Step	Hyp	Ref	Expression
1		cjneg	$⊢ A \in ℂ \to \overline{- A} = - \overline{A}$
2	1	oveq2d	$⊢ A \in ℂ \to (- A) \overline{- A} = (- A) (- \overline{A})$
3		cjcl	$⊢ A \in ℂ \to \overline{A} \in ℂ$
4		mul2neg	$⊢ (A \in ℂ \land \overline{A} \in ℂ) \to (- A) (- \overline{A}) = A \overline{A}$
5	3 4	mpdan	$⊢ A \in ℂ \to (- A) (- \overline{A}) = A \overline{A}$
6	2 5	eqtrd	$⊢ A \in ℂ \to (- A) \overline{- A} = A \overline{A}$
7	6	fveq2d	$⊢ A \in ℂ \to \sqrt{(- A) \overline{- A}} = \sqrt{A \overline{A}}$
8		negcl	$⊢ A \in ℂ \to - A \in ℂ$
9		absval	$⊢ - A \in ℂ \to \|- A\| = \sqrt{(- A) \overline{- A}}$
10	8 9	syl	$⊢ A \in ℂ \to \|- A\| = \sqrt{(- A) \overline{- A}}$
11		absval	$⊢ A \in ℂ \to \|A\| = \sqrt{A \overline{A}}$
12	7 10 11	3eqtr4d	$⊢ A \in ℂ \to \|- A\| = \|A\|$

Metamath Proof Explorer