Metamath Proof Explorer

Theorem axmulgt0

Description: The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. (This restates ax-pre-mulgt0 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005)

		Ref	Expression
	Assertion	axmulgt0	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 < A \land 0 < B) \to 0 < A B)$

Proof

Step	Hyp	Ref	Expression
1		ax-pre-mulgt0	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 <_{ℝ} A \land 0 <_{ℝ} B) \to 0 <_{ℝ} A B)$
2		0re	$⊢ 0 \in ℝ$
3		ltxrlt	$⊢ (0 \in ℝ \land A \in ℝ) \to (0 < A \leftrightarrow 0 <_{ℝ} A)$
4	2 3	mpan	$⊢ A \in ℝ \to (0 < A \leftrightarrow 0 <_{ℝ} A)$
5		ltxrlt	$⊢ (0 \in ℝ \land B \in ℝ) \to (0 < B \leftrightarrow 0 <_{ℝ} B)$
6	2 5	mpan	$⊢ B \in ℝ \to (0 < B \leftrightarrow 0 <_{ℝ} B)$
7	4 6	bi2anan9	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 < A \land 0 < B) \leftrightarrow (0 <_{ℝ} A \land 0 <_{ℝ} B))$
8		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
9		ltxrlt	$⊢ (0 \in ℝ \land A B \in ℝ) \to (0 < A B \leftrightarrow 0 <_{ℝ} A B)$
10	2 8 9	sylancr	$⊢ (A \in ℝ \land B \in ℝ) \to (0 < A B \leftrightarrow 0 <_{ℝ} A B)$
11	1 7 10	3imtr4d	$⊢ (A \in ℝ \land B \in ℝ) \to ((0 < A \land 0 < B) \to 0 < A B)$