Theorem absor

Description: The absolute value of a real number is either that number or its negative. (Contributed by NM, 27-Feb-2005)

	Ref	Expression
Assertion	absor	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) = 𝐴 ∨ ( abs ‘ 𝐴 ) = - 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		letric	⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ∨ 𝐴 ≤ 0 ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ∨ 𝐴 ≤ 0 ) )
4		absid	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( abs ‘ 𝐴 ) = 𝐴 )
5	4	ex	⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 → ( abs ‘ 𝐴 ) = 𝐴 ) )
6		absnid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) → ( abs ‘ 𝐴 ) = - 𝐴 )
7	6	ex	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≤ 0 → ( abs ‘ 𝐴 ) = - 𝐴 ) )
8	5 7	orim12d	⊢ ( 𝐴 ∈ ℝ → ( ( 0 ≤ 𝐴 ∨ 𝐴 ≤ 0 ) → ( ( abs ‘ 𝐴 ) = 𝐴 ∨ ( abs ‘ 𝐴 ) = - 𝐴 ) ) )
9	3 8	mpd	⊢ ( 𝐴 ∈ ℝ → ( ( abs ‘ 𝐴 ) = 𝐴 ∨ ( abs ‘ 𝐴 ) = - 𝐴 ) )