My proof about $\text{sup}(AB) = \text{inf}(A) \text{inf}(B)$ for real negative nonempty sets $A,B$ Given two nonempty bounded below sets $A,B\subset \mathbb R$ of negative numbers.
Define $AB=\left\{ab:a \in A,b \in B\right\}$
I concluded that $$\text{sup}(AB) =  \text{inf}(A)  \text{inf}(B)$$

$$ab \le \text{inf}(A)b \le\text{inf}(A)\text{inf}(B)$$
So $AB$ is a nonempty subset of $\mathbb R$ bounded above and so its supremum does exist, by the minimality of supremum :
$$  \text{sup}(AB) \le \text{inf}(A)\text{inf}(B)\tag{I}$$
On the other hand:
$$\text{sup}(AB)\ge ab \iff \frac{1}{a}\text{sup}(AB)\le b$$
Which is true for all $a \in A,b \in B$,from the definition of infimum:
$$\frac{1}{a}\text{sup}(AB)\le \text{inf}(B) \iff \frac{1}{\text{inf}(B)}\text{sup}(AB)\le a$$
Again from the definition of infimum:
$$\frac{1}{\text{inf}(B)}\text{sup}(AB)\le \text{inf}(A) \iff \text{sup}(AB) \ge  \text{inf}(A)  \text{inf}(B)\tag{II}$$
From $\text{(I)}$ and $\text{(II)}$ the result follows.

The result looks like the relation $$\text{sup}(AB) =  \text{sup}(A)  \text{sup}(B)$$ for two positive nonempty real subsets $A,B$.
Can someone check the validity of my proof?
 A: Your proof is fine - but, I think that this is the sort of problem where a reader will be more easily convinced of the correctness of the proof if you reduce the problem to one involving positive numbers first. It's a bit jarring if the first statement in the proof is
$$ab\leq \inf(A)b\leq \inf(A)\inf(B)$$
because then the reader needs to explicitly think that one must have $\inf(A)\leq a$ but that this get reversed when we multiply by a negative $b$. This doesn't affect the correctness of your proof, of course, but multiplying by negative numbers everywhere makes things much more difficult for the reader, since one has to worry about the directions of inequalities getting reversed.
Instead, I propose you would most cleanly start this proof by presenting a lemma:

Lemma: If $A$ and $B$ are sets of positive real numbers, then $\sup(AB)=\sup(A)\sup(B).$

Then, prior to proving this lemma, you can mention its application to your given problem:

This lemma implies the given problem since, if $A$ and $B$ were sets of negative real numbers, then $(-A)$ and $(-B)$ would be sets of positive real numbers. Assuming the lemma, this yields $\sup(-A)\sup(-B)=\sup((-A)(-B))$. However, note that $(-A)(-B)=AB$ and that $\sup(-A)=-\inf(A)$, so we can derive $\inf(A)\inf(B)=\sup(AB)$ for sets of negative numbers from the lemma.

You might consider breaking out the fact that $-\inf(A)=\sup(-A)$ as a lemma of its own if this is not something you want to use without proof. Doing it this way breaks out all the difficulties of negative numbers into one small section and leaves us with only positive numbers (where multiplication by a constant is an increasing function) - and it nicely takes advantage of the idea that the negative numbers sort of look like the positive numbers, just reversed.
With this prelude out of the way, let's take a look at what you've written, and how it might be better formatted and fit into such a proof. First of all, your first equation is correct, but it should be given context. Your ultimate claim is now that $\sup(A)\sup(B)$ is the least upper bound for $\sup(AB)$, so it's reasonable to have two steps: first, that it is an upper bound, and second, that it is the least upper bound.

Lemma: $\sup(A)\sup(B)$ is an upper bound for $AB$.
Proof: Let $ab\in AB$ where $a\in A$ and $b\in B$. By definition $a\leq \sup(A)$ and $b\leq \sup(B)$. As multiplication by a constant preserves the order, we can derive that $$ab\leq \sup(A)b\leq \sup(A)\sup(B).$$

This is essentially what you wrote, except that it is explicit about both why we care about the equation and how the variables are quantified. You don't have to write in the rigid lemma and proof format, but it is important to let the reader know why an equation is desirable.
The other part of your proof shows that this is the least upper bound. You might notice that you don't actually need to assume $\sup(AB)$ exists - everything you do in that section is true of any upper bound, and ultimately, that's what you want to do. You might continue your proof as:

Lemma: $\sup(A)\sup(B)$ is less than or equal to any other upper bound $L$ for $AB$.
Proof: Suppose that $L$ is an upper bound for $AB$. Then, for every $a\in A$ and $b\in B$ we have
$$L\geq ab$$
which implies
$$\frac{L}a \geq b.$$
This means that $\frac{L}a$ is an upper bound for $B$ and therefore, by the definition of the supremum, we must have
$$\frac{L}a \geq \sup(B).$$
Rearranging further gives
$$\frac{L}{\sup(B)}\geq a$$
where we may then invoke that $\sup(A)$ is the least upper bound for $A$ to receive that
$$\frac{L}{\sup(B)}\geq \sup(A)$$
$$L\geq \sup(A)\sup(B).$$

Then, you can simply conclude:

These two lemmas together imply that $\sup(A)\sup(B)$ is the least upper bound of $AB$, as desired.

