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 + B + A B +

Proof

Step Hyp Ref Expression
1 rpre A + A
2 rpre B + B
3 remulcl A B A B
4 1 2 3 syl2an A + B + A B
5 elrp A + A 0 < A
6 elrp B + B 0 < B
7 mulgt0 A 0 < A B 0 < B 0 < A B
8 5 6 7 syl2anb A + B + 0 < A B
9 elrp A B + A B 0 < A B
10 4 8 9 sylanbrc A + B + A B +