I want to prove that: $∀r,s∈N,r<s∧r>0⇒s∤r$
I'm thinking of rewriting this as a contrapositive along with a translation of the divides predicate:
$∀r,s∈N,∃k∈Z,r=sk⇒r≥s∨r≤0$
Where would I go from here, assuming that the contrapositive was the right way to go?
On
Maybe proceed by contradiction: assume $s\mid r$, then $r=sk$ for some $k\in\Bbb Z$. Since we have $r>0$, we must have $k>0$, so $sk>0$ (note, $s\neq 0$ since $0\nmid r>0$).
Well this produces our contradiction, since we also suppose $r<s$, so we have $$r=sk\geq s>r$$
On
Here is how I would approach this: try and simplify $\;s \mid r\;$ after expanding its definition, under the assumption that $\;0<r<s\;$.
In this answer I'm assuming all variables range over the integers.
So we calculate as follows: $% \require{begingroup} \begingroup \newcommand{\calc}{\begin{align} \quad &} \newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}} \newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} } \newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & } \newcommand{\endcalc}{\end{align}} \newcommand{\Ref}[1]{\text{(#1)}} \newcommand{\then}{\Rightarrow} \newcommand{\false}{\text{false}} %$ $$\calc s \mid r \op\equiv\hint{definition of 'divides'} \langle \exists k :: ks=r \rangle \op\then\hint{using assumption $\;0<r<s\;$} \langle \exists k :: 0<ks<s \rangle \op\equiv\hint{divide by $\;s\;$, using $\;s>0\;$} \langle \exists k :: 0<k<1 \rangle \op\equiv\hint{$\;k\;$ is an integer} \false \endcalc$$ In other words, we've proved $$ \langle \forall r,s :: 0<r<s \;\then\; s \not\mid r \rangle $$
$% \endgroup %$
For your second statement, if $r$ is not positive then we are done. Else, $k>0$ since $s$ is positive too. Then $k\geq 1$ so $r=ks\geq 1\cdot s = s$.