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

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