Proving the Triangle Inequality using only the Axioms of Inequality on the set of Real Numbers I want to prove that for all $a, b \in \mathbb R, |a + b| \leq |a| + |b|$, using only the following axioms, definition, and theorems below:
Axioms:
For all $a,b,c \in \mathbb R:$


*

*Either $a \leq b$ or $b \leq a$

*If $a \leq b$ and $b \leq a$, then $a = b$

*If $a \leq b$ and $b \leq c$, then $a \leq c$

*If $a \leq b$, then $a + c \leq b + c$

*If $a \leq b$ and $0 \leq c$, then $ac \leq bc$
Definition:
Let $a \in \mathbb R$. Then $|a|:= \begin{cases}
a,  & \text{if $0 \leq a$} \\
-a, & \text{if $a \lt 0$}
\end{cases}$
Theorems: For all $a,b \in \mathbb R:$


*

*$0 \leq a^2$ 

*$0 \leq |a|$

*$-|a| \leq a \leq |a|$ and $a=|a|$ if, and only if, $0 \leq a$

*$|ab| = |a||b|$
In a coursebook that I'm reading for Real Analysis, it specifically states that all theorems must be proved using only the axioms and the theorems that have previously been given to us. However, one proof in the coursebook for showing that the Triangle Inequality holds seems to contradict what it had mentioned. In particular, their proof is the following:


*

*"Let $a,b \in \mathbb R$. Then $|a+b|^2 = (a+b)^2 = a^2 + 2ab + b^2 \leq a^2 +2|a||b| + |b|^2 = (|a| + |b|)^2$. Thus, we get that $|a + b| \leq |a| + |b|$ by taking the square root of each side."


For instance, it does not actually prove anywhere that if $|a + b|^2 \leq (|a| + |b|)^2$, then $|a + b| \leq |a| + |b|$. I thought we had to state each axiom explicitly step-by-step. So in my case, I would have done something like this in a part of the proof:


*

*"Let $a,b \in \mathbb R$. We note first that for any $c \in \mathbb R$, $|c|^2 = c^2$. Indeed, if $0 \leq c$, then by the definition, $|c| = c$, and if $c \leq 0$, $|c| = -c$. Thus, $|c|^2 = c^2$  for any $c \in \mathbb R$. We then note that $|a + b|^2 = (a+b)^2 = a^2 + 2ab + b^2$. By Theorem 3 above, since $2ab \in \mathbb R$, we have that $2ab \leq |2ab|$, and by Theorem 4, we have that $2ab \leq |2a||b| = 2|a||b|$. By Axiom 4, $a^2 + 2ab + b^2 \leq a^2 + 2|a||b| + b^2 = |a|^2 + 2|a||b| + |b|^2 = (|a| + |b|)^2$. We now have the fact that $|a+b|^2 \leq (|a| + |b|)^2$."


My main question is, did the coursebook mean that I should be this rigorous when proving theorems like these? And also, how does one prove the statement that comes from squaring the two sides? Since we're dealing with inequality, don't we have to use the rules of inequality rather than just using "intuition"?
All answers are appreciated. 
 A: As egreg demonstrated in his answer, you certainly don't need the function $g(x) = \sqrt x$ in your 'toolbox' to derive the triangle inequality. But the OP indicated in his comments that he thought using the function $f(x) = x^2$ was a 'guess'. 
The problem is that mathematicians already know the 'end game', including 'tricks' and what's important.
How about a reset. We want to prove the triangle inequality holds true in the real line. We start by 'playing around' by using actual numbers to get a feel for things (this is always allowed, even in a rigorous course). Then we can write out a rigorous proof, sketched out here.
Case 0: If $a = 0$ or $b = 0$ then $|a + b| = |a| + |b|$.
Case 1: If $a > 0$ and $b > 0$ then $|a + b| = |a| + |b|$.
Case 2: If $a > 0$ and $b < 0$ then $|a + b| < |a| + |b|$.
Case 3: If $a < 0$ and $b < 0$ then $|a + b| = |a| + |b|$.
Case 4: If $a < 0$ and $b > 0$ then $|a + b| < |a| + |b|$.
A: From $x\le|x|$ you derive $ab\le|ab|$; you also know that $|ab|=|a||b|$. Since $2\ge0$, because $1=1^2\ge0$ and so $1+1\ge0+0$, we can state
$$
2ab\le 2|a||b|
$$
We can add terms to both sides and maintain the inequality:
$$
a^2+2ab+b^2\le a^2+2|a||b|+b^2
$$
Now we use that $a^2=|a|^2$ (easily proved by cases):
$$
a^2+2ab+b^2\le|a|^2+2|a||b|+|b|^2
$$
The standard algebra identity yields
$$
(a+b)^2\le(|a|+|b|)^2
$$
that we can also write
$$
|a+b|^2\le(|a|+|b|)^2
$$
Note that $|a|+|b|\ge0$. Now we need a lemma:

If $x\ge0$, $y\ge0$ and $x^2\le y^2$, then $x\le y$.

