Archimedean property by contrapositive Archimedean property of $\mathbb{R}$:
$$\forall x,y\in \mathbb{R}\text{ with }x>0,\exists n\in \mathbb{N}:nx>y. (*)$$
I saw how this theorem is proved by contradiction.
I would like to see how this theorem will look in the contrapositive form.
QUESTION 1: Can I put (*) in the conditional form "if A, then B"? My attempt:
$$\forall x,y\in \mathbb{R}\text{ with }x>0 \implies \exists n\in \mathbb{N}:nx>y. (**)?$$
Or "if for any real x and y with x>0 then there is natural n such that nx>y."
And the if part looks stangely.
QUESTION 2: If I can do that then how  will do look (**) in the contrapositive form "if not B, then not A"?
 A: 

Archimedean property of $\mathbb{R}$: $$\forall x,y\in
\mathbb{R}\text{ with }x>0,\exists n\in \mathbb{N}:nx>y.$$


Here, “with” means ‘such that’.

$$\forall x,y\in \mathbb{R}\text{ with }x>0 \implies
\exists n\in \mathbb{N}:nx>y.\tag2$$

Correction: $$\forall x,y\in \mathbb{R}\Big(x>0 \implies
\exists n\in \mathbb{N}:nx>y\Big).\tag{2c}$$
Leaving the “with” there is grammatically incorrect:

*

*✗ “for each $m$ with $m$ is positive implies that $m+1$ is positive”

versus

*

*✔ “for each $m,\:m$ is positive implies that $m+1$ is positive”

*✔ “for each $m,\:$ if $m$ is positive, then $m+1$ is positive”


"if for any real $x$ and $y$ with $x>0$ then there is natural $n$ such that $nx>y.$" And the "if" part looks strange.

Your translation is incoherent; correction:
“For each pair of real $x$ and $y,$ if $x>0,$ then for some natural $n,\; nx>y.$”

QUESTION 2: If I can do that then how  will do look $(2)$ in the contrapositive form "if not B, then not A"?

Regardless of whether a statement P is quantified, its contrapositive is logically equivalent to P itself. So, when taking the contrapositive of $(2),$ just modify the conditional portion, leaving the external quantifiers alone (otherwise the equivalence will be lost).

Addendum

Re: the contrapositive, is this correct? $$\forall x,y\in \mathbb{R}\Big( \forall n\in \mathbb{N}:nx\leq y \implies x\leq 0\Big).$$

Yes, but notice that the colon is no longer read as "such that", so leaving it there is potentially confusing? The colon (including in $(2\text c)$ above) is at best superfluous. So, slightly better: $$\forall x{,}y{\in} \mathbb{R}\;\Big( \forall n{\in} \mathbb{N}\;nx\leq y \implies x\leq 0\Big).$$ Also, do note that this is NOT equivalent to $$\forall x{,}y{\in} \mathbb{R}\;\forall n{\in} \mathbb{N}\;\Big(nx\leq y \implies x\leq 0\Big).$$
A: Note that $\forall x,y\in\mathbb R$ is just stating the domain of the proposition and can be expressed as:

Given real numbers $x$ and $y$

Now to the actual inference:

if $x>0$, then there exists $n\in\mathbb N$ such that $nx>y$

This part has the form:
$$
A\implies B
$$
and the contrapositive is:
$$
\neg B\implies \neg A
$$
which is:

if $\forall n\in\mathbb N$ we have $nx\leq y$, then $x\leq 0$

