Proof of simple inequality using only fundamental axioms

Question

I want to prove that the solution set to the inequality $$5-x^2<-2$$ is $\ (-\infty, -\sqrt{7})\cup(\sqrt{7}, +\infty)\ $ using only the following axioms/statements (some of them have been put on the same line to keep it short):

1. Associative law (for addition and multiplication)
2. Existence of additive identity and existence of multiplicative identity
3. Existence of additive and multiplicative inverses
4. Commutative law (for addition and multiplication)
5. Closure under addition and closure under multiplication
6. Distributive law
7. Trichotomy law and definition of $\ <,\ >,\ \leq,\ \geq$
8. Definition of squaring ($x^2$) and square root
9. [Derived from 1-6] $\; a < b \Longleftrightarrow a+c<b+c$

Here is my (failed) attempt:

$$5-x^2<-2 \quad \stackrel{(9)}\Leftrightarrow \quad 2+5-x^2+x^2<2-2+x^2 \quad\stackrel{(1,3)}\Leftrightarrow \quad 7 < x^2$$

At this point I already wasn't sure how to continue. The only thing that occurred to me was:

$$7 < x^2 \quad \stackrel{(7)}\Rightarrow \quad x^2 \neq 7 \quad \stackrel{(8)}\Leftrightarrow \quad x\neq \sqrt{7}\ \land \ x\neq -\sqrt{7}$$

So now we know that the solution set S is a subset of $(-\infty, -\sqrt{7})\cup(-\sqrt{7}, \sqrt{7})\cup(\sqrt{7}, +\infty)$, but I don't know how to prove (explicitly using one of the previous 8 assertions at each step) that no $\ x\in(-\sqrt{7}, \sqrt{7})\ $ satisfies the original inequality.

Answer 1

You can use $\;x^2>7\iff\sqrt{x^2}=|x|>\sqrt 7$.

Answer 2

Hint: Presuming that $(5)$ includes the axiom of multiplicativity: $a \le b$ and $c \ge 0$ imply $ac \le bc$, $$0 \le x \le \sqrt{7} \stackrel{(5)}\implies x^2 \le \sqrt{7}x \stackrel{(5)}\le \sqrt{7}\cdot \sqrt{7} = 7.$$