MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltp1d Structured version   Visualization version   GIF version

Theorem ltp1d 10806
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
StepHypRef Expression
1 ltp1d.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltp1 10713 . 2 (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
31, 2syl 17 1 (𝜑𝐴 < (𝐴 + 1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976   class class class wbr 4577  (class class class)co 6527  cr 9792  1c1 9794   + caddc 9796   < clt 9931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7607  df-en 7820  df-dom 7821  df-sdom 7822  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121
This theorem is referenced by:  zltp1le  11263  rpnnen1lem5  11653  rpnnen1lem5OLD  11659  fznatpl1  12223  fzonn0p1  12369  seqf1olem1  12660  seqf1olem2  12661  bernneq3  12812  expmulnbnd  12816  discr1  12820  discr  12821  bcp1nk  12924  bcpasc  12928  hashfzp1  13033  hashfun  13039  seqcoll  13060  seqcoll2  13061  o1rlimmul  14146  fsum1p  14275  climcndslem2  14370  mertenslem1  14404  fprodntriv  14460  fprod1p  14486  fprodeq0  14493  binomfallfaclem2  14559  fallfacval4  14562  sqrt2irr  14766  nno  14885  iserodd  15327  prmreclem4  15410  prmreclem5  15411  4sqlem11  15446  vdwlem6  15477  vdwlem11  15482  vdwlem12  15483  sylow1lem1  17785  efgsfo  17924  efgred  17933  telgsums  18162  srgbinomlem3  18314  icopnfcnv  22497  cnheibor  22510  pjthlem1  22961  ovolicopnf  23044  uniioombllem3  23104  dvfsumrlim  23543  plyco0  23697  vieta1lem2  23815  mtest  23907  itgulm  23911  psercnlem1  23928  psercn  23929  abelthlem2  23935  abelthlem7  23941  logcnlem4  24136  atanlogsublem  24387  birthdaylem2  24424  efrlim  24441  fsumharmonic  24483  ftalem5  24548  basellem1  24552  basellem3  24554  ppiprm  24622  chtprm  24624  chtdif  24629  ppidif  24634  chtub  24682  perfectlem2  24700  gausslemma2dlem4  24839  gausslemma2dlem6  24842  lgsquadlem2  24851  dchrisum0lem1b  24949  dchrisum0lem3  24953  pntrlog2bndlem6  25017  pntpbnd1  25020  pntpbnd2  25021  pntlemc  25029  pntlemf  25039  ostth2lem1  25052  ostth2lem3  25069  axlowdimlem16  25583  wwlknredwwlkn  26048  wwlkext2clwwlk  26125  eupap1  26297  eupath2lem3  26300  smcnlem  26765  pjhthlem1  27468  pmtrto1cl  29014  psgnfzto1stlem  29015  esumpmono  29302  oddpwdc  29577  ballotlemfc0  29715  ballotlemfcc  29716  subfaclim  30258  erdsze2lem2  30274  cvmliftlem7  30361  cvmliftlem10  30364  relowlssretop  32211  poimirlem1  32404  poimirlem2  32405  poimirlem3  32406  poimirlem4  32407  poimirlem6  32409  poimirlem7  32410  poimirlem8  32411  poimirlem9  32412  poimirlem10  32413  poimirlem11  32414  poimirlem12  32415  poimirlem15  32418  poimirlem16  32419  poimirlem17  32420  poimirlem19  32422  poimirlem20  32423  poimirlem22  32425  poimirlem23  32426  poimirlem24  32427  poimirlem25  32428  poimirlem28  32431  poimirlem29  32432  poimirlem31  32434  mblfinlem2  32441  itg2addnclem2  32456  isbnd3  32577  eldioph2lem1  36165  pell14qrgapw  36282  rmygeid  36373  monoords  38276  infxr  38348  ioodvbdlimc1lem1  38645  ioodvbdlimc1lem2  38646  ioodvbdlimc2lem  38648  dvnxpaek  38656  dvnmul  38657  iblspltprt  38689  itgspltprt  38695  wallispilem5  38786  stirlinglem1  38791  stirlinglem3  38793  stirlinglem5  38795  stirlinglem6  38796  stirlinglem7  38797  stirlinglem10  38800  fourierdlem11  38835  fourierdlem12  38836  fourierdlem20  38844  fourierdlem30  38854  fourierdlem50  38873  fourierdlem54  38877  fourierdlem64  38887  fourierdlem65  38888  fourierdlem76  38899  fourierdlem77  38900  fourierdlem79  38902  fourierdlem102  38925  fourierdlem103  38926  fourierdlem104  38927  fourierdlem114  38937  etransclem46  38997  ioorrnopnxrlem  39026  caratheodorylem1  39240  vonioolem2  39396  vonicclem2  39399  perfectALTVlem2  39990  crctcsh1wlkn0lem3  41037  wwlksnredwwlkn  41123  wwlksext2clwwlk  41253  aacllem  42339
  Copyright terms: Public domain W3C validator