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 \leq A A$

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

Metamath Proof Explorer