Metamath Proof Explorer


Theorem sqge0

Description: A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999)

Ref Expression
Assertion sqge0 ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 msqge0 ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 · 𝐴 ) )
2 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3 sqval ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
4 2 3 syl ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
5 1 4 breqtrrd ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 ↑ 2 ) )