# 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 ${⊢}\left({A}\in ℝ\wedge {A}\ne 0\right)\to 0<{A}{A}$

### Proof

Step Hyp Ref Expression
1 id ${⊢}{A}\in ℝ\to {A}\in ℝ$
2 0red ${⊢}{A}\in ℝ\to 0\in ℝ$
3 1 2 lttri2d ${⊢}{A}\in ℝ\to \left({A}\ne 0↔\left({A}<0\vee 0<{A}\right)\right)$
4 3 biimpa ${⊢}\left({A}\in ℝ\wedge {A}\ne 0\right)\to \left({A}<0\vee 0<{A}\right)$
5 mullt0 ${⊢}\left(\left({A}\in ℝ\wedge {A}<0\right)\wedge \left({A}\in ℝ\wedge {A}<0\right)\right)\to 0<{A}{A}$
6 5 anidms ${⊢}\left({A}\in ℝ\wedge {A}<0\right)\to 0<{A}{A}$
7 mulgt0 ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({A}\in ℝ\wedge 0<{A}\right)\right)\to 0<{A}{A}$
8 7 anidms ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0<{A}{A}$
9 6 8 jaodan ${⊢}\left({A}\in ℝ\wedge \left({A}<0\vee 0<{A}\right)\right)\to 0<{A}{A}$
10 4 9 syldan ${⊢}\left({A}\in ℝ\wedge {A}\ne 0\right)\to 0<{A}{A}$