Proof of The Reflection of a Closed Interval

Computations with real numbers are those of The Real Numbers as a Type (vi).

Proof of (i). Let $u\in[a,b]$, so $a\le u\le b$. Then $a=a+b-b\le a+b-u\le a+b-a=b$, so $a+b-u\in[a,b]$. Hence (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v), with $[a,b]$ for $A$ and $B$ and the expression $a+b-u$ for $t$) there is a map $\psi:[a,b]\to[a,b]$ with $\psi(u)=a+b-u$ for every $u\in[a,b]$, and it is the only one, by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv).

Proof of (ii) and (iii). For $u,v\in[a,b]$, $\psi(\psi(u))=a+b-(a+b-u)=u$ and $\psi(u)-\psi(v)=v-u$, so $|\psi(u)-\psi(v)|=|v-u|=|u-v|$.

Proof of (iv). Since $[a,b]\subseteq\mathbb{R}$, $\psi$ is also a map $[a,b]\to\mathbb{R}$, by Functions, Values of a Function, and Functions from One Class to Another (iii). Let $s\in[a,b]$ and let $\varepsilon>0$ be real; put $\delta=\varepsilon$. Every $t\in[a,b]$ with $|t-s|<\delta$ satisfies $|\psi(t)-\psi(s)|=|t-s|<\varepsilon$, by (iii). By the $\varepsilon$-$\delta$ form of continuity in The Real Line: Standing Notation and Background for Calculus on Intervals (vi), $\psi$ is continuous at $s$ relative to $[a,b]$; as $s$ was arbitrary, $\psi$ is continuous on $[a,b]$, by Continuous Map Between Metric Spaces (ii).

Proof of (v). As in the proof of (iv), $\psi$ is a map $[a,b]\to\mathbb{R}$. Let $s\in[a,b]$ and let $\varepsilon>0$ be real; put $\delta=1$. For every $t\in[a,b]$ with $0<|t-s|<\delta$ we have $t-s\neq0$ and $\psi(t)-\psi(s)=s-t=-(t-s)$, so

$$\Bigl|\frac{\psi(t)-\psi(s)}{t-s}-(-1)\Bigr|=|(-1)-(-1)|=0<\varepsilon .$$

So $-1$ is a derivative of $\psi$ at $s$, by Derivative of a Real Function on an Interval (i) with $[a,b]$ for $I$; hence $\psi$ is differentiable at $s$ and $\psi'(s)=-1$, by Derivative of a Real Function on an Interval (ii). As $s\in[a,b]$ was arbitrary, $\psi$ is differentiable, by Derivative of a Real Function on an Interval (iii).