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
|- ( A e. RR -> 0 <_ ( A x. A ) )

Proof

Step Hyp Ref Expression
1 oveq12
 |-  ( ( A = 0 /\ A = 0 ) -> ( A x. A ) = ( 0 x. 0 ) )
2 1 anidms
 |-  ( A = 0 -> ( A x. A ) = ( 0 x. 0 ) )
3 0cn
 |-  0 e. CC
4 3 mul01i
 |-  ( 0 x. 0 ) = 0
5 2 4 eqtrdi
 |-  ( A = 0 -> ( A x. A ) = 0 )
6 5 breq2d
 |-  ( A = 0 -> ( 0 <_ ( A x. A ) <-> 0 <_ 0 ) )
7 0red
 |-  ( ( A e. RR /\ A =/= 0 ) -> 0 e. RR )
8 simpl
 |-  ( ( A e. RR /\ A =/= 0 ) -> A e. RR )
9 8 8 remulcld
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( A x. A ) e. RR )
10 msqgt0
 |-  ( ( A e. RR /\ A =/= 0 ) -> 0 < ( A x. A ) )
11 7 9 10 ltled
 |-  ( ( A e. RR /\ A =/= 0 ) -> 0 <_ ( A x. A ) )
12 0re
 |-  0 e. RR
13 leid
 |-  ( 0 e. RR -> 0 <_ 0 )
14 12 13 mp1i
 |-  ( A e. RR -> 0 <_ 0 )
15 6 11 14 pm2.61ne
 |-  ( A e. RR -> 0 <_ ( A x. A ) )