Metamath Proof Explorer

Theorem rpmulcl

Description: Closure law for multiplication of positive reals. Part of Axiom 7 of Apostol p. 20. (Contributed by NM, 27-Oct-2007)

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

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( A e. RR+ -> A e. RR )
2 rpre 
 |-  ( B e. RR+ -> B e. RR )
3 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4 1 2 3 syl2an 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A x. B ) e. RR )
5 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
6 elrp 
 |-  ( B e. RR+ <-> ( B e. RR /\ 0 < B ) )
7 mulgt0 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A x. B ) )
8 5 6 7 syl2anb 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> 0 < ( A x. B ) )
9 elrp 
 |-  ( ( A x. B ) e. RR+ <-> ( ( A x. B ) e. RR /\ 0 < ( A x. B ) ) )
10 4 8 9 sylanbrc 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A x. B ) e. RR+ )