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

Theorem ltaddrp 11015
Description: Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.)
Assertion
Ref Expression
ltaddrp  |-  ( ( A  e.  RR  /\  B  e.  RR+ )  ->  A  <  ( A  +  B ) )

Proof of Theorem ltaddrp
StepHypRef Expression
1 elrp 10985 . 2  |-  ( B  e.  RR+  <->  ( B  e.  RR  /\  0  < 
B ) )
2 ltaddpos 9821 . . . . 5  |-  ( ( B  e.  RR  /\  A  e.  RR )  ->  ( 0  <  B  <->  A  <  ( A  +  B ) ) )
32biimpd 207 . . . 4  |-  ( ( B  e.  RR  /\  A  e.  RR )  ->  ( 0  <  B  ->  A  <  ( A  +  B ) ) )
43expcom 435 . . 3  |-  ( A  e.  RR  ->  ( B  e.  RR  ->  ( 0  <  B  ->  A  <  ( A  +  B ) ) ) )
54imp32 433 . 2  |-  ( ( A  e.  RR  /\  ( B  e.  RR  /\  0  <  B ) )  ->  A  <  ( A  +  B ) )
61, 5sylan2b 472 1  |-  ( ( A  e.  RR  /\  B  e.  RR+ )  ->  A  <  ( A  +  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1757   class class class wbr 4284  (class class class)co 6084   RRcr 9273   0cc0 9274    + caddc 9277    < clt 9410   RR+crp 10983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418  ax-sep 4405  ax-nul 4413  ax-pow 4462  ax-pr 4523  ax-un 6365  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3281  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3630  df-if 3784  df-pw 3854  df-sn 3870  df-pr 3872  df-op 3876  df-uni 4084  df-br 4285  df-opab 4343  df-mpt 4344  df-id 4627  df-po 4632  df-so 4633  df-xp 4837  df-rel 4838  df-cnv 4839  df-co 4840  df-dm 4841  df-rn 4842  df-res 4843  df-ima 4844  df-iota 5373  df-fun 5412  df-fn 5413  df-f 5414  df-f1 5415  df-fo 5416  df-f1o 5417  df-fv 5418  df-ov 6087  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-ltxr 9415  df-rp 10984
This theorem is referenced by:  ltaddrpd  11048  efgt1  13387  efgsfo  16220  efgredlemd  16225  efgredlem  16228  iccntr  20244  reconnlem2  20250  opnreen  20254  minveclem3b  20761  logimul  21952  emcllem2  22279  emcllem4  22281  emcllem6  22283  perfectlem2  22458  bclbnd  22508  pntibndlem1  22727  pntlemd  22732  pntlemc  22733  pntlemr  22740  pntlemp  22748  smcnlem  23919  ballotlem2  26723  stoweidlem59  29704
  Copyright terms: Public domain W3C validator