Theorem msqge0

Description: A square is nonnegative. (Contributed by NM, 23-May-2007) (Revised by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	msqge0	$$⊢A\in ℝ\to 0\le AA$$

Proof

Step	Hyp	Ref	Expression
1		oveq12	$$⊢\left(A=0\wedge A=0\right)\to AA=0\cdot 0$$
2	1	anidms	$$⊢A=0\to AA=0\cdot 0$$
3		0cn	$$⊢0\in ℂ$$
4	3	mul01i	$$⊢0\cdot 0=0$$
5	2 4	eqtrdi	$$⊢A=0\to AA=0$$
6	5	breq2d	$$⊢A=0\to \left(0\le AA\leftrightarrow 0\le 0\right)$$
7		0red	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to 0\in ℝ$$
8		simpl	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to A\in ℝ$$
9	8 8	remulcld	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to AA\in ℝ$$
10		msqgt0	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to 0<AA$$
11	7 9 10	ltled	$$⊢\left(A\in ℝ\wedge A\ne 0\right)\to 0\le AA$$
12		0re	$$⊢0\in ℝ$$
13		leid	$$⊢0\in ℝ\to 0\le 0$$
14	12 13	mp1i	$$⊢A\in ℝ\to 0\le 0$$
15	6 11 14	pm2.61ne	$$⊢A\in ℝ\to 0\le AA$$