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