Metamath Proof Explorer

Theorem rpaddcl

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

Ref Expression
Assertion rpaddcl 
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A + 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 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
4 1 2 3 syl2an 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A + B ) e. RR )
5 elrp 
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
6 elrp 
 |-  ( B e. RR+ <-> ( B e. RR /\ 0 < B ) )
7 addgt0 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < B ) ) -> 0 < ( A + B ) )
8 7 an4s 
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A + B ) )
9 5 6 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 4 9 10 sylanbrc 
 |-  ( ( A e. RR+ /\ B e. RR+ ) -> ( A + B ) e. RR+ )