This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ge0divd

Description: Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	rpgecld.1	$⊢ φ \to A \in ℝ$
	rpgecld.2	$⊢ φ \to B \in ℝ^{+}$
Assertion	ge0divd	$⊢ φ \to (0 \leq A \leftrightarrow 0 \leq \frac{A}{B})$

Step	Hyp	Ref	Expression
1		rpgecld.1	$⊢ φ \to A \in ℝ$
2		rpgecld.2	$⊢ φ \to B \in ℝ^{+}$
3	2	rpred	$⊢ φ \to B \in ℝ$
4	2	rpgt0d	$⊢ φ \to 0 < B$
5		ge0div	$⊢ (A \in ℝ \land B \in ℝ \land 0 < B) \to (0 \leq A \leftrightarrow 0 \leq \frac{A}{B})$
6	1 3 4 5	syl3anc	$⊢ φ \to (0 \leq A \leftrightarrow 0 \leq \frac{A}{B})$