square of a real number is always positive I was working on a problem and had to prove firsthand that $a^2&gt;0$ if $a$ is not $0$ and I did not find anything on the site that gave a proof using the properties I'm using so I was wondering if mine was good:

$P$ is the set of all positive numbers

Case 1

If $a&gt;0$ then $(a-0) = a\in P$.

Then $(a-0)a\in P$ (closure under multiplication)

$\Rightarrow (a^2 -0)\in P \Rightarrow a^2&gt;0$

Case 2

If $a&lt;0$ then $(0-a) = -a\in P$.

Then $-a(0-a)\in P$ (closure under multiplication)

$\Rightarrow (0 + a^2)\in P$ considering $((-a)(-b) = ab)$

$\Rightarrow (a^2 -(-0)) = (a^2 - 0)\in P \Rightarrow a^2&gt;0$

I feel like $(-a)(-b) = ab$ kind of implies what I'm trying to prove...

Thank you for your help!!
Short answer:

Let $a$ be positive and note that $-a=(-1)a$. Then by associativity of the multiplication,

$$(-a)^2=(-1)^2a^2=a^2.$$
Proposition 10 is the requested result.

Introduction

$+$ is a binary operations from $\mathbb{R}\times \mathbb{R} \to \mathbb{R}$,$-$ 
is a function from $\mathbb{R} \to \mathbb{R}$, $\frac 1 .$ is a function from $\mathbb{R}\setminus \{0\} \to \mathbb{R}$ and $0$ and $1$ are from $\mathbb{R}$
, $0 \ne 1$

In tthe Axiom section the tags on the right side are the names of the axioms. So the associative law of the $+$ operator is called $(\text{AddAssoc})$

The propositions have names $(\text{P1})$ to $(\text{P10})$.
In the proofs the tag on the right side is the name of the axiom that is used to get from the current line to the next line. So in the proof of proposal 1 to get from the first line 
$$a\cdot 0$$
to the second line 
$$0\cdot a+0 $$
one uses axiom $(\text{A2})$
$$a=a+0$$
where we substitue $a$ by $0\cdot a$
to get
$$0\cdot a= 0\cdot a +0$$

In the proofs propositions 1 to 6 and 8 the expression in a line is a real number that is equal to the real number  of the next line or an inequality holds. 
Proposition 7 and  9 are more complex. These are equivalent logical expressions. Proposition 10 is the most complex. It is an indirect proof where we deduce a contradiction from some assumptions.

$(\text{def})$ means that is a definition or an abbreviation that is used here, e.g. $a^2$ is an abbreviation for $a\cdot a$. We do not explicitly state this definition in this text but assume they are known to the reader.

Propositions 1 to 4 are valid for all fields. Propositions 5 to 10 need the order axioms for their proofs.

Maybe it is also useful to read the post from the bottom to the end, so starting with propostion 10 that is the statement asked by the OP.

Axioms

$$a+(b+c)=(a+b)+c \tag{AddAssoc}$$
$$0+a=a \tag{AddIdent}$$
$$a+0=a \tag{AddIdent}$$
$$a+(-a)=0 \tag{AddInv}$$
$$(-a)+a=0 \tag{AddInv}$$
$$a+b=b+a \tag{AddComm}$$

$$a \cdot (b \cdot c)=(a \cdot b) \cdot c \tag{MulAssoc}$$
$$1 \cdot a=a \tag{MulIdent}$$
$$a \cdot 1=a \tag{MulIdent}$$
$$a \cdot \frac 1 a =1 \tag{MulInv}$$
$$\frac 1 a \cdot a   =1 \tag{MulInv}$$
$$a \cdot b=b \cdot a \tag{MulComm}$$

$$a\cdot(b+c)=a\cdot b + a \cdot c \tag{Distrib}$$
$$(a+b) \cdot c =a\cdot c + b \cdot c \tag{Distrib}$$

These axioms define a field.

$$a&lt;0 \; \lor a=0  \; \lor a&gt;0 \tag{OrdTrich}$$
$$a&gt;0 \;  \land  \; b&gt;0 \Rightarrow a\cdot b &gt;0 \tag{OrdMulClose}$$
$$ a&lt;b \Rightarrow a+c \; &lt; \; b+c\tag{OrdTranInv}$$

This is an ordered field now. For our investigations we do not need the completeness axiom that holds in a complete ordered field.

Proposition 1
$$a\cdot 0=0 \tag{P1}$$
Proof
$$ 0\cdot a \tag{AddIdent} $$
$$ =0\cdot a+0  \tag{AddInv} $$
$$=0\cdot a+(0\cdot a+(-(0\cdot a)))  \tag{AddAssoc}$$
$$=(0\cdot a+0\cdot a)+(-(0\cdot a))  \tag{Distrib}$$
$$=(0+0)\cdot a+(-(0\cdot a )) \tag{AddIdent}$$
$$=0\cdot a+(-(0\cdot a))  \tag{AddInv}$$
$$=0$$

