MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpaddcl Structured version   Visualization version   Unicode version

Theorem rpaddcl 11312
Description: Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
Assertion
Ref Expression
rpaddcl  |-  ( ( A  e.  RR+  /\  B  e.  RR+ )  ->  ( A  +  B )  e.  RR+ )

Proof of Theorem rpaddcl
StepHypRef Expression
1 rpre 11297 . . 3  |-  ( A  e.  RR+  ->  A  e.  RR )
2 rpre 11297 . . 3  |-  ( B  e.  RR+  ->  B  e.  RR )
3 readdcl 9608 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B
)  e.  RR )
41, 2, 3syl2an 484 . 2  |-  ( ( A  e.  RR+  /\  B  e.  RR+ )  ->  ( A  +  B )  e.  RR )
5 elrp 11293 . . 3  |-  ( A  e.  RR+  <->  ( A  e.  RR  /\  0  < 
A ) )
6 elrp 11293 . . 3  |-  ( B  e.  RR+  <->  ( B  e.  RR  /\  0  < 
B ) )
7 addgt0 10088 . . . 4  |-  ( ( ( A  e.  RR  /\  B  e.  RR )  /\  ( 0  < 
A  /\  0  <  B ) )  ->  0  <  ( A  +  B
) )
87an4s 839 . . 3  |-  ( ( ( A  e.  RR  /\  0  <  A )  /\  ( B  e.  RR  /\  0  < 
B ) )  -> 
0  <  ( A  +  B ) )
95, 6, 8syl2anb 486 . 2  |-  ( ( A  e.  RR+  /\  B  e.  RR+ )  ->  0  <  ( A  +  B
) )
10 elrp 11293 . 2  |-  ( ( A  +  B )  e.  RR+  <->  ( ( A  +  B )  e.  RR  /\  0  < 
( A  +  B
) ) )
114, 9, 10sylanbrc 675 1  |-  ( ( A  e.  RR+  /\  B  e.  RR+ )  ->  ( A  +  B )  e.  RR+ )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1890   class class class wbr 4373  (class class class)co 6275   RRcr 9524   0cc0 9525    + caddc 9528    < clt 9661   RR+crp 11291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-br 4374  df-opab 4433  df-mpt 4434  df-id 4726  df-po 4732  df-so 4733  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-ov 6278  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-rp 11292
This theorem is referenced by:  rpaddcld  11345  fsumrpcl  13813  logcnlem2  23599  logcnlem3  23600  logcnlem4  23601  loglesqrt  23709  ang180lem2  23750  cxp2limlem  23912  logdifbnd  23930  emcllem4  23935  emcllem5  23936  emcllem6  23937  selberg2lem  24399  chpdifbndlem2  24403  pntpbnd1a  24434  pntpbnd1  24435  pntpbnd2  24436  pntpbnd  24437  pntibndlem1  24438  pntibndlem2  24440  pntibnd  24442  pntlemd  24443  pntlemq  24450  pntlemr  24451  pntlemj  24452  pntlemp  24459  pntleml  24460  smcnlem  26344  hoidmvlelem3  38481
  Copyright terms: Public domain W3C validator