Theorem redivclzi

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

	Ref	Expression
Hypotheses	redivcl.1	⊢ 𝐴 ∈ ℝ
	redivcl.2	⊢ 𝐵 ∈ ℝ
Assertion	redivclzi	⊢ ( 𝐵 ≠ 0 → ( 𝐴 / 𝐵 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		redivcl.1	⊢ 𝐴 ∈ ℝ
2		redivcl.2	⊢ 𝐵 ∈ ℝ
3		redivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
4	1 2 3	mp3an12	⊢ ( 𝐵 ≠ 0 → ( 𝐴 / 𝐵 ) ∈ ℝ )