Note that I have not touched your algebra at all, except to convert things to positive numbers - what you wrote is perfectly solid, but could be improved by telling the reader why some algebra is important before just jumping to a result and by moving to an easier context for the algebra.
Also observe that, in splitting the proof up according to our requirements, we also eliminated any usage of the completeness of the real numbers - indeed, I might note that your proof method is quite a good one, as it avoids using epsilons or convergence and sticks close to the algebraic and order theoretic definitions.

A slight aside on the second half of the proof: I often like to think about the step from
$$L\geq ab$$
to
$$L\geq \sup(A)b$$
as a single operation of "taking the supremum of both sides over $A$" - since then the whole second half becomes that we take the supremum over $a\in A$ then over $b\in B$ - and can generalize this slightly to allow non-negative reals instead of just positive reals. You need some additional lemma to do this formally - something like:

If $f$ is a continuous non-decreasing function then $\sup(f[X])=f(\sup(X))$

Although, in this case, it suffices to just prove this where $f(x)=\alpha x$ for $\alpha\geq 0$. I suppose, most conservatively, you might just prove an extra lemma:

If $c$ is a positive real, then $\sup(cS)=c\sup(S)$

and applying this twice in the second half to see that $L\geq ab$ implies $L\geq \sup(A)b$ and $L\geq \sup(A)\sup(B)$ in two steps.
Either way, this breaks out some of the algebra into something a bit more conceptual and the idea of turning an inequality quantified over a set into an inequality of extrema has often proved to be useful when I've wanted to do these harder problems in this sort of style.

It's definitely overkill for this problem, but if you're really so inclined, you can also do this sort of manipulation in a more set theoretic way by additionally noting that if $\mathcal F$ is a set of subsets of $\mathbb R$ and $\bigcup \mathcal F$ is the union of all elements of $\mathcal F$, then $$\sup\left(\bigcup \mathcal F\right) = \sup\{\sup(S) : S\in \mathcal F\}.$$
Then you just observe that $AB=\bigcup_{b\in B}bA$ so \begin{align*}\sup(AB)&=\sup\{\sup(bA) : b\in B\}\\&= \sup\{b\sup(A) : b\in B\}\\&=\sup(\sup(A)B)\\&=\sup(A)\sup(B).\end{align*}
where you use the given lemma for the first step, then use the prior lemma that $\sup(cS)=c\sup(S)$ several times - although a lot of the algebra you did ends up being packed into the proof of these lemmas so this ends up being essentially the same argument you put forth, except that it works using sets instead of equations with quantifiers. Sometimes this is a useful way to think about things, although I typically think that the algebraic methods you're using are clearer.
A: Yeah, it looks alright, in terms of logic, but can be improved in terms of style and exposition. Here are some (opinionated) remarks:

*

*The proof can be much, much shorter. If you have a clear audience in mind, then you'll have a clear(er) idea of what details to keep and not.

*Indeed, a short proof leaves less doubt as to its validity!

*You don't need completeness axiom here, just show the RHS satisfies the two conditions to be a least upper bound! (I.e., the part before equation (I) doesn't add anything.)

*It is much better to tell us where $a$ and $b$ live before, rather than after the inequalities they apply to. In fact, you can even fix them at the beginning!

An alternative proof.
I also think with sup/inf questions, choosing the right tool makes things much more straightforward  (I like sequences myself, but the original definition), if you have the lemmas to hand
You showed $s:= \inf(A)\inf(B)$ is an upper bound for $AB$, that was quite nice (although it would be nice if you made it clear exactly where you used that $b$ negative and $a$ negative!). It too may be shortened, because content wise there isn't much to say!
From there on, you just need to show it is a least upper bound (i.e. supremum) — no need to revoke the completeness axiom.
Way using sequences
I absolutely love this result. If you've seen it before, you can use it, in combination with taking limits in inequalities.

For a non-empty set $C \subset \mathbb R$, there always exists a sequence $(x_n)_{n=1}^∞\subset C$ such that $$(x_n)\to \inf (C).$$
(This applies even if $\inf(C) = -∞$, and for $\sup$ in place of $\inf$)

You may well have seen it in an equivalent form, like, for $C \subset \mathbb R$ if the infimum $\inf(C)$ "exists"/is finite; then for all $\epsilon>0$, there is an element of $C$ inside the interval $$(\inf(C) - \epsilon, \inf(C)].$$
In any case, we can prove the following claim:
Claim: For all $U$ upper bounds on $AB$, $$U \geq s.$$
Proof: Let $U$ be an upper bound on $AB$, and let

*

*$(a_n)_{n=1}^∞$ be a sequence of elements in $A$ which converges to $\inf(A).$

*$(b_n)_{n=1}^∞$ be a sequence of elements in $B$ which converges to $\inf(B).$
Then

*

*$(a_nb_n)_{n=1}^∞$ converges to $\inf(A)\inf(B) = s$, by the product rule; and

*for all $n \in \mathbb N$, $a_nb_n \in AB$,$\ $ so $$U \geq a_nb_n.$$
Combining these two:
$$a_nb_n \leq U \implies \lim_{n\to ∞}(a_nb_n) \leq U,\qquad\text{i.e. }s \leq U.\text{ QED}$$
Everything follows from this: not only is $s$ is not only an upper bound, but the least upper bound, i.e. supremum.)
