超準解析

$\hat r_j:=(r_j,r_j,\dots)$ とおく。Łośの定理 の定理「Łoś の定理」により
$$ {}^*\mathfrak{R}\models\varphi([\hat r_1],\dots,[\hat r_n])\iff S:=\{i\in\mathbb{N}\mid\mathfrak{R}\models\varphi(r_1,\dots,r_n)\}\in U $$
である。$S$ は $i$ によらない条件で定まるので、$\mathfrak{R}\models\varphi(\vec r)$ なら $S=\mathbb{N}\in U$、そうでなければ $S=\emptyset\notin U$ である。よって前半が成り立つ。
後半：原子論理式 $x_1=x_2$、$x_1+x_2=x_3$、$x_1\cdot x_2=x_3$、$x_1< x_2$、$\underline{A}(x_1,\dots,x_n)$、$\underline{g}(x_1,\dots,x_n)=x_{n+1}$ に前半を当てると、実数どうしの等号・和・積・大小、$A$ への所属、$g$ の値が ${}^*\mathfrak{R}$ でも同じになる。たとえば $\vec r\in\mathbb{R}^n$ について $\vec r\in{}^*A\iff\vec r\in A$ なので ${}^*A\cap\mathbb{R}^n=A$ である。$\square$

順序体の公理（順序体 の記事の定義「順序体の公理」）は、記号 $\underline{0},\underline{1},\underline{+},\underline{\cdot},\underline{<}$ だけを使った有限個の $L_{\mathbb{R}}$ の文である（逆元の存在は $\forall x\,(x\neq\underline 0\to\exists y\ x\cdot y=\underline1)$ と書ける）。これらは $\mathfrak{R}$ で成り立つので、thm-nsa-transfer により ${}^*\mathfrak{R}$ でも成り立つ。$\mathbb{R}$ が部分順序体であることは thm-nsa-transfer の後半による。$\square$

正の実数 $r$ をとる。$\{i\mid0< 1/(i+1)< r\}$ は $i>1/r$ となる $i$ をすべて含むので補集合が有限であり、$U$ に属する。よって $0< \varepsilon< r$ である。同様に $\{i\mid i>r\}$ は補集合が有限なので $\omega>r$ である。$\{i\mid i\in\mathbb{N}\}=\mathbb{N}\in U$ なので $\omega\in{}^*\mathbb{N}$ である。$\varepsilon$ は $0$ でも正の実数でもないので実数でない。$\square$

要点：実数の上界・誤差を足したり掛けたりする、$\varepsilon$-$\delta$ 論法と同じ評価である。

一意性：実数 $r,s$ がともに $x$ に無限に近ければ、prop-nsa-arith により $r\approx s$、すなわち $r-s$ は無限小な実数である。正の実数 $\lvert r-s\rvert$ は自分自身より小さくはなれないので、$r=s$ である。
存在：$x$ は有限なので、ある実数 $b$ で $-b< x< b$ である。$X:=\{s\in\mathbb{R}\mid s< x\}$ とおくと、$-b\in X$ で、$X$ の元はどれも $b$ より小さい。実数の上限性質（実数 の記事の定義「上限性質」）により、$t:=\sup X$ が存在する。正の実数 $r$ をとる。$t+r$ は $X$ に属さないので（$t$ より大きいから）$x\le t+r$ である。$t-r$ は $X$ の上界でないので、ある $s\in X$ で $t-r< s< x$ である。よって $\lvert x-t\rvert\le r$ であり、$r$ は任意なので（$r/2$ に当てれば狭義の不等号になる）$x-t$ は無限小、$x\approx t$ である。
準同型：$x\approx\operatorname{st}(x)$、$y\approx\operatorname{st}(y)$ なら、prop-nsa-arith により $x+y\approx\operatorname{st}(x)+\operatorname{st}(y)$、また $xy-\operatorname{st}(x)\operatorname{st}(y)=x(y-\operatorname{st}(y))+\operatorname{st}(y)(x-\operatorname{st}(x))$ は無限小である。一意性から $\operatorname{st}(x+y)=\operatorname{st}(x)+\operatorname{st}(y)$、$\operatorname{st}(xy)=\operatorname{st}(x)\operatorname{st}(y)$ であり、実数 $r$ では $\operatorname{st}(r)=r$ なので全射である。核は定義から $\mathcal{I}$ である。順序：$x\le y$ で $\operatorname{st}(x)>\operatorname{st}(y)$ とすると、$d:=\operatorname{st}(x)-\operatorname{st}(y)$ は正の実数で、$x-y\approx d$ より $x-y>d/2>0$ となって矛盾する。$\square$

