不等式

1：$b-a\in P$ かつ $c-b\in P$ であるから、def-inequality-order-axioms の 2 により $(c-b)+(b-a)=c-a\in P$、すなわち $a< c$ である。
2：$(b+c)-(a+c)=b-a\in P$ であるから $a+c< b+c$ である。後半は $a+c< b+c< b+d$ と 1 による。
3：$c>0$ のとき、$b-a\in P$ と $c\in P$ から $(b-a)c=bc-ac\in P$、すなわち $ac< bc$ である。$c<0$ のときは $-c\in P$ なので $(b-a)(-c)=ac-bc\in P$、すなわち $bc< ac$ である。
4：$a>0$ とする。$1/a<0$ なら $-1/a\in P$ で、$a\cdot(-1/a)=-1\in P$ となるが、ex-inequality-square により $1\in P$ なので 1 の条件に反する。$1/a=0$ は $a\cdot(1/a)=1\ne0$ に反する。よって $1/a>0$ である。$0< a< b$ のとき、$1/(ab)>0$ であり（前半と 2 により $ab>0$、その逆数も正）、$a< b$ の両辺に $1/(ab)$ を掛けて（3）$1/b<1/a$ を得る。
5：$b-a$ に def-inequality-order-axioms の 1 を適用すればよい。$\le$ が反射的・推移的（1 による）・反対称的（$a\le b$ かつ $b\le a$ で $a\ne b$ なら $a< b$ かつ $b< a$ となり 1 に反する）で任意の 2 元が比較可能であるから、$\le$ は全順序である。
$\le$ に置き換えた主張は、等号の場合を別に確かめれば同様である。$\square$

まず次の補助的な主張を $n$ に関する帰納法で示す。「正の実数 $x_1,\ldots,x_n$ が $x_1x_2\cdots x_n=1$ を満たすなら $x_1+\cdots+x_n\ge n$ であり、等号は $x_1=\cdots=x_n=1$ のときに限る。」$n=1$ では $x_1=1$ で等号が成り立つ。$n$ で正しいとし、積が $1$ の正の実数 $x_1,\ldots,x_{n+1}$ をとる。番号を付け替えて $x_1$ を最小、$x_{n+1}$ を最大としてよい。積が $1$ だから $x_1\le1\le x_{n+1}$ である（すべて $>1$ または すべて $<1$ なら積が $1$ にならない）。$n$ 個の正の実数 $x_1x_{n+1},x_2,\ldots,x_n$ の積は $1$ なので、帰納法の仮定により $x_1x_{n+1}+x_2+\cdots+x_n\ge n$ である。したがって
$$ x_1+x_2+\cdots+x_{n+1}=(x_1x_{n+1}+x_2+\cdots+x_n)+x_1+x_{n+1}-x_1x_{n+1}\ge n+x_1+x_{n+1}-x_1x_{n+1}=n+1+(x_{n+1}-1)(1-x_1) $$
であり、$x_{n+1}-1\ge0$、$1-x_1\ge0$ から最右辺は $n+1$ 以上である。等号が成り立つには $(x_{n+1}-1)(1-x_1)=0$ が必要で、$x_{n+1}=1$ ならすべての $x_i\le1$ かつ積が $1$ なのですべて $1$、$x_1=1$ ならすべての $x_i\ge1$ かつ積が $1$ なのですべて $1$ である。逆にすべて $1$ なら等号が成り立つ。
定理を示す。ある $a_i$ が $0$ なら左辺は $0$ で右辺は非負だから不等式は成り立ち、等号は右辺が $0$、すなわちすべての $a_j$ が $0$ のときに限る。すべての $a_i$ が正のとき、$G:=\sqrt[n]{a_1\cdots a_n}>0$ とおき（正の実数の $n$ 乗根の存在は実数の完備性による）、$x_i:=a_i/G$ とおくと $x_1\cdots x_n=1$ であるから、補助的な主張により $\sum_i a_i/G\ge n$、すなわち $(a_1+\cdots+a_n)/n\ge G$ である。等号はすべての $x_i=1$、すなわち $a_1=\cdots=a_n=G$ のときに限る。$\square$

