Theorem ltp1d 12059

Description: A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
ltp1d.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
ltp1d	⊢ (𝜑 → 𝐴 < (𝐴 + 1))

Proof of Theorem ltp1d

Step	Hyp	Ref	Expression
1		ltp1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltp1 11968	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 < (𝐴 + 1))

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5093  (class class class)co 7352  ℝcr 11012  1c1 11014   + caddc 11016   < clt 11153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089  ax-pre-mulgt0 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-sub 11353  df-neg 11354

This theorem is referenced by:  zltp1le  12528  rpnnen1lem5  12881  fznatpl1  13480  fzonn0p1  13644  seqf1olem1  13950  seqf1olem2  13951  bernneq3  14140  expmulnbnd  14144  discr1  14148  discr  14149  bcp1nk  14226  bcpasc  14230  hashfzp1  14340  hashfun  14346  seqcoll  14373  seqcoll2  14374  o1rlimmul  15528  fsum1p  15662  climcndslem2  15759  mertenslem1  15793  fprodntriv  15851  fprod1p  15877  fprodeq0  15884  binomfallfaclem2  15949  fallfacval4  15952  sqrt2irr  16160  nno  16295  iserodd  16749  prmreclem4  16833  prmreclem5  16834  4sqlem11  16869  vdwlem6  16900  vdwlem11  16905  vdwlem12  16906  chnub  18530  sylow1lem1  19512  efgsfo  19653  efgred  19662  telgsums  19907  srgbinomlem3  20148  icopnfcnv  24868  cnheibor  24882  pjthlem1  25365  ovolicopnf  25453  uniioombllem3  25514  dvfsumrlim  25966  plyco0  26125  vieta1lem2  26247  mtest  26341  itgulm  26345  psercnlem1  26363  psercn  26364  abelthlem2  26370  abelthlem7  26376  logcnlem4  26582  atanlogsublem  26853  birthdaylem2  26890  efrlim  26907  efrlimOLD  26908  fsumharmonic  26950  ftalem5  27015  basellem1  27019  basellem3  27021  ppiprm  27089  chtprm  27091  chtdif  27096  ppidif  27101  chtub  27151  perfectlem2  27169  gausslemma2dlem4  27308  gausslemma2dlem6  27311  lgsquadlem2  27320  dchrisum0lem1b  27454  dchrisum0lem3  27458  pntrlog2bndlem6  27522  pntpbnd1  27525  pntpbnd2  27526  pntlemc  27534  pntlemf  27544  ostth2lem1  27557  ostth2lem3  27574  axlowdimlem16  28937  crctcshwlkn0lem3  29792  wwlksnredwwlkn  29875  wwlksext2clwwlk  30039  smcnlem  30679  pjhthlem1  31373  pmtrto1cl  33075  psgnfzto1stlem  33076  cycpmrn  33119  extdgfialglem1  33726  esumpmono  34113  oddpwdc  34388  ballotlemfc0  34527  ballotlemfcc  34528  fsum2dsub  34641  breprexp  34667  subfaclim  35253  erdsze2lem2  35269  cvmliftlem7  35356  cvmliftlem10  35359  relowlssretop  37428  poimirlem1  37682  poimirlem2  37683  poimirlem3  37684  poimirlem4  37685  poimirlem6  37687  poimirlem7  37688  poimirlem8  37689  poimirlem9  37690  poimirlem10  37691  poimirlem11  37692  poimirlem12  37693  poimirlem15  37696  poimirlem16  37697  poimirlem17  37698  poimirlem19  37700  poimirlem20  37701  poimirlem22  37703  poimirlem23  37704  poimirlem24  37705  poimirlem25  37706  poimirlem28  37709  poimirlem29  37710  poimirlem31  37712  mblfinlem2  37719  itg2addnclem2  37733  isbnd3  37845  aks4d1p1p3  42183  aks4d1p1p2  42184  aks4d1p1p6  42187  aks4d1p1p7  42188  aks4d1p1p5  42189  2np3bcnp1  42258  sticksstones6  42265  sticksstones7  42266  sticksstones10  42269  sticksstones12a  42271  sticksstones22  42282  sumcubes  42432  3cubeslem1  42802  eldioph2lem1  42878  pell14qrgapw  42994  rmygeid  43082  monoords  45423  infxr  45490  supxrunb3  45522  uzubioo  45690  limsup10exlem  45895  xlimxrre  45954  xlimpnfv  45961  ioodvbdlimc1lem1  46054  ioodvbdlimc1lem2  46055  ioodvbdlimc2lem  46057  dvnxpaek  46065  dvnmul  46066  iblspltprt  46096  itgspltprt  46102  wallispilem5  46192  stirlinglem1  46197  stirlinglem3  46199  stirlinglem5  46201  stirlinglem6  46202  stirlinglem7  46203  stirlinglem10  46206  fourierdlem11  46241  fourierdlem12  46242  fourierdlem20  46250  fourierdlem30  46260  fourierdlem50  46279  fourierdlem54  46283  fourierdlem64  46293  fourierdlem65  46294  fourierdlem76  46305  fourierdlem77  46306  fourierdlem79  46308  fourierdlem102  46331  fourierdlem103  46332  fourierdlem104  46333  fourierdlem114  46343  etransclem46  46403  ioorrnopnxrlem  46429  caratheodorylem1  46649  vonioolem2  46804  vonicclem2  46807  smflimsuplem4  46946  ormklocald  46997  ormkglobd  46998  natglobalincr  47000  perfectALTVlem2  47847  aacllem  49927