# 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 \implies \ \$ $\displaystyle 0 + 0$ $<$ $\displaystyle 1 + 1$ Real Number Inequalities can be Added $\displaystyle \implies \ \$ $\displaystyle 0$ $<$ $\displaystyle \frac 1 {1 + 1}$ Reciprocal of Strictly Positive Real Number is Strictly Positive $(1):\quad$ $\displaystyle \implies \ \$ $\displaystyle 0$ $<$ $\displaystyle \frac 1 2$

Then:

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

Similarly:

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

$\blacksquare$