Metamath Proof Explorer


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 ≤ ( 𝐴 · 𝐴 ) )