Theorem rpmtmip

Description: "Minus times minus is plus", see also nnmtmip , holds for positive reals, too (formalized to "The product of two negative reals is a positive real"). "The reason for this" in this case is that ( -u A x. -u B ) = ( A x. B ) for all complex numbers A and B because of mul2neg , A and B are complex numbers because of rpcn , and ( A x. B ) e. RR+ because of rpmulcl . Note that the opposites -u A and -u B of the positive reals A and B are negative reals. (Contributed by AV, 23-Dec-2022)

	Ref	Expression
Assertion	rpmtmip	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(-A\right)\left(-B\right)\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
2		rpcn	$$⊢B\in {ℝ}^{+}\to B\in ℂ$$
3		mul2neg	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to \left(-A\right)\left(-B\right)=AB$$
4	1 2 3	syl2an	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(-A\right)\left(-B\right)=AB$$
5		rpmulcl	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to AB\in {ℝ}^{+}$$
6	4 5	eqeltrd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \left(-A\right)\left(-B\right)\in {ℝ}^{+}$$