Theorem ltp1d 11308

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 4886  (class class class)co 6922  ℝcr 10271  1c1 10273   + caddc 10275   < clt 10411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-po 5274  df-so 5275  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609

This theorem is referenced by:  zltp1le  11779  rpnnen1lem5  12128  fznatpl1  12712  fzonn0p1  12864  seqf1olem1  13158  seqf1olem2  13159  bernneq3  13311  expmulnbnd  13315  discr1  13319  discr  13320  bcp1nk  13422  bcpasc  13426  hashfzp1  13532  hashfun  13538  seqcoll  13562  seqcoll2  13563  o1rlimmul  14757  fsum1p  14889  climcndslem2  14986  mertenslem1  15019  fprodntriv  15075  fprod1p  15101  fprodeq0  15108  binomfallfaclem2  15173  fallfacval4  15176  sqrt2irr  15382  nno  15512  iserodd  15944  prmreclem4  16027  prmreclem5  16028  4sqlem11  16063  vdwlem6  16094  vdwlem11  16099  vdwlem12  16100  sylow1lem1  18397  efgsfo  18537  efgred  18547  telgsums  18777  srgbinomlem3  18929  icopnfcnv  23149  cnheibor  23162  pjthlem1  23643  ovolicopnf  23728  uniioombllem3  23789  dvfsumrlim  24231  plyco0  24385  vieta1lem2  24503  mtest  24595  itgulm  24599  psercnlem1  24616  psercn  24617  abelthlem2  24623  abelthlem7  24629  logcnlem4  24828  atanlogsublem  25093  birthdaylem2  25131  efrlim  25148  fsumharmonic  25190  ftalem5  25255  basellem1  25259  basellem3  25261  ppiprm  25329  chtprm  25331  chtdif  25336  ppidif  25341  chtub  25389  perfectlem2  25407  gausslemma2dlem4  25546  gausslemma2dlem6  25549  lgsquadlem2  25558  dchrisum0lem1b  25656  dchrisum0lem3  25660  pntrlog2bndlem6  25724  pntpbnd1  25727  pntpbnd2  25728  pntlemc  25736  pntlemf  25746  ostth2lem1  25759  ostth2lem3  25776  axlowdimlem16  26306  crctcshwlkn0lem3  27161  wwlksnredwwlkn  27257  wwlksnredwwlknOLD  27258  wwlksext2clwwlk  27454  smcnlem  28124  pjhthlem1  28822  pmtrto1cl  30447  psgnfzto1stlem  30448  esumpmono  30739  oddpwdc  31014  ballotlemfc0  31153  ballotlemfcc  31154  fsum2dsub  31287  breprexp  31313  subfaclim  31769  erdsze2lem2  31785  cvmliftlem7  31872  cvmliftlem10  31875  relowlssretop  33806  poimirlem1  34020  poimirlem2  34021  poimirlem3  34022  poimirlem4  34023  poimirlem6  34025  poimirlem7  34026  poimirlem8  34027  poimirlem9  34028  poimirlem10  34029  poimirlem11  34030  poimirlem12  34031  poimirlem15  34034  poimirlem16  34035  poimirlem17  34036  poimirlem19  34038  poimirlem20  34039  poimirlem22  34041  poimirlem23  34042  poimirlem24  34043  poimirlem25  34044  poimirlem28  34047  poimirlem29  34048  poimirlem31  34050  mblfinlem2  34057  itg2addnclem2  34071  isbnd3  34191  eldioph2lem1  38265  pell14qrgapw  38382  rmygeid  38472  monoords  40402  infxr  40473  supxrunb3  40511  uzubioo  40684  limsup10exlem  40894  xlimxrre  40953  xlimpnfv  40960  ioodvbdlimc1lem1  41056  ioodvbdlimc1lem2  41057  ioodvbdlimc2lem  41059  dvnxpaek  41067  dvnmul  41068  iblspltprt  41098  itgspltprt  41104  wallispilem5  41195  stirlinglem1  41200  stirlinglem3  41202  stirlinglem5  41204  stirlinglem6  41205  stirlinglem7  41206  stirlinglem10  41209  fourierdlem11  41244  fourierdlem12  41245  fourierdlem20  41253  fourierdlem30  41263  fourierdlem50  41282  fourierdlem54  41286  fourierdlem64  41296  fourierdlem65  41297  fourierdlem76  41308  fourierdlem77  41309  fourierdlem79  41311  fourierdlem102  41334  fourierdlem103  41335  fourierdlem104  41336  fourierdlem114  41346  etransclem46  41406  ioorrnopnxrlem  41432  caratheodorylem1  41649  vonioolem2  41804  vonicclem2  41807  smflimsuplem4  41938  perfectALTVlem2  42638  aacllem  43635