Proposition 2:
$$(-1)^2=1 \tag{P2}$$
Proof:
$$(-1)^2 \tag{AddIdent}$$
$$=(-1)^2+0 \tag{AddInv}$$
$$=(-1)^2+((-1)+1) \tag{AddAssoc}$$
$$=((-1)^2+(-1))+1 \tag{MulIdent}$$
$$=((-1)^2+(-1)\cdot 1)+1 \tag{Distrib}$$
$$=(-1)((-1)+1)+1 \tag{AddInv}$$
$$=(-1)\cdot 0+1 \tag{P1}$$
$$=0+1 \tag{AddIdent}$$
$$=1$$

Proposition 3
$$-a=(-1)a \tag{P3}$$
Proof
$$-a \tag{AddIdent}$$
$$=-a+0 \tag{P1}$$
$$=-a+0\cdot a \tag{AddInv}$$
$$=-a+(1+(-1))\cdot a \tag{Distrib}$$
$$=-a+(1\cdot a+(-1)\cdot a) \tag{MulIdent}$$
$$=-a+(a+(-1)\cdot a) \tag{AddAssoc}$$
$$=(-a+a)+(-1)\cdot a \tag{AddInv}$$
$$=0+(-1)\cdot a \tag{AddIdent}$$
$$=(-1)\cdot a$$

Proposition 4
$$(-a)^2=a^2   \tag{P4}$$

Proof
$$ (-a)^2 \tag{P3}$$
$$= ((-1)a)^2 \tag{def}$$
$$=((-1)a)((-1)a) \tag{MulAssoc}$$
$$=(((-1)a)(-1))a \tag{MulAssoc}$$
$$=((-1)(a(-1)))a \tag{MulComm}$$
$$=((-1)((-1)a))a \tag{MulAssoc}$$
$$=(((-1)(-1))a)a \tag{MulAssoc}$$
$$=((-1)(-1))(a\cdot a) \tag{def}$$
$$=(-1)^2a^2 \tag{P2}$$
$$=1\cdot a^2  \tag{MulIdent}$$
$$=a^2$$

Proposition 5
$$1&gt;0 \tag{P5}$$
Proof:
$$1 \tag{MulIdent}$$
$$=1\cdot 1 \tag{OrdMulClose}$$
$$\ge 0 $$

Proposition 6
$$(-1)^2&gt;0 \tag{P6}$$
Proof:
$$(-1)^2 \tag{P2}$$
$$=1\tag{P5}$$
$$\ge 0 $$

Proposition 7
$$a \ge 0 \Rightarrow a^2\ge0\tag{P7}$$
Proof

This follows from $(\text{OrdMulClose})$
if we replace $b$ by $a$.

Proposition 8
$$a \le 0 \Rightarrow a^2\ge0\tag{P8}$$ 
Proof:
We have 
$$a \le 0 \tag{OrdTranInv}$$
$$a+(-a) \le 0+(-a)$$
applying $(\text{AddInv})$ to the LHS and $(\text{AddIdent})$ to the RHS gives
$$0\le -a$$
which means 
$$-a \ge 0$$
So by $(\text{P7})$ we have
$$(-a)^2 \ge 0\tag{1}$$
From $(\text{P4})$
So we have 
$$a^2 =(-a)^2 \tag{2}$$
From $(1)$ and $(2)$ follows
$$a^2\ge 0$$

Proposition 9
$$a^2\ge0\tag{P9}$$
Proof:
From $(\text{OrdTrich})$ we know that for each $a \in \mathbb{R}$ holds
$$a&lt;0 \; \lor a=0  \; \lor a&gt;0 $$
So from $(\text{P7})$  and $(\text{P8})$ follows $(\text{P9})$ 

Proposition 10
$$a\ne0 \Rightarrow a^2\gt0\tag{P10}$$
Proof:
From $(\text{P9})$  we have
$$a^2\ge0$$
if 
$$a^2=0\tag{3}$$
and
$$a\ne 0\tag{4}$$
we can assume that there is $\frac 1 a$
and so from $(3)$ we get
$$\frac 1 a a^2=0\tag{MulAssoc}$$
$$\Rightarrow (\frac 1 a \cdot a) \cdot a=0\tag{MulInv}$$
$$\Rightarrow 1 \cdot a=0\tag{MulIdent}$$
$$\Rightarrow a=0$$
which contradicts $(\text{4})$