absid

Description: A nonnegative number is its own absolute value. (Contributed by NM, 11-Oct-1999) (Revised by Mario Carneiro, 29-May-2016)

		Ref	Expression
	Assertion	absid	$⊢ (A \in ℝ \land 0 \leq A) \to \|A\| = A$

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℝ \land 0 \leq A) \to A \in ℝ$
2	1	recnd	$⊢ (A \in ℝ \land 0 \leq A) \to A \in ℂ$
3		absval	$⊢ A \in ℂ \to \|A\| = \sqrt{A \overline{A}}$
4	2 3	syl	$⊢ (A \in ℝ \land 0 \leq A) \to \|A\| = \sqrt{A \overline{A}}$
5	1	cjred	$⊢ (A \in ℝ \land 0 \leq A) \to \overline{A} = A$
6	5	oveq2d	$⊢ (A \in ℝ \land 0 \leq A) \to A \overline{A} = A A$
7	2	sqvald	$⊢ (A \in ℝ \land 0 \leq A) \to A^{2} = A A$
8	6 7	eqtr4d	$⊢ (A \in ℝ \land 0 \leq A) \to A \overline{A} = A^{2}$
9	8	fveq2d	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A \overline{A}} = \sqrt{A^{2}}$
10		sqrtsq	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A^{2}} = A$
11	4 9 10	3eqtrd	$⊢ (A \in ℝ \land 0 \leq A) \to \|A\| = A$

Metamath Proof Explorer