Prove $1 > 0$ in ordered field My proof of $1>0$ in the ordered field $F=\mathbb{R}$ seems too simple, but maybe it's correct?
Here are the field axioms and resultant lemmas I'm drawing upon in the main Theorem.
Field Axiom (F1): $a \cdot 1 = a\;\forall a \in F$
Field Axiom (F2): $\forall a \in F,\;\exists (-a) \in F: a + (-a) = 0$
Field Axiom (F3): $a + 0 = a\;\;\forall a \in F$
Field Axiom (F4): $a(b + c) = ab + ac\;\;\forall a,b,c \in F$
Field Axiom (F5): $(a + b) + c = a + (b+c)\;\forall a,b,c \in F$
Field Axiom (F6): $a+b = b+ a\;\forall a,b \in F$
Field Axiom (F7): $a\neq 0 \implies \exists a^{-1}: aa^{-1} = 1$
Ordered Field Axiom (O1): $a \leq b \text{ and } c\geq0 \implies ac \leq bc$
Ordered Field Axiom (O2): $a \leq b \implies a + c \leq b + c$
Lemma (L1): $a\cdot 0 = 0\;\;\forall a \in F$:
$$ a(1+0) \stackrel{F4}{=} a\cdot 1 + a\cdot 0 \stackrel{F1}{=} a + a\cdot 0 = a(1+0) \stackrel{F3}{=} a\cdot 1 \stackrel{F1}{=}a \implies $$
$$a+a\cdot 0 = a \implies (-a) + a +  a\cdot 0 = (-a) + a   \stackrel{F2}{\implies} 0 + a\cdot 0  = 0$$
$$\stackrel{F3}{\implies} a\cdot 0  = 0\;\;\square$$
Lemma (L2): $a>0 \implies a^{-1} > 0$
Assume $a>0, a^{-1} \leq 0 $ then
$$a^{-1} \leq 0 \stackrel{O1}{\implies} aa^{-1} \leq 0\cdot a  \stackrel{F7,L1}{\implies} 1 \leq 0 \stackrel{O1}{\implies} a\cdot 1 \leq a\cdot 0 \stackrel{F1,L1}{\implies} a \leq 0$$
But we assumed $a>0$, therefore $a^{-1} > 0\;\;\square$
Lemma (L3): $a>b \implies a-b > 0$
$$a+(-a)>b+(-a) \stackrel{F2}{\implies}  0>b-a\;\;\square$$
Lemma (L4): $a<b \text{ and } ac < bc \implies c> 0$
Assume $a<b \text{ and } ac < bc$
$$ac < bc \stackrel{O2}{\implies} ac + (-ac) < bc + (-ac) \stackrel{F2}{\implies} 0 \leq bc + (-ac) \stackrel{F4}{\implies}0 \leq c(b + (-a))$$
Therefore,
$$b>a \stackrel{L3}{\implies} b + (-a) > 0 \stackrel{F2}{\implies}(b + (-a))^{-1} > 0 \stackrel{O1}{\implies}$$
$$0\cdot (b + (-a))^{-1} < c(b + (-a))\cdot (b + (-a))^{-1} \stackrel{F7,L1}{\implies} 0 \leq c\cdot 1 \stackrel{F1}{\implies} 0 < c\;\;\square$$

Theorem: $0<1$
$$a < b \implies a \stackrel{F1}{=} a\cdot1 < b \stackrel{F1}{=}b\cdot1 \implies a\cdot 1 < b\cdot 1 \stackrel{L4}{\implies} 1>0 \;\;\square$$
 A: Your proof if fine but it extremely long and much more complicated than it needs to be.
The man thing is proving Th:  $x^2 \ge 0$ and $x^2 = 0 \iff x=0$ and $0< 1$ follows as a corollary.
Lemma 1: can be more easily proven via $a\cdot 0 + a\cdot 0 = a(0+0) = a\cdot 0$ so $a\cdot 0 + a\cdot 0 + (-(a\cdot 0)) = a\cdot 0 + (-(a\cdot 0))$ so $a\cdot 0 + 0 = 0$ and $a\cdot 0 = 0$.
The only three other lemmas you need are:
Lemma B:  $a > 0 \implies -a < 0$.
Proof:  $a > 0 \implies a+(-a) > 0 + (-a) \implies 0 > -a$.
Lemma D:  $-(-a) = a$.
Pf:  $(-a) + a = a+(-a) = 0$ so $-(-a) = a$
Lemma C: $a(-b) = (-a)b = -(ab)$ and $(-a)(-b)=ab$ and $(-a)(-b) = ab$
Pf: $ab + a(-b) = a(b+(-b)) = a\cdot 0 = 0$ and therefore $-(ab) = a(-b)$.  Likewise $ab + (-a)b = (a +(-a))b = 0\cdot b = 0$ and therefore $-(a) =(-a)b$
Finally $(-a)(-b) = -(a(-b))=-(-(ab)) = ab$.
Thereom:  $x^2 \ge 0$ with $x^2 = 0 \iff x=0$.
Pf:  If $x > 0$ then $x\times x > 0 \times x$ and $x^2 > 0$.
if $x=0$ then $x^2 = x\times x = 0 \times 0$ and by Lemma 1 $0\times 0 = 0$.
If $x < 0$ then $0 < -x$ and $(-x)^2 > 0$ and as $(-x)^2 = x^2$ we have $x^2 > 0$.
Corollary:  $1 > 0$.
Pf:  $1 = 1^2$ and $1\ne 0$ so $1^2 > 0$ so $1 > 0$.
A: *

*$a\cdot 0=0\quad \forall a\in F$


*$a\cdot 1= a\quad \forall a\in F$
Let $a<0$ then $a\cdot 1<a\cdot 0$
Implies $a\cdot(1-0) <0$
Since $a<0$ and $a\cdot (1-0)<0$
Implies $1-0>0$
Hence $1>0+0=0$
