Theorem nnmtmip

Description: "Minus times minus is plus, The reason for this we need not discuss." (W. H. Auden, as quoted in M. Guillen "Bridges to Infinity", p. 64, see also Metamath Book, section 1.1.1, p. 5) This statement, formalized to "The product of two negative integers is a positive integer", is proved by the following theorem, therefore it actually need not be discussed anymore. "The reason for this" 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 nncn , and ( A x. B ) e. NN because of nnmulcl . This also holds for positive reals, see rpmtmip . Note that the opposites -u A and -u B of the positive integers A and B are negative integers. (Contributed by AV, 23-Dec-2022)

	Ref	Expression
Assertion	nnmtmip	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( - 𝐴 · - 𝐵 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		nncn	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℂ )
2		nncn	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
3		mul2neg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( - 𝐴 · - 𝐵 ) = ( 𝐴 · 𝐵 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( - 𝐴 · - 𝐵 ) = ( 𝐴 · 𝐵 ) )
5		nnmulcl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) ∈ ℕ )
6	4 5	eqeltrd	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( - 𝐴 · - 𝐵 ) ∈ ℕ )