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 ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( - ๐ด ยท - ๐ต ) โˆˆ โ„+ )

Proof

Step Hyp Ref Expression
1 rpcn โŠข ( ๐ด โˆˆ โ„+ โ†’ ๐ด โˆˆ โ„‚ )
2 rpcn โŠข ( ๐ต โˆˆ โ„+ โ†’ ๐ต โˆˆ โ„‚ )
3 mul2neg โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( - ๐ด ยท - ๐ต ) = ( ๐ด ยท ๐ต ) )
4 1 2 3 syl2an โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( - ๐ด ยท - ๐ต ) = ( ๐ด ยท ๐ต ) )
5 rpmulcl โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( ๐ด ยท ๐ต ) โˆˆ โ„+ )
6 4 5 eqeltrd โŠข ( ( ๐ด โˆˆ โ„+ โˆง ๐ต โˆˆ โ„+ ) โ†’ ( - ๐ด ยท - ๐ต ) โˆˆ โ„+ )