Theorem sqge0i

Description: The square of a real is nonnegative. (Contributed by NM, 3-Aug-1999)

	Ref	Expression
Hypothesis	resqcl.1	$$⊢A\in ℝ$$
Assertion	sqge0i	$$⊢0\le A^2$$

Proof

Step	Hyp	Ref	Expression
1		resqcl.1	$$⊢A\in ℝ$$
2	1	msqge0i	$$⊢0\le AA$$
3	1	recni	$$⊢A\in ℂ$$
4	3	sqvali	$$⊢A^2=AA$$
5	2 4	breqtrri	$$⊢0\le A^2$$