Proof of A Sum of Natural Numbers Exceeds Each Summand and Is Not One

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Let $a,b\in\mathbb{N}$. 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, applied to $m=a$ and $n=b$, $a+b\in\mathbb{N}$, and $1\in\mathbb{N}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets.

Clause above. By Arithmetic and Order of the Natural Numbers §difference, applied to $a$ and to $a+b$ in place of $b$, $a<a+b$ holds if and only if there is $d\in\mathbb{N}$ with $a+b=a+d$. The element $d=b$ of $\mathbb{N}$ is such a $d$. Hence $a<a+b$.

Clause not-one. Suppose, for a contradiction, that $a+b=1$. By the clause above, just proved, $a<a+b$, that is, $a<1$. By Arithmetic and Order of the Natural Numbers §least, applied to $a$, $1\le a$; so by Arithmetic and Order of the Natural Numbers §partial-order, applied to $1$ and $a$ in place of $a$ and $b$, $1<a$ or $1=a$. Thus, besides $a<1$, also $1<a$ or $a=1$ holds, so at least two of $a<1$, $a=1$ and $1<a$ hold. This contradicts Arithmetic and Order of the Natural Numbers §trichotomy, applied to $a$ and to $1$ in place of $b$, by which exactly one of them holds. Hence $a+b\neq1$.