Structure of $\Bbb N$ in $\Bbb R$ and substraction in $\Bbb N$. I'm working with the definition of $\Bbb N$ as the intersection of all inductive susbsets of $\Bbb R$, being a subset $I$ inductive iff $1\in I$ and $\forall n(n\in I\to n+1\in I)$.
By the way, $\Bbb R$ is defined by its axioms: that is, as a complete, ordered field. Then, $\Bbb N$ is defined inside of $\Bbb R$ as described above.
I'm trying to prove that if $x$ is a positive real number then $[x,x+1)$ has exactly one natural number. Intuitively, I'm trying to get the 'spacing' between natural numbers from the fact that they are in every inductive set.
My try:

*

*I started stating that if $x,y\in\Bbb N$ and $y<x$ then $x-y\in\Bbb N$, but I don't know how to prove it. I have defined the set $A=\{z\in \Bbb R:z\le x\vee z-x\in\Bbb N\}$ to see that it is inductive, but I couldn't prove that $z\in A\to z+1\in A$ when $z\le x$ and $z+1>x$.

If I manage to prove this, it is done, because if $x-y\in \Bbb N$ then $x-y\ge 1$.
 A: You can prove it like this ; Since all reals are bounded by naturals you know that the set of all numbers greater than equal to $x+1$ is non empty by induction you can prove that it also must have a least element so there is a least natural $n$ such that $x+1\le n$ which ismplies that $n-1$ lies in your interval .
A: If $A$ is inductive, then so is $A\setminus (-\infty,1)$. Therefore, $\Bbb N\subseteq [1,\infty)$.
Let $$ S=\{\,x\in \Bbb R\mid \#([x,x+1)\cap\Bbb N)\ge 2\,\}$$
and assume $S\ne \emptyset$. Then $0\le \inf S<\infty$. We can pick $s\in S$ with $\inf S\le s<\inf S+1$. Let $n_1,n_2$ be two of the natural numbers $\in [s,s+1)$, where $s\le n_1<n_2<s+1$.
As $n_2-1,n_1\in [n_2-1,n_2)$ and $n_2-1<\inf S$, we conclude that $n_2-1\notin \Bbb N$. Also, $n_2>n_1\ge 1$. Then $\Bbb N\setminus \{n_2\}$ is inductive, contradicting $n_2\in \Bbb N$. We conclude that $S=\emptyset$, i.e., each $[x,x+1)$ contains at most one natural number.
A similar argument shows that
$$ T:=\{\,x\in \Bbb R_{>0}\mid [x,x+1)\cap\Bbb N=\emptyset\,\}$$
is empty, whence your desired result.
