Theorem ltp1d 12195

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

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5147  (class class class)co 7430  ℝcr 11151  1c1 11153   + caddc 11155   < clt 11292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492

This theorem is referenced by:  zltp1le  12664  rpnnen1lem5  13020  fznatpl1  13614  fzonn0p1  13777  seqf1olem1  14078  seqf1olem2  14079  bernneq3  14266  expmulnbnd  14270  discr1  14274  discr  14275  bcp1nk  14352  bcpasc  14356  hashfzp1  14466  hashfun  14472  seqcoll  14499  seqcoll2  14500  o1rlimmul  15651  fsum1p  15785  climcndslem2  15882  mertenslem1  15916  fprodntriv  15974  fprod1p  16000  fprodeq0  16007  binomfallfaclem2  16072  fallfacval4  16075  sqrt2irr  16281  nno  16415  iserodd  16868  prmreclem4  16952  prmreclem5  16953  4sqlem11  16988  vdwlem6  17019  vdwlem11  17024  vdwlem12  17025  sylow1lem1  19630  efgsfo  19771  efgred  19780  telgsums  20025  srgbinomlem3  20245  icopnfcnv  24986  cnheibor  25000  pjthlem1  25484  ovolicopnf  25572  uniioombllem3  25633  dvfsumrlim  26086  plyco0  26245  vieta1lem2  26367  mtest  26461  itgulm  26465  psercnlem1  26483  psercn  26484  abelthlem2  26490  abelthlem7  26496  logcnlem4  26701  atanlogsublem  26972  birthdaylem2  27009  efrlim  27026  efrlimOLD  27027  fsumharmonic  27069  ftalem5  27134  basellem1  27138  basellem3  27140  ppiprm  27208  chtprm  27210  chtdif  27215  ppidif  27220  chtub  27270  perfectlem2  27288  gausslemma2dlem4  27427  gausslemma2dlem6  27430  lgsquadlem2  27439  dchrisum0lem1b  27573  dchrisum0lem3  27577  pntrlog2bndlem6  27641  pntpbnd1  27644  pntpbnd2  27645  pntlemc  27653  pntlemf  27663  ostth2lem1  27676  ostth2lem3  27693  axlowdimlem16  28986  crctcshwlkn0lem3  29841  wwlksnredwwlkn  29924  wwlksext2clwwlk  30085  smcnlem  30725  pjhthlem1  31419  chnub  32985  pmtrto1cl  33101  psgnfzto1stlem  33102  cycpmrn  33145  esumpmono  34059  oddpwdc  34335  ballotlemfc0  34473  ballotlemfcc  34474  fsum2dsub  34600  breprexp  34626  subfaclim  35172  erdsze2lem2  35188  cvmliftlem7  35275  cvmliftlem10  35278  relowlssretop  37345  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  mblfinlem2  37644  itg2addnclem2  37658  isbnd3  37770  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  2np3bcnp1  42125  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones22  42149  metakunt12  42197  metakunt18  42203  prodsplit  42221  sumcubes  42325  3cubeslem1  42671  eldioph2lem1  42747  pell14qrgapw  42863  rmygeid  42952  monoords  45247  infxr  45316  supxrunb3  45348  uzubioo  45519  limsup10exlem  45727  xlimxrre  45786  xlimpnfv  45793  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnxpaek  45897  dvnmul  45898  iblspltprt  45928  itgspltprt  45934  wallispilem5  46024  stirlinglem1  46029  stirlinglem3  46031  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  fourierdlem11  46073  fourierdlem12  46074  fourierdlem20  46082  fourierdlem30  46092  fourierdlem50  46111  fourierdlem54  46115  fourierdlem64  46125  fourierdlem65  46126  fourierdlem76  46137  fourierdlem77  46138  fourierdlem79  46140  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  etransclem46  46235  ioorrnopnxrlem  46261  caratheodorylem1  46481  vonioolem2  46636  vonicclem2  46639  smflimsuplem4  46778  natglobalincr  46830  perfectALTVlem2  47646  aacllem  49031