Theorem redivclzi

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

	Ref	Expression
Hypotheses	redivcl.1	|- A e. RR
	redivcl.2	|- B e. RR
Assertion	redivclzi	|- ( B =/= 0 -> ( A / B ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		redivcl.1	|- A e. RR
2		redivcl.2	|- B e. RR
3		redivcl	|- ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A / B ) e. RR )
4	1 2 3	mp3an12	|- ( B =/= 0 -> ( A / B ) e. RR )