lediv2

Description: Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006)

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

Proof

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	3	3ad2ant2	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to \frac{1}{B} \in ℝ$
5		gt0ne0	$⊢ (A \in ℝ \land 0 < A) \to A \neq 0$
6		rereccl	$⊢ (A \in ℝ \land A \neq 0) \to \frac{1}{A} \in ℝ$
7	5 6	syldan	$⊢ (A \in ℝ \land 0 < A) \to \frac{1}{A} \in ℝ$
8	7	3ad2ant1	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to \frac{1}{A} \in ℝ$
9		simp3l	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to C \in ℝ$
10		simp3r	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to 0 < C$
11		lemul2	$⊢ (\frac{1}{B} \in ℝ \land \frac{1}{A} \in ℝ \land (C \in ℝ \land 0 < C)) \to (\frac{1}{B} \leq \frac{1}{A} \leftrightarrow C (\frac{1}{B}) \leq C (\frac{1}{A}))$
12	4 8 9 10 11	syl112anc	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (\frac{1}{B} \leq \frac{1}{A} \leftrightarrow C (\frac{1}{B}) \leq C (\frac{1}{A}))$
13		lerec	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (A \leq B \leftrightarrow \frac{1}{B} \leq \frac{1}{A})$
14	13	3adant3	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (A \leq B \leftrightarrow \frac{1}{B} \leq \frac{1}{A})$
15		recn	$⊢ C \in ℝ \to C \in ℂ$
16		recn	$⊢ B \in ℝ \to B \in ℂ$
17	16	adantr	$⊢ (B \in ℝ \land 0 < B) \to B \in ℂ$
18	17 1	jca	$⊢ (B \in ℝ \land 0 < B) \to (B \in ℂ \land B \neq 0)$
19		divrec	$⊢ (C \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{C}{B} = C (\frac{1}{B})$
20	19	3expb	$⊢ (C \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{C}{B} = C (\frac{1}{B})$
21	15 18 20	syl2an	$⊢ (C \in ℝ \land (B \in ℝ \land 0 < B)) \to \frac{C}{B} = C (\frac{1}{B})$
22	21	3adant2	$⊢ (C \in ℝ \land (A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to \frac{C}{B} = C (\frac{1}{B})$
23		recn	$⊢ A \in ℝ \to A \in ℂ$
24	23	adantr	$⊢ (A \in ℝ \land 0 < A) \to A \in ℂ$
25	24 5	jca	$⊢ (A \in ℝ \land 0 < A) \to (A \in ℂ \land A \neq 0)$
26		divrec	$⊢ (C \in ℂ \land A \in ℂ \land A \neq 0) \to \frac{C}{A} = C (\frac{1}{A})$
27	26	3expb	$⊢ (C \in ℂ \land (A \in ℂ \land A \neq 0)) \to \frac{C}{A} = C (\frac{1}{A})$
28	15 25 27	syl2an	$⊢ (C \in ℝ \land (A \in ℝ \land 0 < A)) \to \frac{C}{A} = C (\frac{1}{A})$
29	28	3adant3	$⊢ (C \in ℝ \land (A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to \frac{C}{A} = C (\frac{1}{A})$
30	22 29	breq12d	$⊢ (C \in ℝ \land (A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B)) \to (\frac{C}{B} \leq \frac{C}{A} \leftrightarrow C (\frac{1}{B}) \leq C (\frac{1}{A}))$
31	30	3coml	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B) \land C \in ℝ) \to (\frac{C}{B} \leq \frac{C}{A} \leftrightarrow C (\frac{1}{B}) \leq C (\frac{1}{A}))$
32	31	3adant3r	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (\frac{C}{B} \leq \frac{C}{A} \leftrightarrow C (\frac{1}{B}) \leq C (\frac{1}{A}))$
33	12 14 32	3bitr4d	$⊢ ((A \in ℝ \land 0 < A) \land (B \in ℝ \land 0 < B) \land (C \in ℝ \land 0 < C)) \to (A \leq B \leftrightarrow \frac{C}{B} \leq \frac{C}{A})$

Metamath Proof Explorer

Theorem lediv2

Proof