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 AA00<AA

Proof

Step Hyp Ref Expression
1 id AA
2 0red A0
3 1 2 lttri2d AA0A<00<A
4 3 biimpa AA0A<00<A
5 mullt0 AA<0AA<00<AA
6 5 anidms AA<00<AA
7 mulgt0 A0<AA0<A0<AA
8 7 anidms A0<A0<AA
9 6 8 jaodan AA<00<A0<AA
10 4 9 syldan AA00<AA