平方根

存在：$S=\{x\in\mathbb{R}\mid x\ge0,\ x^2\le a\}$ とおく。$0\in S$ なので $S$ は空でない。$x>1+a$ ならば $x^2>x(1+a)\ge x>a$ なので $x\notin S$ であり、$S$ は $1+a$ を上界にもつ。実数の上限性質（実数の完備性）により $s=\sup S$ が存在し、$s\ge0$ である。$s^2=a$ を示す。
$s^2< a$ と仮定する。$0< h< 1$ かつ $h< (a-s^2)/(2s+1)$ となる $h$ をとると
$$ (s+h)^2=s^2+2sh+h^2< s^2+h(2s+1)< a $$
であるから $s+h\in S$ となり、$s$ が上界であることに反する。
$s^2>a$ と仮定する。このとき $s>0$ である。$h=(s^2-a)/(2s)$ とおくと $0< h\le s/2$ であり、
$$ (s-h)^2=s^2-2sh+h^2>s^2-2sh=a $$
である。$x\in S$ が $x>s-h$ を満たしたとすると、$x>s-h>0$ から $x^2>(s-h)^2>a$ となり $x\in S$ に反する。よって $s-h$ は $S$ の上界であり、$s-h< s$ は $s$ が最小の上界であることに反する。
以上から $s^2=a$ であり、$b=s$ が求めるものである。
一意性：$b,c\ge0$ が $b^2=c^2=a$ を満たすとすると $(b-c)(b+c)=b^2-c^2=0$ である。$b+c=0$ ならば $b,c\ge0$ より $b=c=0$ であり、$b+c\ne0$ ならば $b-c=0$ である。いずれにしても $b=c$ である。$\square$

1. $x^2=a$ ならば $(x-\sqrt a)(x+\sqrt a)=x^2-a=0$ なので $x=\sqrt a$ または $x=-\sqrt a$ であり、逆にこの 2 つは解である。$a>0$ ならば $\sqrt a>0$ なので 2 つは異なる。$a=0$ ならば両者は $0$ に一致する。実数の 2 乗は非負なので、$c< 0$ のとき解はない。
2. $\sqrt a\sqrt b\ge0$ かつ $(\sqrt a\sqrt b)^2=ab$ なので、thm-sqrt-real の一意性により $\sqrt{ab}=\sqrt a\sqrt b$ である。$b>0$ のときも同様に $\sqrt a/\sqrt b\ge0$、$(\sqrt a/\sqrt b)^2=a/b$ から従う。
3. $\sqrt a< \sqrt b$ ならば、非負の数どうしの不等式に $\sqrt a$ と $\sqrt b$ を掛けて $a=\sqrt a\sqrt a\le\sqrt a\sqrt b< \sqrt b\sqrt b=b$ である（2 つ目の不等号は $\sqrt b>0$ による）。逆に $\sqrt a\ge\sqrt b$ ならば同じ計算で $a\ge b$ となる。
4. $|x|\ge0$ かつ $|x|^2=x^2$ なので、一意性により $\sqrt{x^2}=|x|$ である。
5. 対称性から $a\ge b$ としてよい。$\sqrt b+\sqrt{a-b}\ge0$ であり
   $$ \bigl(\sqrt b+\sqrt{a-b}\bigr)^2=b+(a-b)+2\sqrt{b(a-b)}\ge a $$
   なので、3 により $\sqrt a\le\sqrt b+\sqrt{a-b}$、すなわち $0\le\sqrt a-\sqrt b\le\sqrt{a-b}$ である。$\square$

