Metamath Proof Explorer

Theorem ltdiv1

Description: Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to A \in ℝ$
2		simp2	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to B \in ℝ$
3		simp3l	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \in ℝ$
4		simp3r	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to 0 < C$
5	4	gt0ne0d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \neq 0$
6	3 5	rereccld	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{1}{C} \in ℝ$
7		recgt0	$⊢ (C \in ℝ \land 0 < C) \to 0 < \frac{1}{C}$
8	7	3ad2ant3	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to 0 < \frac{1}{C}$
9		ltmul1	$⊢ (A \in ℝ \land B \in ℝ \land (\frac{1}{C} \in ℝ \land 0 < \frac{1}{C})) \to (A < B \leftrightarrow A (\frac{1}{C}) < B (\frac{1}{C}))$
10	1 2 6 8 9	syl112anc	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < B \leftrightarrow A (\frac{1}{C}) < B (\frac{1}{C}))$
11	1	recnd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to A \in ℂ$
12	3	recnd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to C \in ℂ$
13	11 12 5	divrecd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{A}{C} = A (\frac{1}{C})$
14	2	recnd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to B \in ℂ$
15	14 12 5	divrecd	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to \frac{B}{C} = B (\frac{1}{C})$
16	13 15	breq12d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{A}{C} < \frac{B}{C} \leftrightarrow A (\frac{1}{C}) < B (\frac{1}{C}))$
17	10 16	bitr4d	$⊢ (A \in ℝ \land B \in ℝ \land (C \in ℝ \land 0 < C)) \to (A < B \leftrightarrow \frac{A}{C} < \frac{B}{C})$