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

Metamath Proof Explorer

Theorem ltrecii

Description: The reciprocal of both sides of 'less than'. (Contributed by NM, 15-Sep-1999)

	Ref	Expression
Hypotheses	ltplus1.1	$⊢ A \in ℝ$
	prodgt0.2	$⊢ B \in ℝ$
	ltreci.3	$⊢ 0 < A$
	ltreci.4	$⊢ 0 < B$
Assertion	ltrecii	$⊢ A < B \leftrightarrow \frac{1}{B} < \frac{1}{A}$

Step	Hyp	Ref	Expression
1		ltplus1.1	$⊢ A \in ℝ$
2		prodgt0.2	$⊢ B \in ℝ$
3		ltreci.3	$⊢ 0 < A$
4		ltreci.4	$⊢ 0 < B$
5	1 2	ltreci	$⊢ (0 < A \land 0 < B) \to (A < B \leftrightarrow \frac{1}{B} < \frac{1}{A})$
6	3 4 5	mp2an	$⊢ A < B \leftrightarrow \frac{1}{B} < \frac{1}{A}$