Wikipedia describes a metric space as $(M,d)$, where $M$ is a set and $d(x,y)$ is a metric. The axioms are as follows:
$d : M \times M \rightarrow \mathbb{R}$
$d( x, x) = 0$
$d( x, y ) = d ( y, x )$
$d( x, z ) \leq d( x, y ) + d( y , z )$
A proof of $d(x,y)\geq 0$ is provided as follows:
Proof 1 (from Wikipedia)
(1) $d(x,y)+d(y,x)\geq d(x,x)$ by triangle inequality
(2) $d(x,y)+d(x,y)\geq d(x,x)$ by symmetry
(3) $2 \times d(x,y)\geq 0$ by identity of indiscernibles
(4) $d(x,y)\geq 0$ we have non-negativity
It seems to me that a model of real numbers $\mathbb{R}$ is included in the metric space axioms and proof. I assume that the reasoning from (3) to (4) is provided by division by 2 over the inequality of two real numbers .
Proof 2 represents a variation of Proof 1, were step (3) differs from Proof 1.
Proof 2
(1) $d(x,y)+d(y,x)\geq d(x,x)$ by triangle inequality
(2) $d(x,y)+d(x,y)\geq d(x,x)$ by symmetry
(3) $d(x,y)+d(x,y)\geq 0$ by identity of indiscernibles
(4) $d(x,y)\geq 0$ by $\forall z \in \mathbb{R} \bullet((z + z) \geq 0) \Rightarrow (z \geq 0))$
Is the rule used to infer (4) from (3) valid? If it is,what property of real numbers is being invoked?
The reason I am using $((z + z) \geq 0) \Rightarrow (z \geq 0))$ instead of $((2 * z) \geq 0) \Rightarrow (z \geq 0))$ is that I can get the former, but not the latter, to work in a theorem prover.
It's in the definition. $d:\mathbb M \times M \to \mathbb R$ so by definition $d(x,y)$ is a real number. Note, all the arithmetic and ordering and algebra you are doing is in $d(w,u)$ values in $\mathbb R$. We are doing nothing in the space $M$ itself except comparing whether two values are equal or not.
If $x < 0$ then $x+x < 0 + x$ (axiom: if $a < b$ then for all $x$, $a+x< b+x$.)
So $x + x < x$ and $x < 0$. So $x+x < 0$ (by transitivity).
By trichotomy this contradicts $x + x \ge 0$.
So if $x + x \ge 0$ then $x < 0$ is impossible. So by trichotomy $x > 0$ or $x = 0$.
......
The second proof is sidestepping (why I don't know) the algebraic natural of the reals.
$x + x = 2x$ ("Why? Well, that's for the algebra class... I'm teaching metric spaces, so I dont know.... I guess")
And $2x \ge 0\implies x \ge 0$ (ditto)
To avoid the issue it uses a more basic abstract idea.
....
I'm being a little facetious but $1 + 1 = 2$ and $x + x =2x$ by definition and by distributions. But proving $2> 0$ and that $2 > 0\implies \frac 12 > 0$ is not trivial. (It's not hard but it's not trivial). So the issue really is Which Framework of Axioms are you applying. Can we assume "basic algebra" (in which case $x + x = 2x$ and $2> 0$ and $2x \ge 0 \implies x \ge 0$ is all obvious and acceptable)? Or are we assuming nothing but what we have been given (then we must prove $x + x \ge 0\implies x \ge 0$).
....
But in any event. $d(w,u)$ IS a real number and all of these are real number arithmetic.
If $d(x,y)=n$ is a integer and $d(x,y)$ is not a perfect square then $\sqrt{d(x,y)}$ is irrational.
That is a valid (albeit it irrelevant and non-analytical) observation.
....
And to save you trouble ahead, when asked to prove that that by notation: $x\cdot x\cdot .... \cdot x = x^m$ where $x$ is some abstract space and $\cdot$ is abstract associative binary operation on $X$, and you are asked to prove $x^mx^n = x^{m+n}$..... $m,n$ are integers and $+$ is addition, and $m+n$ does mean "take $m$ things and then continue with $n$ more things" and simplying saying "$\cdot$ is associative; so performing an opperation $m$ times ant then another $n$ times so you did it $m+n$ times is the same as performing it $m$ times and then perfoming it $n$ times and performing the operation on the results" is a proof.