Theorem ltaddrpd 13035

Description: Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)

Hypotheses

Ref	Expression
rpgecld.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
rpgecld.2	⊢ (𝜑 → 𝐵 ∈ ℝ+)

Assertion

Ref	Expression
ltaddrpd	⊢ (𝜑 → 𝐴 < (𝐴 + 𝐵))

Proof of Theorem ltaddrpd

Step	Hyp	Ref	Expression
1		rpgecld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		rpgecld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ+)
3		ltaddrp 12997	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵))
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → 𝐴 < (𝐴 + 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5110  (class class class)co 7390  ℝcr 11074   + caddc 11078   < clt 11215  ℝ⁺crp 12958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-ltxr 11220  df-rp 12959

This theorem is referenced by:  ltaddrp2d  13036  xov1plusxeqvd  13466  isumltss  15821  effsumlt  16086  tanhlt1  16135  4sqlem12  16934  vdwlem1  16959  prmgaplem7  17035  chfacfscmul0  22752  chfacfpmmul0  22756  nlmvscnlem2  24580  nlmvscnlem1  24581  iccntr  24717  icccmplem2  24719  reconnlem2  24723  opnreen  24727  lebnumii  24872  ipcnlem2  25151  ipcnlem1  25152  ivthlem2  25360  ovolgelb  25388  ovollb2lem  25396  itg2monolem3  25660  dvferm1lem  25895  lhop1lem  25925  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  pserdvlem1  26344  pserdv  26346  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamucov  26955  perfectlem2  27148  bposlem2  27203  pntibndlem2  27509  pntlemb  27515  pntlem3  27527  tpr2rico  33909  omssubaddlem  34297  fibp1  34399  heicant  37656  itg2addnc  37675  rrnequiv  37836  2np3bcnp1  42139  2ap1caineq  42140  pellfundex  42881  rmspecfund  42904  acongeq  42979  jm3.1lem2  43014  oddfl  45283  infrpge  45354  xralrple2  45357  xrralrecnnle  45386  iooiinicc  45547  iooiinioc  45561  fsumnncl  45577  climinf  45611  lptre2pt  45645  ioodvbdlimc1lem2  45937  wallispilem4  46073  dirkertrigeqlem3  46105  dirkercncflem2  46109  fourierdlem63  46174  fourierdlem65  46176  fourierdlem75  46186  fourierdlem79  46190  fouriersw  46236  etransclem35  46274  qndenserrnbllem  46299  omeiunltfirp  46524  hoidmvlelem1  46600  hoidmvlelem3  46602  hoiqssbllem3  46629  iinhoiicc  46679  iunhoiioo  46681  vonioolem2  46686  vonicclem1  46688  preimaleiinlt  46726  smfmullem3  46798  perfectALTVlem2  47727