Theorem sqge0

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

	Ref	Expression
Assertion	sqge0	$$⊢A\in ℝ\to 0\le A^2$$

Proof

Step	Hyp	Ref	Expression
1		msqge0	$$⊢A\in ℝ\to 0\le AA$$
2		recn	$$⊢A\in ℝ\to A\in ℂ$$
3		sqval	$$⊢A\in ℂ\to A^2=AA$$
4	2 3	syl	$$⊢A\in ℝ\to A^2=AA$$
5	1 4	breqtrrd	$$⊢A\in ℝ\to 0\le A^2$$