Theorem ltp1d 12144

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5149  (class class class)co 7409  ℝcr 11109  1c1 11111   + caddc 11113   < clt 11248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447

This theorem is referenced by:  zltp1le  12612  rpnnen1lem5  12965  fznatpl1  13555  fzonn0p1  13709  seqf1olem1  14007  seqf1olem2  14008  bernneq3  14194  expmulnbnd  14198  discr1  14202  discr  14203  bcp1nk  14277  bcpasc  14281  hashfzp1  14391  hashfun  14397  seqcoll  14425  seqcoll2  14426  o1rlimmul  15563  fsum1p  15699  climcndslem2  15796  mertenslem1  15830  fprodntriv  15886  fprod1p  15912  fprodeq0  15919  binomfallfaclem2  15984  fallfacval4  15987  sqrt2irr  16192  nno  16325  iserodd  16768  prmreclem4  16852  prmreclem5  16853  4sqlem11  16888  vdwlem6  16919  vdwlem11  16924  vdwlem12  16925  sylow1lem1  19466  efgsfo  19607  efgred  19616  telgsums  19861  srgbinomlem3  20051  icopnfcnv  24458  cnheibor  24471  pjthlem1  24954  ovolicopnf  25041  uniioombllem3  25102  dvfsumrlim  25548  plyco0  25706  vieta1lem2  25824  mtest  25916  itgulm  25920  psercnlem1  25937  psercn  25938  abelthlem2  25944  abelthlem7  25950  logcnlem4  26153  atanlogsublem  26420  birthdaylem2  26457  efrlim  26474  fsumharmonic  26516  ftalem5  26581  basellem1  26585  basellem3  26587  ppiprm  26655  chtprm  26657  chtdif  26662  ppidif  26667  chtub  26715  perfectlem2  26733  gausslemma2dlem4  26872  gausslemma2dlem6  26875  lgsquadlem2  26884  dchrisum0lem1b  27018  dchrisum0lem3  27022  pntrlog2bndlem6  27086  pntpbnd1  27089  pntpbnd2  27090  pntlemc  27098  pntlemf  27108  ostth2lem1  27121  ostth2lem3  27138  axlowdimlem16  28215  crctcshwlkn0lem3  29066  wwlksnredwwlkn  29149  wwlksext2clwwlk  29310  smcnlem  29950  pjhthlem1  30644  pmtrto1cl  32258  psgnfzto1stlem  32259  cycpmrn  32302  esumpmono  33077  oddpwdc  33353  ballotlemfc0  33491  ballotlemfcc  33492  fsum2dsub  33619  breprexp  33645  subfaclim  34179  erdsze2lem2  34195  cvmliftlem7  34282  cvmliftlem10  34285  relowlssretop  36244  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem28  36516  poimirlem29  36517  poimirlem31  36519  mblfinlem2  36526  itg2addnclem2  36540  isbnd3  36652  aks4d1p1p3  40934  aks4d1p1p2  40935  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  2np3bcnp1  40960  sticksstones6  40967  sticksstones7  40968  sticksstones10  40971  sticksstones12a  40973  sticksstones22  40984  metakunt12  40996  metakunt18  41002  prodsplit  41021  sumcubes  41211  3cubeslem1  41422  eldioph2lem1  41498  pell14qrgapw  41614  rmygeid  41703  monoords  44007  infxr  44077  supxrunb3  44109  uzubioo  44280  limsup10exlem  44488  xlimxrre  44547  xlimpnfv  44554  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnxpaek  44658  dvnmul  44659  iblspltprt  44689  itgspltprt  44695  wallispilem5  44785  stirlinglem1  44790  stirlinglem3  44792  stirlinglem5  44794  stirlinglem6  44795  stirlinglem7  44796  stirlinglem10  44799  fourierdlem11  44834  fourierdlem12  44835  fourierdlem20  44843  fourierdlem30  44853  fourierdlem50  44872  fourierdlem54  44876  fourierdlem64  44886  fourierdlem65  44887  fourierdlem76  44898  fourierdlem77  44899  fourierdlem79  44901  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem114  44936  etransclem46  44996  ioorrnopnxrlem  45022  caratheodorylem1  45242  vonioolem2  45397  vonicclem2  45400  smflimsuplem4  45539  natglobalincr  45591  perfectALTVlem2  46390  aacllem  47848