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

Theorem ltp1d 11558
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 11468 . 2 (𝐴 ∈ ℝ → 𝐴 < (𝐴 + 1))
31, 2syl 17 1 (𝜑𝐴 < (𝐴 + 1))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105   class class class wbr 5057  (class class class)co 7145  cr 10524  1c1 10526   + caddc 10528   < clt 10663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861
This theorem is referenced by:  zltp1le  12020  rpnnen1lem5  12368  fznatpl1  12949  fzonn0p1  13102  seqf1olem1  13397  seqf1olem2  13398  bernneq3  13580  expmulnbnd  13584  discr1  13588  discr  13589  bcp1nk  13665  bcpasc  13669  hashfzp1  13780  hashfun  13786  seqcoll  13810  seqcoll2  13811  o1rlimmul  14963  fsum1p  15096  climcndslem2  15193  mertenslem1  15228  fprodntriv  15284  fprod1p  15310  fprodeq0  15317  binomfallfaclem2  15382  fallfacval4  15385  sqrt2irr  15590  nno  15721  iserodd  16160  prmreclem4  16243  prmreclem5  16244  4sqlem11  16279  vdwlem6  16310  vdwlem11  16315  vdwlem12  16316  sylow1lem1  18652  efgsfo  18794  efgred  18803  telgsums  19042  srgbinomlem3  19221  icopnfcnv  23473  cnheibor  23486  pjthlem1  23967  ovolicopnf  24052  uniioombllem3  24113  dvfsumrlim  24555  plyco0  24709  vieta1lem2  24827  mtest  24919  itgulm  24923  psercnlem1  24940  psercn  24941  abelthlem2  24947  abelthlem7  24953  logcnlem4  25155  atanlogsublem  25420  birthdaylem2  25457  efrlim  25474  fsumharmonic  25516  ftalem5  25581  basellem1  25585  basellem3  25587  ppiprm  25655  chtprm  25657  chtdif  25662  ppidif  25667  chtub  25715  perfectlem2  25733  gausslemma2dlem4  25872  gausslemma2dlem6  25875  lgsquadlem2  25884  dchrisum0lem1b  26018  dchrisum0lem3  26022  pntrlog2bndlem6  26086  pntpbnd1  26089  pntpbnd2  26090  pntlemc  26098  pntlemf  26108  ostth2lem1  26121  ostth2lem3  26138  axlowdimlem16  26670  crctcshwlkn0lem3  27517  wwlksnredwwlkn  27600  wwlksext2clwwlk  27763  smcnlem  28401  pjhthlem1  29095  pmtrto1cl  30668  psgnfzto1stlem  30669  cycpmrn  30712  esumpmono  31237  oddpwdc  31511  ballotlemfc0  31649  ballotlemfcc  31650  fsum2dsub  31777  breprexp  31803  subfaclim  32332  erdsze2lem2  32348  cvmliftlem7  32435  cvmliftlem10  32438  relowlssretop  34526  poimirlem1  34774  poimirlem2  34775  poimirlem3  34776  poimirlem4  34777  poimirlem6  34779  poimirlem7  34780  poimirlem8  34781  poimirlem9  34782  poimirlem10  34783  poimirlem11  34784  poimirlem12  34785  poimirlem15  34788  poimirlem16  34789  poimirlem17  34790  poimirlem19  34792  poimirlem20  34793  poimirlem22  34795  poimirlem23  34796  poimirlem24  34797  poimirlem25  34798  poimirlem28  34801  poimirlem29  34802  poimirlem31  34804  mblfinlem2  34811  itg2addnclem2  34825  isbnd3  34943  3cubeslem1  39159  eldioph2lem1  39235  pell14qrgapw  39351  rmygeid  39439  monoords  41440  infxr  41511  supxrunb3  41548  uzubioo  41719  limsup10exlem  41929  xlimxrre  41988  xlimpnfv  41995  ioodvbdlimc1lem1  42092  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  dvnxpaek  42103  dvnmul  42104  iblspltprt  42134  itgspltprt  42140  wallispilem5  42231  stirlinglem1  42236  stirlinglem3  42238  stirlinglem5  42240  stirlinglem6  42241  stirlinglem7  42242  stirlinglem10  42245  fourierdlem11  42280  fourierdlem12  42281  fourierdlem20  42289  fourierdlem30  42299  fourierdlem50  42318  fourierdlem54  42322  fourierdlem64  42332  fourierdlem65  42333  fourierdlem76  42344  fourierdlem77  42345  fourierdlem79  42347  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem114  42382  etransclem46  42442  ioorrnopnxrlem  42468  caratheodorylem1  42685  vonioolem2  42840  vonicclem2  42843  smflimsuplem4  42974  perfectALTVlem2  43764  aacllem  44830
  Copyright terms: Public domain W3C validator