This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \leq A^{2}$

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