Theorem 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	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
2	1	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
3		absval	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
4	2 3	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
5	1	cjred	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ∗ ‘ 𝐴 ) = 𝐴 )
6	5	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) = ( 𝐴 · 𝐴 ) )
7	2	sqvald	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
8	6 7	eqtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) = ( 𝐴 ↑ 2 ) )
9	8	fveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) = ( √ ‘ ( 𝐴 ↑ 2 ) ) )
10		sqrtsq	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = 𝐴 )
11	4 9 10	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )