Theorem msqge0

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

	Ref	Expression
Assertion	msqge0	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq12	⊢ ( ( 𝐴 = 0 ∧ 𝐴 = 0 ) → ( 𝐴 · 𝐴 ) = ( 0 · 0 ) )
2	1	anidms	⊢ ( 𝐴 = 0 → ( 𝐴 · 𝐴 ) = ( 0 · 0 ) )
3		0cn	⊢ 0 ∈ ℂ
4	3	mul01i	⊢ ( 0 · 0 ) = 0
5	2 4	eqtrdi	⊢ ( 𝐴 = 0 → ( 𝐴 · 𝐴 ) = 0 )
6	5	breq2d	⊢ ( 𝐴 = 0 → ( 0 ≤ ( 𝐴 · 𝐴 ) ↔ 0 ≤ 0 ) )
7		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 ∈ ℝ )
8		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
9	8 8	remulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · 𝐴 ) ∈ ℝ )
10		msqgt0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 · 𝐴 ) )
11	7 9 10	ltled	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 ≤ ( 𝐴 · 𝐴 ) )
12		0re	⊢ 0 ∈ ℝ
13		leid	⊢ ( 0 ∈ ℝ → 0 ≤ 0 )
14	12 13	mp1i	⊢ ( 𝐴 ∈ ℝ → 0 ≤ 0 )
15	6 11 14	pm2.61ne	⊢ ( 𝐴 ∈ ℝ → 0 ≤ ( 𝐴 · 𝐴 ) )