mulgt1

Description: The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005) (Proof shortened by SN, 29-Jun-2025)

		Ref	Expression
	Assertion	mulgt1	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to 1 < A B$

Step	Hyp	Ref	Expression
1		1red	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to 1 \in ℝ$
2		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to A \in ℝ$
3		remulcl	$⊢ (A \in ℝ \land B \in ℝ) \to A B \in ℝ$
4	3	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to A B \in ℝ$
5		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to 1 < A$
6		simprr	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to 1 < B$
7		0red	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to 0 \in ℝ$
8		0lt1	$⊢ 0 < 1$
9	8	a1i	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to 0 < 1$
10	7 1 2 9 5	lttrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to 0 < A$
11		ltmulgt11	$⊢ (A \in ℝ \land B \in ℝ \land 0 < A) \to (1 < B \leftrightarrow A < A B)$
12	11	3expa	$⊢ ((A \in ℝ \land B \in ℝ) \land 0 < A) \to (1 < B \leftrightarrow A < A B)$
13	10 12	syldan	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to (1 < B \leftrightarrow A < A B)$
14	6 13	mpbid	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to A < A B$
15	1 2 4 5 14	lttrd	$⊢ ((A \in ℝ \land B \in ℝ) \land (1 < A \land 1 < B)) \to 1 < A B$

Metamath Proof Explorer