Theorem ltp1d 12058

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5093  (class class class)co 7352  ℝcr 11011  1c1 11013   + caddc 11015   < clt 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-resscn 11069  ax-1cn 11070  ax-icn 11071  ax-addcl 11072  ax-addrcl 11073  ax-mulcl 11074  ax-mulrcl 11075  ax-mulcom 11076  ax-addass 11077  ax-mulass 11078  ax-distr 11079  ax-i2m1 11080  ax-1ne0 11081  ax-1rid 11082  ax-rnegex 11083  ax-rrecex 11084  ax-cnre 11085  ax-pre-lttri 11086  ax-pre-lttrn 11087  ax-pre-ltadd 11088  ax-pre-mulgt0 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-po 5527  df-so 5528  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11154  df-mnf 11155  df-xr 11156  df-ltxr 11157  df-le 11158  df-sub 11352  df-neg 11353

This theorem is referenced by:  zltp1le  12528  rpnnen1lem5  12885  fznatpl1  13484  fzonn0p1  13648  seqf1olem1  13954  seqf1olem2  13955  bernneq3  14144  expmulnbnd  14148  discr1  14152  discr  14153  bcp1nk  14230  bcpasc  14234  hashfzp1  14344  hashfun  14350  seqcoll  14377  seqcoll2  14378  o1rlimmul  15532  fsum1p  15666  climcndslem2  15763  mertenslem1  15797  fprodntriv  15855  fprod1p  15881  fprodeq0  15888  binomfallfaclem2  15953  fallfacval4  15956  sqrt2irr  16164  nno  16299  iserodd  16753  prmreclem4  16837  prmreclem5  16838  4sqlem11  16873  vdwlem6  16904  vdwlem11  16909  vdwlem12  16910  chnub  18534  sylow1lem1  19516  efgsfo  19657  efgred  19666  telgsums  19911  srgbinomlem3  20152  icopnfcnv  24873  cnheibor  24887  pjthlem1  25370  ovolicopnf  25458  uniioombllem3  25519  dvfsumrlim  25971  plyco0  26130  vieta1lem2  26252  mtest  26346  itgulm  26350  psercnlem1  26368  psercn  26369  abelthlem2  26375  abelthlem7  26381  logcnlem4  26587  atanlogsublem  26858  birthdaylem2  26895  efrlim  26912  efrlimOLD  26913  fsumharmonic  26955  ftalem5  27020  basellem1  27024  basellem3  27026  ppiprm  27094  chtprm  27096  chtdif  27101  ppidif  27106  chtub  27156  perfectlem2  27174  gausslemma2dlem4  27313  gausslemma2dlem6  27316  lgsquadlem2  27325  dchrisum0lem1b  27459  dchrisum0lem3  27463  pntrlog2bndlem6  27527  pntpbnd1  27530  pntpbnd2  27531  pntlemc  27539  pntlemf  27549  ostth2lem1  27562  ostth2lem3  27579  axlowdimlem16  28942  crctcshwlkn0lem3  29797  wwlksnredwwlkn  29880  wwlksext2clwwlk  30044  smcnlem  30684  pjhthlem1  31378  pmtrto1cl  33075  psgnfzto1stlem  33076  cycpmrn  33119  extdgfialglem1  33712  esumpmono  34099  oddpwdc  34374  ballotlemfc0  34513  ballotlemfcc  34514  fsum2dsub  34627  breprexp  34653  subfaclim  35239  erdsze2lem2  35255  cvmliftlem7  35342  cvmliftlem10  35345  relowlssretop  37414  poimirlem1  37667  poimirlem2  37668  poimirlem3  37669  poimirlem4  37670  poimirlem6  37672  poimirlem7  37673  poimirlem8  37674  poimirlem9  37675  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem15  37681  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem22  37688  poimirlem23  37689  poimirlem24  37690  poimirlem25  37691  poimirlem28  37694  poimirlem29  37695  poimirlem31  37697  mblfinlem2  37704  itg2addnclem2  37718  isbnd3  37830  aks4d1p1p3  42168  aks4d1p1p2  42169  aks4d1p1p6  42172  aks4d1p1p7  42173  aks4d1p1p5  42174  2np3bcnp1  42243  sticksstones6  42250  sticksstones7  42251  sticksstones10  42254  sticksstones12a  42256  sticksstones22  42267  sumcubes  42412  3cubeslem1  42782  eldioph2lem1  42858  pell14qrgapw  42974  rmygeid  43062  monoords  45403  infxr  45470  supxrunb3  45502  uzubioo  45670  limsup10exlem  45875  xlimxrre  45934  xlimpnfv  45941  ioodvbdlimc1lem1  46034  ioodvbdlimc1lem2  46035  ioodvbdlimc2lem  46037  dvnxpaek  46045  dvnmul  46046  iblspltprt  46076  itgspltprt  46082  wallispilem5  46172  stirlinglem1  46177  stirlinglem3  46179  stirlinglem5  46181  stirlinglem6  46182  stirlinglem7  46183  stirlinglem10  46186  fourierdlem11  46221  fourierdlem12  46222  fourierdlem20  46230  fourierdlem30  46240  fourierdlem50  46259  fourierdlem54  46263  fourierdlem64  46273  fourierdlem65  46274  fourierdlem76  46285  fourierdlem77  46286  fourierdlem79  46288  fourierdlem102  46311  fourierdlem103  46312  fourierdlem104  46313  fourierdlem114  46323  etransclem46  46383  ioorrnopnxrlem  46409  caratheodorylem1  46629  vonioolem2  46784  vonicclem2  46787  smflimsuplem4  46926  ormklocald  46977  ormkglobd  46978  natglobalincr  46980  perfectALTVlem2  47827  aacllem  49907