ltdiv23i

Description: Swap denominator with other side of 'less than'. (Contributed by NM, 26-Sep-1999)

	Ref	Expression
Hypotheses	ltplus1.1	$⊢ A \in ℝ$
	prodgt0.2	$⊢ B \in ℝ$
	ltmul1.3	$⊢ C \in ℝ$
Assertion	ltdiv23i	$⊢ (0 < B \land 0 < C) \to (\frac{A}{B} < C \leftrightarrow \frac{A}{C} < B)$

Step	Hyp	Ref	Expression
1		ltplus1.1	$⊢ A \in ℝ$
2		prodgt0.2	$⊢ B \in ℝ$
3		ltmul1.3	$⊢ C \in ℝ$
4		ltdiv23	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (\frac{A}{B} < C \leftrightarrow \frac{A}{C} < B)$
5	1 4	mp3an1	$⊢ ((B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (\frac{A}{B} < C \leftrightarrow \frac{A}{C} < B)$
6	2 5	mpanl1	$⊢ (0 < B \land (C \in ℝ \land 0 < C)) \to (\frac{A}{B} < C \leftrightarrow \frac{A}{C} < B)$
7	3 6	mpanr1	$⊢ (0 < B \land 0 < C) \to (\frac{A}{B} < C \leftrightarrow \frac{A}{C} < B)$

Metamath Proof Explorer