This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ (A \in ℝ^{+} \land B \in ℝ^{+}) \to (- A) (- B) \in ℝ^{+}$

Proof

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