Theorem ltp1d 12133

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 12043	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝐴 < (𝐴 + 1))

Syntax hints:   → wi 4   ∈ wcel 2145   class class class wbr 5104  (class class class)co 7400  ℝcr 11087  1c1 11089   + caddc 11091   < clt 11231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432

This theorem is referenced by:  zltp1le  12632  rpnnen1lem5  12993  fznatpl1  13594  fzonn0p1  13759  seqf1olem1  14065  seqf1olem2  14066  bernneq3  14255  expmulnbnd  14259  discr1  14263  discr  14264  bcp1nk  14341  bcpasc  14345  hashfzp1  14456  hashfun  14462  seqcoll  14489  seqcoll2  14490  o1rlimmul  15658  fsum1p  15792  climcndslem2  15892  mertenslem1  15926  fprodntriv  15984  fprod1p  16010  fprodeq0  16017  binomfallfaclem2  16082  fallfacval4  16085  sqrt2irr  16293  nno  16428  iserodd  16883  prmreclem4  16967  prmreclem5  16968  4sqlem11  17003  vdwlem6  17034  vdwlem11  17039  vdwlem12  17040  chnub  18666  sylow1lem1  19656  efgsfo  19797  efgred  19806  telgsums  20051  srgbinomlem3  20298  icopnfcnv  25058  cnheibor  25071  pjthlem1  25553  ovolicopnf  25640  uniioombllem3  25701  dvfsumrlim  26147  plyco0  26306  vieta1lem2  26429  mtest  26521  itgulm  26525  psercnlem1  26542  psercn  26543  abelthlem2  26549  abelthlem7  26555  logcnlem4  26764  atanlogsublem  27034  birthdaylem2  27071  efrlim  27088  fsumharmonic  27130  ftalem5  27195  basellem1  27199  basellem3  27201  ppiprm  27269  chtprm  27271  chtdif  27276  ppidif  27281  chtub  27330  perfectlem2  27348  gausslemma2dlem4  27487  gausslemma2dlem6  27490  lgsquadlem2  27499  dchrisum0lem1b  27633  dchrisum0lem3  27637  pntrlog2bndlem6  27701  pntpbnd1  27704  pntpbnd2  27705  pntlemc  27713  pntlemf  27723  ostth2lem1  27736  ostth2lem3  27753  axlowdimlem16  29212  crctcshwlkn0lem3  30066  wwlksnredwwlkn  30149  wwlksext2clwwlk  30313  smcnlem  30954  pjhthlem1  31648  pmtrto1cl  33327  psgnfzto1stlem  33328  cycpmrn  33371  extdgfialglem1  33994  esumpmono  34381  oddpwdc  34656  ballotlemfc0  34795  ballotlemfcc  34796  fsum2dsub  34906  breprexp  34932  subfaclim  35546  erdsze2lem2  35562  cvmliftlem7  35649  cvmliftlem10  35652  relowlssretop  37864  poimirlem1  38127  poimirlem2  38128  poimirlem3  38129  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem8  38134  poimirlem9  38135  poimirlem10  38136  poimirlem11  38137  poimirlem12  38138  poimirlem15  38141  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem22  38148  poimirlem23  38149  poimirlem24  38150  poimirlem25  38151  poimirlem28  38154  poimirlem29  38155  poimirlem31  38157  mblfinlem2  38164  itg2addnclem2  38178  isbnd3  38290  aks4d1p1p3  42693  aks4d1p1p2  42694  aks4d1p1p6  42697  aks4d1p1p7  42698  aks4d1p1p5  42699  2np3bcnp1  42768  sticksstones6  42775  sticksstones7  42776  sticksstones10  42779  sticksstones12a  42781  sticksstones22  42792  sumcubes  42929  3cubeslem1  43272  eldioph2lem1  43348  pell14qrgapw  43460  rmygeid  43548  monoords  45875  infxr  45941  supxrunb3  45973  uzubioo  46140  limsup10exlem  46345  xlimxrre  46404  xlimpnfv  46411  ioodvbdlimc1lem1  46504  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  dvnxpaek  46515  dvnmul  46516  iblspltprt  46546  itgspltprt  46552  wallispilem5  46642  stirlinglem1  46647  stirlinglem3  46649  stirlinglem5  46651  stirlinglem6  46652  stirlinglem7  46653  stirlinglem10  46656  fourierdlem11  46691  fourierdlem12  46692  fourierdlem20  46700  fourierdlem30  46710  fourierdlem50  46729  fourierdlem54  46733  fourierdlem64  46743  fourierdlem65  46744  fourierdlem76  46755  fourierdlem77  46756  fourierdlem79  46758  fourierdlem102  46781  fourierdlem103  46782  fourierdlem104  46783  fourierdlem114  46793  etransclem46  46853  ioorrnopnxrlem  46879  caratheodorylem1  47099  vonioolem2  47254  vonicclem2  47257  smflimsuplem4  47396  ormklocald  47449  ormkglobd  47450  natglobalincr  47452  perfectALTVlem2  48343  aacllem  50431