Theorem ltp1d 11835

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  (class class class)co 7255  ℝcr 10801  1c1 10803   + caddc 10805   < clt 10940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138

This theorem is referenced by:  zltp1le  12300  rpnnen1lem5  12650  fznatpl1  13239  fzonn0p1  13392  seqf1olem1  13690  seqf1olem2  13691  bernneq3  13874  expmulnbnd  13878  discr1  13882  discr  13883  bcp1nk  13959  bcpasc  13963  hashfzp1  14074  hashfun  14080  seqcoll  14106  seqcoll2  14107  o1rlimmul  15256  fsum1p  15393  climcndslem2  15490  mertenslem1  15524  fprodntriv  15580  fprod1p  15606  fprodeq0  15613  binomfallfaclem2  15678  fallfacval4  15681  sqrt2irr  15886  nno  16019  iserodd  16464  prmreclem4  16548  prmreclem5  16549  4sqlem11  16584  vdwlem6  16615  vdwlem11  16620  vdwlem12  16621  sylow1lem1  19118  efgsfo  19260  efgred  19269  telgsums  19509  srgbinomlem3  19693  icopnfcnv  24011  cnheibor  24024  pjthlem1  24506  ovolicopnf  24593  uniioombllem3  24654  dvfsumrlim  25100  plyco0  25258  vieta1lem2  25376  mtest  25468  itgulm  25472  psercnlem1  25489  psercn  25490  abelthlem2  25496  abelthlem7  25502  logcnlem4  25705  atanlogsublem  25970  birthdaylem2  26007  efrlim  26024  fsumharmonic  26066  ftalem5  26131  basellem1  26135  basellem3  26137  ppiprm  26205  chtprm  26207  chtdif  26212  ppidif  26217  chtub  26265  perfectlem2  26283  gausslemma2dlem4  26422  gausslemma2dlem6  26425  lgsquadlem2  26434  dchrisum0lem1b  26568  dchrisum0lem3  26572  pntrlog2bndlem6  26636  pntpbnd1  26639  pntpbnd2  26640  pntlemc  26648  pntlemf  26658  ostth2lem1  26671  ostth2lem3  26688  axlowdimlem16  27228  crctcshwlkn0lem3  28078  wwlksnredwwlkn  28161  wwlksext2clwwlk  28322  smcnlem  28960  pjhthlem1  29654  pmtrto1cl  31268  psgnfzto1stlem  31269  cycpmrn  31312  esumpmono  31947  oddpwdc  32221  ballotlemfc0  32359  ballotlemfcc  32360  fsum2dsub  32487  breprexp  32513  subfaclim  33050  erdsze2lem2  33066  cvmliftlem7  33153  cvmliftlem10  33156  relowlssretop  35461  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem8  35712  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem28  35732  poimirlem29  35733  poimirlem31  35735  mblfinlem2  35742  itg2addnclem2  35756  isbnd3  35869  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  2np3bcnp1  40028  sticksstones6  40035  sticksstones7  40036  sticksstones10  40039  sticksstones12a  40041  sticksstones22  40052  metakunt12  40064  metakunt18  40070  prodsplit  40089  3cubeslem1  40422  eldioph2lem1  40498  pell14qrgapw  40614  rmygeid  40702  monoords  42726  infxr  42796  supxrunb3  42829  uzubioo  42995  limsup10exlem  43203  xlimxrre  43262  xlimpnfv  43269  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnxpaek  43373  dvnmul  43374  iblspltprt  43404  itgspltprt  43410  wallispilem5  43500  stirlinglem1  43505  stirlinglem3  43507  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  fourierdlem11  43549  fourierdlem12  43550  fourierdlem20  43558  fourierdlem30  43568  fourierdlem50  43587  fourierdlem54  43591  fourierdlem64  43601  fourierdlem65  43602  fourierdlem76  43613  fourierdlem77  43614  fourierdlem79  43616  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  etransclem46  43711  ioorrnopnxrlem  43737  caratheodorylem1  43954  vonioolem2  44109  vonicclem2  44112  smflimsuplem4  44243  perfectALTVlem2  45062  aacllem  46391