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

Theorem ltp1d 11559
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 11469 . 2 (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
31, 2syl 17 1 (𝜑𝐴 < (𝐴 + 1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114   class class class wbr 5042  (class class class)co 7140  cr 10525  1c1 10527   + caddc 10529   < clt 10664
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5437  df-po 5451  df-so 5452  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862
This theorem is referenced by:  zltp1le  12020  rpnnen1lem5  12368  fznatpl1  12956  fzonn0p1  13109  seqf1olem1  13405  seqf1olem2  13406  bernneq3  13588  expmulnbnd  13592  discr1  13596  discr  13597  bcp1nk  13673  bcpasc  13677  hashfzp1  13788  hashfun  13794  seqcoll  13818  seqcoll2  13819  o1rlimmul  14966  fsum1p  15099  climcndslem2  15196  mertenslem1  15231  fprodntriv  15287  fprod1p  15313  fprodeq0  15320  binomfallfaclem2  15385  fallfacval4  15388  sqrt2irr  15593  nno  15722  iserodd  16161  prmreclem4  16244  prmreclem5  16245  4sqlem11  16280  vdwlem6  16311  vdwlem11  16316  vdwlem12  16317  sylow1lem1  18714  efgsfo  18856  efgred  18865  telgsums  19104  srgbinomlem3  19283  icopnfcnv  23545  cnheibor  23558  pjthlem1  24039  ovolicopnf  24126  uniioombllem3  24187  dvfsumrlim  24632  plyco0  24787  vieta1lem2  24905  mtest  24997  itgulm  25001  psercnlem1  25018  psercn  25019  abelthlem2  25025  abelthlem7  25031  logcnlem4  25234  atanlogsublem  25499  birthdaylem2  25536  efrlim  25553  fsumharmonic  25595  ftalem5  25660  basellem1  25664  basellem3  25666  ppiprm  25734  chtprm  25736  chtdif  25741  ppidif  25746  chtub  25794  perfectlem2  25812  gausslemma2dlem4  25951  gausslemma2dlem6  25954  lgsquadlem2  25963  dchrisum0lem1b  26097  dchrisum0lem3  26101  pntrlog2bndlem6  26165  pntpbnd1  26168  pntpbnd2  26169  pntlemc  26177  pntlemf  26187  ostth2lem1  26200  ostth2lem3  26217  axlowdimlem16  26749  crctcshwlkn0lem3  27596  wwlksnredwwlkn  27679  wwlksext2clwwlk  27840  smcnlem  28478  pjhthlem1  29172  pmtrto1cl  30772  psgnfzto1stlem  30773  cycpmrn  30816  esumpmono  31412  oddpwdc  31686  ballotlemfc0  31824  ballotlemfcc  31825  fsum2dsub  31952  breprexp  31978  subfaclim  32509  erdsze2lem2  32525  cvmliftlem7  32612  cvmliftlem10  32615  relowlssretop  34741  poimirlem1  35016  poimirlem2  35017  poimirlem3  35018  poimirlem4  35019  poimirlem6  35021  poimirlem7  35022  poimirlem8  35023  poimirlem9  35024  poimirlem10  35025  poimirlem11  35026  poimirlem12  35027  poimirlem15  35030  poimirlem16  35031  poimirlem17  35032  poimirlem19  35034  poimirlem20  35035  poimirlem22  35037  poimirlem23  35038  poimirlem24  35039  poimirlem25  35040  poimirlem28  35043  poimirlem29  35044  poimirlem31  35046  mblfinlem2  35053  itg2addnclem2  35067  isbnd3  35180  2np3bcnp1  39307  metakunt12  39320  metakunt18  39326  prodsplit  39336  3cubeslem1  39555  eldioph2lem1  39631  pell14qrgapw  39747  rmygeid  39835  monoords  41868  infxr  41938  supxrunb3  41975  uzubioo  42143  limsup10exlem  42353  xlimxrre  42412  xlimpnfv  42419  ioodvbdlimc1lem1  42512  ioodvbdlimc1lem2  42513  ioodvbdlimc2lem  42515  dvnxpaek  42523  dvnmul  42524  iblspltprt  42554  itgspltprt  42560  wallispilem5  42650  stirlinglem1  42655  stirlinglem3  42657  stirlinglem5  42659  stirlinglem6  42660  stirlinglem7  42661  stirlinglem10  42664  fourierdlem11  42699  fourierdlem12  42700  fourierdlem20  42708  fourierdlem30  42718  fourierdlem50  42737  fourierdlem54  42741  fourierdlem64  42751  fourierdlem65  42752  fourierdlem76  42763  fourierdlem77  42764  fourierdlem79  42766  fourierdlem102  42789  fourierdlem103  42790  fourierdlem104  42791  fourierdlem114  42801  etransclem46  42861  ioorrnopnxrlem  42887  caratheodorylem1  43104  vonioolem2  43259  vonicclem2  43262  smflimsuplem4  43393  perfectALTVlem2  44179  aacllem  45268
  Copyright terms: Public domain W3C validator