Theorem rerpdivcl

Description: Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008)

	Ref	Expression
Assertion	rerpdivcl	|- ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )

Proof

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