Metamath Proof Explorer


Theorem leabsi

Description: A real number is less than or equal to its absolute value. (Contributed by NM, 2-Aug-1999)

Ref Expression
Hypothesis sqrtthi.1 𝐴 ∈ ℝ
Assertion leabsi 𝐴 ≤ ( abs ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 sqrtthi.1 𝐴 ∈ ℝ
2 leabs ( 𝐴 ∈ ℝ → 𝐴 ≤ ( abs ‘ 𝐴 ) )
3 1 2 ax-mp 𝐴 ≤ ( abs ‘ 𝐴 )