Suppose to the contrary that $x>y$ (meaning, as usual, that $y\le x$ and $y\ne x$). Then $x-y>y-y$ and so $c=x-y>0$. Now we can consider $x=y+c$ and so
$$
x^2=(y+c)^2=y^2+2cy+c^2
$$
On the other hand $c>0$ implies $2cy\ge0$ (here we use that $y\ge0$) and $c^2>0$. Thus $2cy+c^2>0$ and so
$$
y^2+2cy+c^2>y^2
$$
We have proved that $x>y\ge0$ implies $x^2>y^2$. By contrapositive, $x^2\le y^2$, with $x\ge0$ and $y\ge0$, implies $x\le y$.
Applying the lemma to $|a+b|^2\le(|a|+|b|)^2$ yields $|a+b|\le|a|+|b|$.
A: The book does seem to have a "practice what you preach violation" but maybe not.
Although it does  specifically states that all theorems must be proved using only the axioms and the theorems that have previously been given to us, it doesn't state that every axioms must be explicitly stated (which would make any proof in, say, Chapter 11 unfathomably tedious) but that clear and obvious applications of said axioms and theorems will be clear to reader.
$|a+b|^2 = (a+b)^2$.
I imagine that somewhere the text has a proposition/theorem that  states $(-a)^2 = a^2$. 
I notice you listed the basic the inequality axioms but none of the Ordered Fields definitions.  From which it can (and should have been proven) that $(-a)b = -(ab)$ and $-(-a) = a$.  And thus $(-a)^2=(-a)(-a)=-(-a*a)=-(-a^2)=a^2$ and $|a+b|=(\pm (a+b))^2 = (a+b)^2$.
[$-(-a)=a$.  Pf:  Def of field says inverses exist. We can prove the are unique but noting of $a+b = a+c=0$ then $b+a+b= b+a+c=0$ and $0+b=0+c$ and $b=c$.  So as to find $-(-a)$ we note that $-a+a=0$ means $-(-a)=a$:: $(-a)b= -ab$. Pf: $ab+(-a)b=(a+(-a))b=0*b=0$ so $(-a)b=-(ab)$:: $0*b=0$. Pf: $0*b =(0+0)b=0*b+0*b$.  So $0=0*b - 0*b =(0*b)+(0*b)-0*b=0*b$.]
So $|a+b|^2 = (a+b)^2$ which is equal to $a^2 + 2ab  +b^2=|a|^2 + 2ab +|b^2|$ by calculations.  $a^2 + 2ab +b^2 \le |a|^2+2|a||b| + |b|^2$ if and only if $ab\le |a||b|$.  And we can prove that.  $|a||b|=|ab|$ and our theorem says $-|ab|\le ab \le |ab|$.
Finally If $0\le a$ and $0\le b$ then Claim: $a\le b$ if and only if $a^2 \le b^2$.  Pf:  By axiom 5: we have if $a \le b$ than $a^2 = a*a\le a*b$.  And we also have $a*b\le b*b=b^2$ and be transitivity $a^2\le b^2$.  Likewise; if $a \not \le b$ we have $b < a$ and by the same reasoning $b^2 < a^2$ so if $a^2\le b^2$ we can assume that it must be the case $a \le b$
And that proves everything.
As to whether the book violated its own rules......maybe...... I'd have to see the full book and what propositions had been stated before and how explicitly.
One thing that is fair is that as a text goes along the presumed ability of the standard to fill in the missing details (such as hearing $(a+b)^2 \le (|a|+|b|)^2$ implies $a+b \le |a| + |b|$ will apply Axiom 5 twice.... maybe...)
Actually are you sure a theorem $a^2 \le b^2 \iff |a| \le |b|$ wasn't already proven?  That seems the biggest violation.
A: ''... it does not actually prove anywhere that if $ |a+b|^2≤(|a|+|b|)^2$, then $|a+b|≤|a|+|b|$. I thought we had to state each axiom explicitly step-by-step.''
This follows from monotonicity of multiplying with nonnegative real: Axiom 5.
On the contrary, $|a+b|>|a|+|b|$ implies
$|a+b|^2> (|a|+|b|) \cdot |a+b|$ by multiplying with $|a+b|$ and
$(|a|+|b|)\cdot |a+b| > (|a|+|b|)^2$ by multiplying with $|a|+|b|$.
Thus by transitivity of $>$, 
$|a+b|^2> (|a|+|b|)^2$.
A: $$|a+b|=\max (\,a+b,\, -(a+b)\,)=$$ $$=\max (\,a+b,\, (-a)+(-b)\,)\le$$ $$\le \max (\,|a|+b,\, (-a)+(-b)\,)\le$$ $$\le \max (\,|a|+|b|, \,(-a)+(-b)\,)\le$$ $$\le \max (\,|a|+|b|,\,|-a|+(-b)\,)\le$$ $$\le \max (|a|+|b|,\,|-a|+|-b|\,)=$$ $$=\max (\,|a|+|b|,\,|a|+|b|\,)=|a|+|b|.$$
