ge0div

Description: Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005)

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

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		lediv1	$⊢ (0 \in ℝ \land A \in ℝ \land (B \in ℝ \land 0 < B)) \to (0 \leq A \leftrightarrow \frac{0}{B} \leq \frac{A}{B})$
3	1 2	mp3an1	$⊢ (A \in ℝ \land (B \in ℝ \land 0 < B)) \to (0 \leq A \leftrightarrow \frac{0}{B} \leq \frac{A}{B})$
4	3	3impb	$⊢ (A \in ℝ \land B \in ℝ \land 0 < B) \to (0 \leq A \leftrightarrow \frac{0}{B} \leq \frac{A}{B})$
5		recn	$⊢ B \in ℝ \to B \in ℂ$
6		gt0ne0	$⊢ (B \in ℝ \land 0 < B) \to B \neq 0$
7		div0	$⊢ (B \in ℂ \land B \neq 0) \to \frac{0}{B} = 0$
8	5 6 7	syl2an2r	$⊢ (B \in ℝ \land 0 < B) \to \frac{0}{B} = 0$
9	8	breq1d	$⊢ (B \in ℝ \land 0 < B) \to (\frac{0}{B} \leq \frac{A}{B} \leftrightarrow 0 \leq \frac{A}{B})$
10	9	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land 0 < B) \to (\frac{0}{B} \leq \frac{A}{B} \leftrightarrow 0 \leq \frac{A}{B})$
11	4 10	bitrd	$⊢ (A \in ℝ \land B \in ℝ \land 0 < B) \to (0 \leq A \leftrightarrow 0 \leq \frac{A}{B})$

Metamath Proof Explorer