ltrec1

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

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

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

Metamath Proof Explorer