$A:=\sum a_i^2$、$B:=\sum b_i^2$、$C:=\sum a_ib_i$ とおく。$A=0$ ならすべての $a_i=0$（ex-inequality-square と def-inequality-order-axioms の 2 により、平方の和が $0$ なら各平方は $0$）で、両辺とも $0$ となり等号が成り立ち、このとき $(a_i)$ は零ベクトルなので線形従属である。以下 $A>0$ とする。任意の実数 $t$ について
$$ 0\le\sum_{i=1}^{n}(ta_i-b_i)^2=At^2-2Ct+B $$
である（ex-inequality-square と def-inequality-order-axioms の 2）。$t=C/A$ を代入すると
$$ 0\le A\frac{C^2}{A^2}-2\frac{C^2}{A}+B=B-\frac{C^2}{A} $$
であり、両辺に $A>0$ を掛けて $C^2\le AB$ を得る。等号 $C^2=AB$ が成り立つのは $\sum(ta_i-b_i)^2=0$（$t=C/A$）のとき、すなわちすべての $i$ について $b_i=ta_i$ のときに限る。逆に $b_i=ta_i$ なら $C=tA$、$B=t^2A$ で $C^2=t^2A^2=AB$ である。$A>0$ かつ $a_i=tb_i$（すべての $i$）の場合は $t\ne0$ で $b_i=t^{-1}a_i$ となるので上に含まれる。$\square$

両辺は非負なので 2 乗して比べればよい。左辺の 2 乗は $\sum a_i^2+2\sum a_ib_i+\sum b_i^2$、右辺の 2 乗は $\sum a_i^2+2\sqrt{\sum a_i^2}\sqrt{\sum b_i^2}+\sum b_i^2$ であるから、示すべきは $\sum a_ib_i\le\sqrt{\sum a_i^2}\sqrt{\sum b_i^2}$ であり、これは thm-inequality-cauchy-schwarz の両辺の平方根をとったものから従う（$\sum a_ib_i\le|\sum a_ib_i|$）。$\square$

任意の $i,j$ について、$a_i-a_j$ と $b_i-b_j$ は同符号（または一方が $0$）なので $(a_i-a_j)(b_i-b_j)\ge0$ である。$i,j$ について総和をとると
$$ 0\le\sum_{i=1}^{n}\sum_{j=1}^{n}(a_i-a_j)(b_i-b_j)=2n\sum_{i}a_ib_i-2\Bigl(\sum_ia_i\Bigr)\Bigl(\sum_jb_j\Bigr) $$
であり、$2n^2$ で割れば主張の不等式になる。向きが逆の場合は $(a_i-a_j)(b_i-b_j)\le0$ から同様である。$\square$

左辺は $x,y,z$ について対称なので $x\ge y\ge z\ge0$ としてよい。左辺の第 1 項と第 2 項の和は
$$ (x-y)\bigl[x^t(x-z)-y^t(y-z)\bigr] $$
であり、$x\ge y\ge0$ から $x^t\ge y^t$（冪関数 $u\mapsto u^t$（$t>0$）の単調性。Rud76）、$x-z\ge y-z\ge0$ なので角括弧の中は非負、$x-y\ge0$ とあわせて非負である。第 3 項は $z^t(z-x)(z-y)=z^t(x-z)(y-z)\ge0$ である。よって左辺は非負である。等号は「$x=y$ または $x^t(x-z)=y^t(y-z)$」かつ「$z=0$ または $x=z$ または $y=z$」のときで、整理すると $x=y=z$ または（$x=y$ かつ $z=0$）の場合に限る（$x>y$ かつ $x^t(x-z)=y^t(y-z)$ は $x^t>y^t$、$x-z>y-z\ge0$ から起こらない）。対称性により、2 つが等しく残りが $0$ の場合が等号の場合である。$\square$