Strict inequality for floating point multiplication

Question

Suppose a, x, and y are positive IEEE floating point numbers with x < y. Prove that a×x < a×y where × denotes floating-point multiplication rounding to nearest.

Naively, you might suppose that for some a and for x close to y, you would get a×x = a×y. It turns out that this can't happen (as long as denormalized numbers, infinities, and NaNs are excluded).

I'm interested in an elegant proof and, if possible, a book or paper where this is given.

TAKE 2: As the reply by Pascal Cuoq shows, the statement above is false. How about the restricted version with y = 1? Here is the statement to be proved:

Suppose a and x are positive IEEE floating point numbers with x < 1. Prove that a×x < a where × denotes floating-point multiplication rounding to nearest.

Answer 1

To put a formal proof to your revised question (with slightly altered language):

Suppose a and x are positive IEEE floating point numbers with x < 1. Prove that [ax] < a where [] denotes default floating-point rounding.

WLOG, let a be in [1, 2). The statement is trivially true if a is 1, so we actually only need to consider a in (1,2). x < 1 implies that x <= 1 - u/2, where u = ulp(1) = ulp(a). We have:

ax <= a - au/2

We also have a > 1, so au/2 > u/2, so:

ax <= a - au/2 < a - u/2

Because ax is more than half an ulp below a, [ax] < a.