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

Metamath Proof Explorer

Theorem msqgt0

Description: A nonzero square is positive. Theorem I.20 of Apostol p. 20. (Contributed by NM, 6-May-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion msqgt0 
|- ( ( A e. RR /\ A =/= 0 ) -> 0 < ( A x. A ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. RR -> A e. RR )
2 0red 
 |-  ( A e. RR -> 0 e. RR )
3 1 2 lttri2d 
 |-  ( A e. RR -> ( A =/= 0 <-> ( A < 0 \/ 0 < A ) ) )
4 3 biimpa 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( A < 0 \/ 0 < A ) )
5 mullt0 
 |-  ( ( ( A e. RR /\ A < 0 ) /\ ( A e. RR /\ A < 0 ) ) -> 0 < ( A x. A ) )
6 5 anidms 
 |-  ( ( A e. RR /\ A < 0 ) -> 0 < ( A x. A ) )
7 mulgt0 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( A e. RR /\ 0 < A ) ) -> 0 < ( A x. A ) )
8 7 anidms 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < ( A x. A ) )
9 6 8 jaodan 
 |-  ( ( A e. RR /\ ( A < 0 \/ 0 < A ) ) -> 0 < ( A x. A ) )
10 4 9 syldan 
 |-  ( ( A e. RR /\ A =/= 0 ) -> 0 < ( A x. A ) )