Formal proof of: $x>y$ and $b>0$ implies $bx>by$?

Question

Property: If $x,y,b \in \mathbb{R}$ and $x>y$ and $b>0$, then $bx>by$.

What is a formal (low-level) proof of this result? Or is this property taken as axiomatic?

The motivation for this question comes from an earlier question (If $a > 1$ then $a^2 > a$) where the accepted answer (in my opinion) amounted to saying it's a special case of the above result.

---

With Asaf Karagila's suggestion, here's a first attempt at achieving a low-level proof:

We will use the ring axioms, and the following ordered ring axioms:

Axiom 1: If $a,b,c \in \mathbb{R}$ and $a \leq b$, then $a+c \leq b+c$.

Axiom 2: If $a,b \in \mathbb{R}$, $0 \leq a$ and $0 \leq b$, then $0 \leq ab$.

We need the property that $\mathbb{R}$ has no zero divisors; we'll take this as an axiom:

Axiom 3: If $a,b \in \mathbb{R}$ and $ab=0$, then $a=0$ or $b=0$.

And we take the definition of $>$ as:

Definition 1: If $a,b \in \mathbb{R}$, $b \leq a$ and $a \neq b$, then $a>b$.

We will also use the following group lemmas (each of which admit proofs using only the group axioms for $(\mathbb{R},+)$):

Lemma 1: If $a,b,c \in \mathbb{R}$ and $a \neq b$, then $a+c \neq b+c$.

Lemma 2: If $a,b \in \mathbb{R}$, then $a(-b)=-(ab)$.

Then for $x,y \in \mathbb{R}$, we have $\small \begin{align*} x>y & \iff y \leq x \text{ and } x \neq y & \text{by Definition 1} \\ & \iff y+(-y) \leq x+(-y) \text{ and } x+(-y) \neq y+(-y) & \text{by Axiom 1; Lemma 1} \\ & \iff 0 \leq x+(-y) \text{ and } x+(-y) \neq 0 \qquad (*) & \text{additive inverse } \\ & \iff x+(-y)>0 \qquad\qquad\qquad\qquad (**) & \text{by Definition 1 } \\ \end{align*} $

Hence, for $x,y,b \in \mathbb{R}$, we have $\small \begin{align*} x>y \text{ and } b>0 & \implies 0 \leq x+(-y) \text{ and } x+(-y) \neq 0 \text{ and } b>0 & \text{by } (*) \\ & \implies 0 \leq x+(-y) \text{ and } x+(-y) \neq 0 \text{ and } 0 \leq b \text{ and } b \neq 0 & \text{by Definition 1} \\ & \implies 0 \leq b(x+(-y)) \text{ and } x+(-y) \neq 0 \text{ and } b \neq 0 & \text{by Axiom 2} \\ & \implies 0 \leq b(x+(-y)) \text{ and } b(x+(-y)) \neq 0 & \text{by Axiom 3} \\ & \implies b(x+(-y))>0 & \text{by Definition 1} \\ & \implies bx+b(-y)>0 & \text{left distrib.} \\ & \implies bx+(-(by))>0 & \text{by Lemma 2} \\ & \implies bx>by & \text{by } (**) \end{align*} $ proving the claim.

Answer 1

From $x>y$ you know that $x-y>0$, since $b>0$ you will have $b(x-y)>0$ (the product of two positive numbers is positive). So $bx>by$. I'm not sure if it is what you want.

Answer 2

The basic fact is that product of two positive numbers is positive and $x>y$ is shorthand to $x-y>0$.

Hence $$ (x>y), ~~\text{and}~~b>0 \Rightarrow b (x-y) > 0 \Rightarrow bx -by >0 \Rightarrow bx > by$$

Answer 3

this is a very interesting question! When it comes to $\mathbb R$, there is basically two options:

1) Define it by an axiom: $\mathbb R$ is the unique (up to isomorphism) of Archimedian totally ordered field satisfying the least upper bound property. With this axiom, the property you want to prove is part of the definition of totally ordered set.

2) Define $\mathbb N$ by the Peano axioms and then build $\mathbb Z$, $\mathbb Q$ and $\mathbb R$ by the usual constructions. So, you have to prove the property for $\mathbb N$ (should work by induction) and then extend it at every step of the construction.