# Mean of Unequal Real Numbers is Between them

## Theorem

$\forall x, y \in \R: x < y \implies x < \dfrac {x + y} 2 < y$

## Proof

First note that:

 $\displaystyle 0$ $<$ $\displaystyle 1$ Real Zero is Less than Real One $\displaystyle \leadsto \ \$ $\displaystyle 0 + 0$ $<$ $\displaystyle 1 + 1$ Real Number Inequalities can be Added $\displaystyle \leadsto \ \$ $\displaystyle 0$ $<$ $\displaystyle \frac 1 {1 + 1}$ Reciprocal of Strictly Positive Real Number is Strictly Positive $\text {(1)}: \quad$ $\displaystyle \leadsto \ \$ $\displaystyle 0$ $<$ $\displaystyle \frac 1 2$

Then:

 $\displaystyle x$ $<$ $\displaystyle y$ $\displaystyle \leadsto \ \$ $\displaystyle x + x$ $<$ $\displaystyle x + y$ Real Number Axioms: $\R O1$: compatibility with addition $\displaystyle \leadsto \ \$ $\displaystyle \paren {x + x} \times \frac 1 2$ $<$ $\displaystyle \paren {x + y} \times \frac 1 2$ Real Number Axioms: $\R O2$: compatibility with multiplication and from $(1)$ $\displaystyle \leadsto \ \$ $\displaystyle x$ $<$ $\displaystyle \frac {x + y} 2$ Definition of Real Division

Similarly:

 $\displaystyle x$ $<$ $\displaystyle y$ $\displaystyle \leadsto \ \$ $\displaystyle x + y$ $<$ $\displaystyle y + y$ Real Number Axioms: $\R O1$: compatibility with addition $\displaystyle \leadsto \ \$ $\displaystyle \paren {x + y} \times \frac 1 2$ $<$ $\displaystyle \paren {y + y} \times \frac 1 2$ Real Number Axioms: $\R O2$: compatibility with multiplication and from $(1)$ $\displaystyle \leadsto \ \$ $\displaystyle \frac {x + y} 2$ $<$ $\displaystyle y$ Definition of Real Division

$\blacksquare$