Metamath Proof Explorer

Theorem ltrec

Description: The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		1red	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 1 \in ℝ$
2		simprl	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to B \in ℝ$
3		simpll	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to A \in ℝ$
4		simplr	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < A$
5		ltmuldiv	$⊢ (1 \in ℝ \land B \in ℝ \land (A \in ℝ \land 0 < A)) \to (1 A < B \leftrightarrow 1 < \frac{B}{A})$
6	1 2 3 4 5	syl112anc	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (1 A < B \leftrightarrow 1 < \frac{B}{A})$
7	3	recnd	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to A \in ℂ$
8	7	mullidd	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 1 A = A$
9	8	breq1d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (1 A < B \leftrightarrow A < B)$
10	2	recnd	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to B \in ℂ$
11	4	gt0ne0d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to A \neq 0$
12	10 7 11	divrecd	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to \frac{B}{A} = B (\frac{1}{A})$
13	12	breq2d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (1 < \frac{B}{A} \leftrightarrow 1 < B (\frac{1}{A}))$
14	6 9 13	3bitr3d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (A < B \leftrightarrow 1 < B (\frac{1}{A}))$
15	3 11	rereccld	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to \frac{1}{A} \in ℝ$
16		simprr	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to 0 < B$
17		ltdivmul	$⊢ (1 \in ℝ \land \frac{1}{A} \in ℝ \land (B \in ℝ \land 0 < B)) \to (\frac{1}{B} < \frac{1}{A} \leftrightarrow 1 < B (\frac{1}{A}))$
18	1 15 2 16 17	syl112anc	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (\frac{1}{B} < \frac{1}{A} \leftrightarrow 1 < B (\frac{1}{A}))$
19	14 18	bitr4d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (A < B \leftrightarrow \frac{1}{B} < \frac{1}{A})$