Metamath Proof Explorer

Theorem lerec

Description: The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 3-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	lerec	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (A \leq B \leftrightarrow \frac{1}{B} \leq \frac{1}{A})$

Proof

Step	Hyp	Ref	Expression
1		ltrec	$⊢ ((B \in ℝ \land 0 < B) \land (A \in ℝ \land 0 < A)) \to (B < A \leftrightarrow \frac{1}{A} < \frac{1}{B})$
2	1	ancoms	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (B < A \leftrightarrow \frac{1}{A} < \frac{1}{B})$
3	2	notbid	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (\neg B < A \leftrightarrow \neg \frac{1}{A} < \frac{1}{B})$
4		simpll	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to A \in ℝ$
5		simprl	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to B \in ℝ$
6	4 5	lenltd	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (A \leq B \leftrightarrow \neg B < A)$
7		simprr	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < B$
8	7	gt0ne0d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to B \neq 0$
9	5 8	rereccld	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to \frac{1}{B} \in ℝ$
10		simplr	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < A$
11	10	gt0ne0d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to A \neq 0$
12	4 11	rereccld	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to \frac{1}{A} \in ℝ$
13	9 12	lenltd	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (\frac{1}{B} \leq \frac{1}{A} \leftrightarrow \neg \frac{1}{A} < \frac{1}{B})$
14	3 6 13	3bitr4d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (A \leq B \leftrightarrow \frac{1}{B} \leq \frac{1}{A})$