$\bar f$ を $f$ を $D$ の外で $0$ とおいた関数とし、$\underline{D}$、$\underline{\bar f}$、$\underline{\lvert\cdot\rvert}$ などを使って主張を $L_{\mathbb{R}}$ の論理式で書く。
1 ⇒ 2：$x\in{}^*D$、$x\approx c$、$x\neq c$ とし、正の実数 $\varepsilon$ をとる。1 により正の実数 $\delta$ があって、$L_{\mathbb{R}}$ の文
$$ \forall x\,\bigl(\underline{D}(x)\land0< \lvert x-\underline c\rvert< \underline\delta\ \to\ \lvert\bar f(x)-\underline L\rvert< \underline\varepsilon\bigr) $$
が $\mathfrak{R}$ で成り立つ。thm-nsa-transfer によりこの文は ${}^*\mathfrak{R}$ でも成り立つ。$x-c$ は $0$ でない無限小なので $0< \lvert x-c\rvert< \delta$ であり、${}^*\bar f(x)={}^*f(x)$ について $\lvert{}^*f(x)-L\rvert< \varepsilon$ である。$\varepsilon$ は任意なので ${}^*f(x)\approx L$ である。
2 ⇒ 1：1 が成り立たないとする。ある正の実数 $\varepsilon$ について、文
$$ \forall\delta\,\Bigl(0< \delta\ \to\ \exists x\,\bigl(\underline{D}(x)\land0< \lvert x-\underline c\rvert< \delta\land\lvert\bar f(x)-\underline L\rvert\ge\underline\varepsilon\bigr)\Bigr) $$
が $\mathfrak{R}$ で成り立つ。thm-nsa-transfer により ${}^*\mathfrak{R}$ でも成り立つ。$\delta$ に正の無限小を代入すると、$x\in{}^*D$ で $0< \lvert x-c\rvert< \delta$ かつ $\lvert{}^*f(x)-L\rvert\ge\varepsilon$ となるものがある。この $x$ は $x\approx c$、$x\neq c$ を満たすが ${}^*f(x)\not\approx L$ なので、2 が成り立たない。$\square$

1：$c$ が $D$ の孤立点なら、$c$ を中心とするある実数の開区間が $D$ と $c$ だけで交わり、移行原理により $x\in{}^*D$、$x\approx c$ なら $x=c$ となるので、両辺とも成り立つ。孤立点でなければ、$c$ での連続性は $\lim_{x\to c}f(x)=f(c)$ と同値であり、$x=c$ では ${}^*f(c)=f(c)$ なので、thm-nsa-limit から従う。
2：$D':=\{h\neq0\mid c+h\in D\}$ 上の関数 $q(h):=(f(c+h)-f(c))/h$ に thm-nsa-limit を当てる（$0$ は $D'$ の集積点である）。恒等式 $\forall h\,\bigl(\underline{D'}(h)\to\bar q(h)\cdot h=\bar f(\underline c+h)-\underline{f(c)}\bigr)$ を移行原理で移すと、$h\in{}^*D'$ について ${}^*q(h)=({}^*f(c+h)-f(c))/h$ である。$D$ が $c$ を含む開区間 $(c-\eta,c+\eta)$ を含むので、移行原理により $0< \lvert h\rvert< \eta$ の超実数 $h$ は ${}^*D'$ に属し、とくに $0$ でない無限小はすべて ${}^*D'$ に属する。$\square$

段 1（実数での有限の分割）． 正の整数 $n$ について、$\delta_n:=(b-a)/n$、$x_k:=a+k\delta_n$ とおく。$f(x_k)\ge0$ となる最小の $k\in\{1,\dots,n\}$ がある（$k=n$ では $f(x_n)=f(b)>0$）。$m:=k-1$ とおくと、$k$ の最小性と $f(x_0)=f(a)<0$ から $f(x_m)<0\le f(x_{m+1})$ である。したがって、$\mathbb{R}$ で次の文が成り立つ。
$$ \forall n\,\Bigl(\underline{\mathbb{N}}(n)\land n\ge1\ \to\ \exists m\,\bigl(\underline{\mathbb{N}}(m)\land m< n\land\bar f(\underline a+m\cdot\tfrac{\underline b-\underline a}{n})<0\le\bar f(\underline a+(m+1)\cdot\tfrac{\underline b-\underline a}{n})\bigr)\Bigr) $$
段 2（移行）． thm-nsa-transfer により、この文は ${}^*\mathfrak{R}$ でも成り立つ。prop-nsa-exist の無限大の超自然数 $\omega$ を $n$ に代入すると、$M\in{}^*\mathbb{N}$、$M< \omega$ で、$\delta:=(b-a)/\omega$、$x:=a+M\delta$、$y:=x+\delta$ について ${}^*f(x)<0\le{}^*f(y)$ となるものがある。$\delta$ は無限小なので $y\approx x$ である。また $m< n$ なら $a\le a+m(b-a)/n< b$ という実数の文を移すと $a\le x< b$、同様に $a< y\le b$ なので、$x,y\in{}^*[a,b]$ である。
段 3（標準部分）． $x$ は有限なので $c:=\operatorname{st}(x)$ が定まり、thm-nsa-standard-part の順序の保存から $a\le c\le b$ である。$y\approx x\approx c$ なので、cor-nsa-continuity の 1（$D=[a,b]$）により ${}^*f(x)\approx f(c)$、${}^*f(y)\approx f(c)$ である。標準部分をとると、${}^*f(x)<0$ から $f(c)=\operatorname{st}({}^*f(x))\le0$、${}^*f(y)\ge0$ から $f(c)\ge0$ である。よって $f(c)=0$ である。$\square$