Theorem redivcli

Description: Closure law for division of reals. (Contributed by NM, 9-May-1999)

	Ref	Expression
Hypotheses	redivcl.1	$$⊢A\in ℝ$$
	redivcl.2	$$⊢B\in ℝ$$
	redivcl.3	$$⊢B\ne 0$$
Assertion	redivcli	$$⊢\frac{A}{B}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		redivcl.1	$$⊢A\in ℝ$$
2		redivcl.2	$$⊢B\in ℝ$$
3		redivcl.3	$$⊢B\ne 0$$
4	1 2	redivclzi	$$⊢B\ne 0\to \frac{A}{B}\in ℝ$$
5	3 4	ax-mp	$$⊢\frac{A}{B}\in ℝ$$