Proof of Splitting the Segment [m+n] into [m] and a Shifted Copy of [n]

Each result cited is universally quantified over the data in its own statement.

Preliminaries. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, $[p]=\{i\in\mathbb{N}:i\le p\}$ for $p\in\mathbb{N}_{0}$, so the elements of a segment are natural numbers; and $[p]=\{1,\dots,p\}$ by Intervals of Natural Numbers §segment. By Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §closed, $m+n\in\mathbb{N}$, so that the segment $[m+n]$ is defined, and $m+1\in\mathbb{N}$, so $1\le m+1$ by Arithmetic and Order of the Natural Numbers §least. Hence Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §split, applied with $1$, $m$ and $n$ in place of its $m$, $n$ and $p$, gives

$$[m+n]=\{1,\dots,m+n\}=\{1,\dots,m\}\cup\{m+1,\dots,m+n\}=[m]\cup\{m+1,\dots,m+n\},\tag{1}$$

with $[m]$ and $\{m+1,\dots,m+n\}$ disjoint; therefore

$$\{m+1,\dots,m+n\}=[m+n]\setminus[m].\tag{2}$$

By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift, applied with $1$, $n$ and $m$ in place of its $m$, $n$ and $p$, the map $j\mapsto j+m$ is a bijection from $\{1,\dots,n\}=[n]$ onto $\{1+m,\dots,n+m\}$. For $j\in[n]$ we have $j\in\mathbb{N}$, so $j+m=m+j$, and also $1+m=m+1$ and $n+m=m+n$, by Arithmetic and Order of the Natural Numbers §commutative. Hence the map $\sigma:[n]\to\{m+1,\dots,m+n\}$, $\sigma(j)=m+j$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol §map-symbol), has the same values as $j\mapsto j+m$ and is a bijection onto $\{m+1,\dots,m+n\}$.

Clause sum. $m+n\in\mathbb{N}$, as shown in the Preliminaries. Since $n\in\mathbb{N}$, $m<m+n$ by Arithmetic and Order of the Natural Numbers §difference, so $m\le m+n$ by Arithmetic and Order of the Natural Numbers §partial-order, and $[m]\subseteq[m+n]$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §inclusion.

Clause shift. For $j\in[n]$, $m+j=\sigma(j)\in\{m+1,\dots,m+n\}=[m+n]\setminus[m]$ by (2), so $m+j\in[m+n]$ and $m+j\notin[m]$. By (2), the map $[n]\to[m+n]\setminus[m]$, $j\mapsto m+j$, is $\sigma$, which is injective and surjective onto $[m+n]\setminus[m]$; so it is a bijection by Injective, Surjective and Bijective Functions between Classes §bijective.

Clause cases. Every value $m+j$ ($j\in[n]$) of $\sigma$ lies in $[m+n]\setminus[m]$, and by Injective, Surjective and Bijective Functions between Classes §surjective every element of $[m+n]\setminus[m]$ is such a value; so $\{m+j:j\in[n]\}=[m+n]\setminus[m]$. Let $k\in[m+n]$. Then $k$ lies in $[m]$ or in $[m+n]\setminus[m]$, and not in both; this is the first assertion. Suppose now that $k\in[m+n]\setminus[m]$, and take $j\in[n]$ with $k=m+j$. As $j\in\mathbb{N}$, $m<m+j=k$ by Arithmetic and Order of the Natural Numbers §difference, so $m\le k$ by Arithmetic and Order of the Natural Numbers §partial-order. Since $j\in\mathbb{N}_{0}$ and $m+j=k$, The Difference of Two Natural Numbers with Zero §difference gives $k-m=j$; hence $k-m\in[n]$ and $k=m+(k-m)$. Finally, if $j'\in[n]$ and $k=m+j'$, then $j'\in\mathbb{N}_{0}$ and $m+j'=k$, so $j'=k-m$ by the uniqueness in The Difference of Two Natural Numbers with Zero §difference.