thm-sqrt-real は、各 $y\ge0$ に対して $f(x)=y$ となる $x\ge0$ がちょうど一つ、すなわち $x=\sqrt y$ であることを述べている。よって $f$ は全単射で、逆写像は $\sqrt{\phantom{y}}$ である。狭義単調増加は prop-sqrt-real-basic の 3 による。
一様連続性：$\varepsilon>0$ に対し $\delta=\varepsilon^2$ とおくと、$|y-y'|< \delta$ ならば prop-sqrt-real-basic の 5 により $|\sqrt y-\sqrt{y'}|\le\sqrt{|y-y'|}< \varepsilon$ である。
微分：$y\ne y_0$ のとき、$y-y_0=(\sqrt y-\sqrt{y_0})(\sqrt y+\sqrt{y_0})$ であり $\sqrt y+\sqrt{y_0}\ge\sqrt{y_0}>0$ なので
$$ \frac{\sqrt y-\sqrt{y_0}}{y-y_0}=\frac{1}{\sqrt y+\sqrt{y_0}} $$
である。連続性から $y\to y_0$ で右辺は $1/(2\sqrt{y_0})$ に収束する。$y_0=0$ では $y>0$ について $(\sqrt y-0)/(y-0)=1/\sqrt y$ であり、これは $y\to+0$ で上に有界でない。$\square$

prop-sqrt-real-basic の 2 により $\sqrt{ab}=\sqrt a\sqrt b$ なので
$$ \frac{a+b}{2}-\sqrt{ab}=\frac{(\sqrt a)^2-2\sqrt a\sqrt b+(\sqrt b)^2}{2}=\frac{(\sqrt a-\sqrt b)^2}{2}\ge0 $$
である。等号は $\sqrt a=\sqrt b$ のとき、prop-sqrt-real-basic の 3 により $a=b$ のときに限る。$\square$

$x_n>0$ ならば $x_{n+1}>0$ なので、帰納法により $x_n>0$ である。3 の等式は
$$ x_{n+1}-\sqrt a=\frac{x_n^2-2\sqrt a\,x_n+a}{2x_n}=\frac{(x_n-\sqrt a)^2}{2x_n} $$
による。右辺は非負なので $x_{n+1}\ge\sqrt a$ であり、1 が従う（これは prop-sqrt-am-gm を $x_n$ と $a/x_n$ に当てたものでもある）。$n\ge1$ では $x_n\ge\sqrt a$ より $x_n^2\ge a$ なので $x_n-x_{n+1}=(x_n^2-a)/(2x_n)\ge0$ となり、2 が従う。また $n\ge1$ では $0\le x_n-\sqrt a\le x_n$ なので
$$ x_{n+1}-\sqrt a=\frac{x_n-\sqrt a}{2x_n}\,(x_n-\sqrt a)\le\frac12(x_n-\sqrt a) $$
である。帰納法により $0\le x_n-\sqrt a\le 2^{-(n-1)}(x_1-\sqrt a)$ となり、$x_n\to\sqrt a$ である。$\square$

$z=a+bi$ について $u(z)=\sqrt{(|z|+a)/2}$、$v(z)=\sqrt{(|z|-a)/2}$ とおくと、$u,v$ は連続関数の合成なので $\mathbb{C}$ 全体で連続であり、$\sqrt z=u(z)+s(z)\,i\,v(z)$ である。
連続性：$z_0=a_0+b_0i$ とする。$b_0\ne0$ ならば $z_0$ の近くで $b$ の符号は一定なので $s$ は定数であり、$\sqrt z$ は $z_0$ で連続である。$b_0=0$、$a_0>0$ ならば $v(z_0)=0$ であり、$|s(z)v(z)|=v(z)\to0$ なので虚部は $0=\operatorname{Im}\sqrt{z_0}$ に収束し、実部 $u$ も連続だから $\sqrt z$ は $z_0$ で連続である。$z_0=0$ では $|\sqrt z|=\sqrt{|z|}\to0$ である。
不連続性：$c>0$、$z_0=-c$ とし、$t>0$ について $z=-c+ti$ と $z'=-c-ti$ を考える。$t\to+0$ で $u\to0$、$v\to\sqrt c$ なので $\sqrt z\to i\sqrt c$、$\sqrt{z'}\to-i\sqrt c$ である。極限が異なるので不連続である。
正則性：$z_0\in\mathbb{C}\setminus(-\infty,0]$ とする。この範囲では $u(z)>0$、すなわち $\operatorname{Re}\sqrt z>0$ である（$u(z)=0$ となるのは $|z|=-a$、すなわち $z\in(-\infty,0]$ のときに限る）。$z\ne z_0$ ならば $\sqrt z\ne\sqrt{z_0}$ であり、
$$ z-z_0=(\sqrt z-\sqrt{z_0})(\sqrt z+\sqrt{z_0}),\qquad \operatorname{Re}(\sqrt z+\sqrt{z_0})>0 $$
なので $\dfrac{\sqrt z-\sqrt{z_0}}{z-z_0}=\dfrac{1}{\sqrt z+\sqrt{z_0}}$ である。連続性から $z\to z_0$ で右辺は $1/(2\sqrt{z_0})$ に収束する。$\square$

そのような $f$ があったとし、$t\in[0,2\pi]$ について
$$ h(t)=\frac{f(\rho e^{it})}{\sqrt\rho\,e^{it/2}} $$
とおく。$h$ は $[0,2\pi]$ 上の連続関数であり、$h(t)^2=\rho e^{it}/(\rho e^{it})=1$ なので、$h(t)\in\{1,-1\}$ である。とくに $h$ は実数値である。$h$ が $1$ と $-1$ の両方の値をとるとすると、中間値の定理 により $h(t)=0$ となる $t$ があり矛盾する。よって $h$ は定数である。
一方、$\rho e^{2\pi i}=\rho$ と $e^{i\pi}=-1$ から
$$ h(2\pi)=\frac{f(\rho)}{\sqrt\rho\,e^{i\pi}}=-\frac{f(\rho)}{\sqrt\rho}=-h(0) $$
であり、$h(0)\ne0$ だから $h(2\pi)\ne h(0)$ である。これは $h$ が定数であることに反する。$\square$

要点：存在は連続汎関数計算で $b=\sqrt a$ を作り、$b$ が $a$ の多項式の極限であることから可換性が従う。一意性は、もう一つの正の平方根 $c$ と $b$ が生成する可換 $C^*$-環の各指標 $\chi$ で $\chi(b),\chi(c)\ge0$、$\chi(b)^2=\chi(c)^2$ となることによる。

$c^2=a$ とすると、$R$ が可換なので $(c-b)(c+b)=c^2-b^2=a-a=0$ であり、零因子がないので $c=b$ または $c=-b$ である。逆に $(-b)^2=b^2=a$ である。$a\ne0$ ならば $b\ne0$ であり、$1+1\ne0$ ならば $b-(-b)=(1+1)b\ne0$ なので $b\ne-b$ である。$\square$