Proof of Nonnegativity of Squares in an Ordered Field

Notation is as in the statement. An ordered field is in particular a field, and $F$ is such a field.

Claim 1. By claim 1 of Properties of the Absolute Value in an Ordered Field, $|t|$ equals $t$ or $-t$. In the first case $|t|^{2}=t\cdot t=t^{2}$. In the second case claim 2 of Zero Products and Elementary Identities in a Field gives $(-t)(-t)=t\cdot t$, so again $|t|^{2}=t^{2}$.

Claim 2. By claim 1 of Properties of the Absolute Value in an Ordered Field we also have $0\le|t|$. Applying claim 5 of Elementary Arithmetic in an Ordered Field to the inequality $0\le|t|$ with the nonnegative multiplier $|t|$ gives

$$|t|\cdot0\le|t|\,|t| .$$

By claim 1 of Zero Products and Elementary Identities in a Field, $|t|\cdot0=0$, so $0\le|t|^{2}$. Claim 1 now gives $0\le t^{2}$. $\blacksquare$