lerec2

Description: Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005)

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

Step	Hyp	Ref	Expression
1		gt0ne0	$⊢ (B \in ℝ \land 0 < B) \to B \neq 0$
2		rereccl	$⊢ (B \in ℝ \land B \neq 0) \to \frac{1}{B} \in ℝ$
3	1 2	syldan	$⊢ (B \in ℝ \land 0 < B) \to \frac{1}{B} \in ℝ$
4		recgt0	$⊢ (B \in ℝ \land 0 < B) \to 0 < \frac{1}{B}$
5	3 4	jca	$⊢ (B \in ℝ \land 0 < B) \to (\frac{1}{B} \in ℝ \land 0 < \frac{1}{B})$
6		lerec	$⊢ ((A \in ℝ \land 0 < A) \land (\frac{1}{B} \in ℝ \land 0 < \frac{1}{B})) \to (A \leq \frac{1}{B} \leftrightarrow \frac{1}{\frac{1}{B}} \leq \frac{1}{A})$
7	5 6	sylan2	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (A \leq \frac{1}{B} \leftrightarrow \frac{1}{\frac{1}{B}} \leq \frac{1}{A})$
8		recn	$⊢ B \in ℝ \to B \in ℂ$
9		recrec	$⊢ (B \in ℂ \land B \neq 0) \to \frac{1}{\frac{1}{B}} = B$
10	8 1 9	syl2an2r	$⊢ (B \in ℝ \land 0 < B) \to \frac{1}{\frac{1}{B}} = B$
11	10	adantl	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to \frac{1}{\frac{1}{B}} = B$
12	11	breq1d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (\frac{1}{\frac{1}{B}} \leq \frac{1}{A} \leftrightarrow B \leq \frac{1}{A})$
13	7 12	bitrd	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (A \leq \frac{1}{B} \leftrightarrow B \leq \frac{1}{A})$

Metamath Proof Explorer