Metamath Proof Explorer

Theorem rpdivcl

Description: Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007)

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

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( A e. RR+ -> A e. RR )
2 rprene0 
 |-  ( B e. RR+ -> ( B e. RR /\ B =/= 0 ) )
3 redivcl 
 |-  ( ( A e. RR /\ B e. RR /\ B =/= 0 ) -> ( A / B ) e. RR )
4 3 3expb 
 |-  ( ( A e. RR /\ ( B e. RR /\ B =/= 0 ) ) -> ( A / B ) e. RR )
5 1 2 4 syl2an 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A / B ) e. RR )
6 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
7 elrp 
 |-  ( B e. RR+ <-> ( B e. RR /\ 0 < B ) )
8 divgt0 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A / B ) )
9 6 7 8 syl2anb 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> 0 < ( A / B ) )
10 elrp 
 |-  ( ( A / B ) e. RR+ <-> ( ( A / B ) e. RR /\ 0 < ( A / B ) ) )
11 5 9 10 sylanbrc 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A / B ) e. RR+ )