Theorem ltp1d 12084

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  (class class class)co 7368  ℝcr 11037  1c1 11039   + caddc 11041   < clt 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379

This theorem is referenced by:  zltp1le  12553  rpnnen1lem5  12906  fznatpl1  13506  fzonn0p1  13670  seqf1olem1  13976  seqf1olem2  13977  bernneq3  14166  expmulnbnd  14170  discr1  14174  discr  14175  bcp1nk  14252  bcpasc  14256  hashfzp1  14366  hashfun  14372  seqcoll  14399  seqcoll2  14400  o1rlimmul  15554  fsum1p  15688  climcndslem2  15785  mertenslem1  15819  fprodntriv  15877  fprod1p  15903  fprodeq0  15910  binomfallfaclem2  15975  fallfacval4  15978  sqrt2irr  16186  nno  16321  iserodd  16775  prmreclem4  16859  prmreclem5  16860  4sqlem11  16895  vdwlem6  16926  vdwlem11  16931  vdwlem12  16932  chnub  18557  sylow1lem1  19539  efgsfo  19680  efgred  19689  telgsums  19934  srgbinomlem3  20175  icopnfcnv  24908  cnheibor  24922  pjthlem1  25405  ovolicopnf  25493  uniioombllem3  25554  dvfsumrlim  26006  plyco0  26165  vieta1lem2  26287  mtest  26381  itgulm  26385  psercnlem1  26403  psercn  26404  abelthlem2  26410  abelthlem7  26416  logcnlem4  26622  atanlogsublem  26893  birthdaylem2  26930  efrlim  26947  efrlimOLD  26948  fsumharmonic  26990  ftalem5  27055  basellem1  27059  basellem3  27061  ppiprm  27129  chtprm  27131  chtdif  27136  ppidif  27141  chtub  27191  perfectlem2  27209  gausslemma2dlem4  27348  gausslemma2dlem6  27351  lgsquadlem2  27360  dchrisum0lem1b  27494  dchrisum0lem3  27498  pntrlog2bndlem6  27562  pntpbnd1  27565  pntpbnd2  27566  pntlemc  27574  pntlemf  27584  ostth2lem1  27597  ostth2lem3  27614  axlowdimlem16  29042  crctcshwlkn0lem3  29897  wwlksnredwwlkn  29980  wwlksext2clwwlk  30144  smcnlem  30784  pjhthlem1  31478  pmtrto1cl  33192  psgnfzto1stlem  33193  cycpmrn  33236  extdgfialglem1  33869  esumpmono  34256  oddpwdc  34531  ballotlemfc0  34670  ballotlemfcc  34671  fsum2dsub  34784  breprexp  34810  subfaclim  35401  erdsze2lem2  35417  cvmliftlem7  35504  cvmliftlem10  35507  relowlssretop  37615  poimirlem1  37869  poimirlem2  37870  poimirlem3  37871  poimirlem4  37872  poimirlem6  37874  poimirlem7  37875  poimirlem8  37876  poimirlem9  37877  poimirlem10  37878  poimirlem11  37879  poimirlem12  37880  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  poimirlem22  37890  poimirlem23  37891  poimirlem24  37892  poimirlem25  37893  poimirlem28  37896  poimirlem29  37897  poimirlem31  37899  mblfinlem2  37906  itg2addnclem2  37920  isbnd3  38032  aks4d1p1p3  42436  aks4d1p1p2  42437  aks4d1p1p6  42440  aks4d1p1p7  42441  aks4d1p1p5  42442  2np3bcnp1  42511  sticksstones6  42518  sticksstones7  42519  sticksstones10  42522  sticksstones12a  42524  sticksstones22  42535  sumcubes  42680  3cubeslem1  43038  eldioph2lem1  43114  pell14qrgapw  43230  rmygeid  43318  monoords  45656  infxr  45722  supxrunb3  45754  uzubioo  45922  limsup10exlem  46127  xlimxrre  46186  xlimpnfv  46193  ioodvbdlimc1lem1  46286  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  dvnxpaek  46297  dvnmul  46298  iblspltprt  46328  itgspltprt  46334  wallispilem5  46424  stirlinglem1  46429  stirlinglem3  46431  stirlinglem5  46433  stirlinglem6  46434  stirlinglem7  46435  stirlinglem10  46438  fourierdlem11  46473  fourierdlem12  46474  fourierdlem20  46482  fourierdlem30  46492  fourierdlem50  46511  fourierdlem54  46515  fourierdlem64  46525  fourierdlem65  46526  fourierdlem76  46537  fourierdlem77  46538  fourierdlem79  46540  fourierdlem102  46563  fourierdlem103  46564  fourierdlem104  46565  fourierdlem114  46575  etransclem46  46635  ioorrnopnxrlem  46661  caratheodorylem1  46881  vonioolem2  47036  vonicclem2  47039  smflimsuplem4  47178  ormklocald  47229  ormkglobd  47230  natglobalincr  47232  perfectALTVlem2  48079  aacllem  50157