Theorem ltaddrpd 13097

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 13059	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → 𝐴 < (𝐴 + 𝐵))
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → 𝐴 < (𝐴 + 𝐵))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143   class class class wbr 5109  (class class class)co 7410  ℝcr 11103   + caddc 11107   < clt 11247  ℝ⁺crp 13020

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11249  df-mnf 11250  df-ltxr 11252  df-rp 13021

This theorem is used by:  ltaddrp2d  13098  xov1plusxeqvd  13529  isumltss  15907  effsumlt  16171  tanhlt1  16220  4sqlem12  17020  vdwlem1  17045  prmgaplem7  17121  chfacfscmul0  23024  chfacfpmmul0  23028  nlmvscnlem2  24851  nlmvscnlem1  24852  iccntr  24988  icccmplem2  24990  reconnlem2  24994  opnreen  24998  lebnumii  25134  ipcnlem2  25412  ipcnlem1  25413  ivthlem2  25620  ovolgelb  25648  ovollb2lem  25656  itg2monolem3  25920  dvferm1lem  26152  lhop1lem  26181  lhop  26184  dvcnvrelem1  26185  dvcnvrelem2  26186  pserdvlem1  26599  pserdv  26601  lgamgulmlem2  27203  lgamgulmlem3  27204  lgamucov  27211  perfectlem2  27403  bposlem2  27458  pntibndlem2  27764  pntlemb  27770  pntlem3  27782  tpr2rico  34311  omssubaddlem  34698  fibp1  34800  qdiff  37999  heicant  38334  itg2addnc  38353  rrnequiv  38514  2np3bcnp1  42939  2ap1caineq  42940  pellfundex  43641  rmspecfund  43664  acongeq  43738  jm3.1lem2  43773  oddfl  46025  infrpge  46095  xralrple2  46098  xrralrecnnle  46126  iooiinicc  46286  iooiinioc  46300  fsumnncl  46316  climinf  46350  lptre2pt  46382  ioodvbdlimc1lem2  46674  wallispilem4  46810  dirkertrigeqlem3  46842  dirkercncflem2  46846  fourierdlem63  46911  fourierdlem65  46913  fourierdlem75  46923  fourierdlem79  46927  fouriersw  46973  etransclem35  47011  qndenserrnbllem  47036  omeiunltfirp  47261  hoidmvlelem1  47337  hoidmvlelem3  47339  hoiqssbllem3  47366  iinhoiicc  47416  iunhoiioo  47418  vonioolem2  47423  vonicclem1  47425  preimaleiinlt  47463  smfmullem3  47535  perfectALTVlem2  48515