Most of your statements are elementary algebra, so these can be proved automatically by a computer algebra system (CAS), such as Maple or Mathematica.
(In case you're interested in the mathematics behind CAS, I can recommend the book Modern Computer Algebra by Joachim von zur Gathen and Jürgen Gerhard, a beautiful book, considered the 'bible' of the field)
Automated theorem proving tends to be mostly a case of doing heuristic search on a structure that represents proofs, if the proof is not one of the few cases for which there is an algorithm that can conclusively solve it. Given that this statements aren't very complicated, it is likely that an automated prover is able to 'find' a proof.
However, I think it is interesting to say a bit more about the statements for which there are nice algorithms:
Statement 3 is (a very simple case of) about roots of a (system of) polynomial equations and can be solved by finding a Gröbner basis with Buchberger's algorithm. The Gröbner basis and Buchberger's algorithm to find one are very nice tools for automated theorem proving. For example, we can even automatically prove elementary theorems in geometry by automatically transforming the problem to finding a root of a polynomial equation in a clever way!
Another interesting class of theorems are statements expressible in quantifier-free Presburger arithmetic (in particular, this arithmetic is without multiplication, so this doesn't apply to your statements), as there is an algorithm to solve all such statements, even though the algorithm is a bit slow.