# Metamath Proof Explorer

## 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)={A}{B}$
4 1 2 3 syl2an ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left(-{A}\right)\left(-{B}\right)={A}{B}$
5 rpmulcl ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to {A}{B}\in {ℝ}^{+}$
6 4 5 eqeltrd ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to \left(-{A}\right)\left(-{B}\right)\in {ℝ}^{+}$