Metamath Proof Explorer


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 )