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 ) )