Theorem ltp1d 12173

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5107  (class class class)co 7417  ℝcr 11127  1c1 11129   + caddc 11131   < clt 11271

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472

This theorem is used by:  zltp1le  12672  rpnnen1lem5  13035  fznatpl1  13637  fzonn0p1  13802  seqf1olem1  14109  seqf1olem2  14110  bernneq3  14299  expmulnbnd  14303  discr1  14307  discr  14308  bcp1nk  14385  bcpasc  14389  hashfzp1  14500  hashfun  14506  seqcoll  14533  seqcoll2  14534  o1rlimmul  15710  fsum1p  15843  climcndslem2  15943  mertenslem1  15977  fprodntriv  16035  fprod1p  16061  fprodeq0  16068  binomfallfaclem2  16132  fallfacval4  16135  sqrt2irr  16343  nno  16478  iserodd  16933  prmreclem4  17017  prmreclem5  17018  4sqlem11  17053  vdwlem6  17084  vdwlem11  17089  vdwlem12  17090  chnub  18716  sylow1lem1  19731  efgsfo  19872  efgred  19881  telgsums  20126  srgbinomlem3  20373  icopnfcnv  25176  cnheibor  25189  pjthlem1  25671  ovolicopnf  25758  uniioombllem3  25819  dvfsumrlim  26265  plyco0  26424  vieta1lem2  26550  mtest  26647  itgulm  26651  psercnlem1  26668  psercn  26669  abelthlem2  26675  abelthlem7  26681  logcnlem4  26890  atanlogsublem  27160  birthdaylem2  27197  efrlim  27214  fsumharmonic  27256  ftalem5  27321  basellem1  27325  basellem3  27327  ppiprm  27395  chtprm  27397  chtdif  27402  ppidif  27407  chtub  27456  perfectlem2  27474  gausslemma2dlem4  27613  gausslemma2dlem6  27616  lgsquadlem2  27625  dchrisum0lem1b  27759  dchrisum0lem3  27763  pntrlog2bndlem6  27827  pntpbnd1  27830  pntpbnd2  27831  pntlemc  27839  pntlemf  27849  ostth2lem1  27862  ostth2lem3  27879  axlowdimlem16  29422  crctcshwlkn0lem3  30288  wwlksnredwwlkn  30371  wwlksext2clwwlk  30535  smcnlem  31186  pjhthlem1  31880  pmtrto1cl  33547  psgnfzto1stlem  33548  cycpmrn  33591  extdgfialglem1  34210  esumpmono  34597  oddpwdc  34873  ballotlemfc0  35012  ballotlemfcc  35013  fsum2dsub  35123  breprexp  35149  subfaclim  35775  erdsze2lem2  35791  cvmliftlem7  35878  cvmliftlem10  35881  relowlssretop  38125  poimirlem1  38378  poimirlem2  38379  poimirlem3  38380  poimirlem4  38381  poimirlem6  38383  poimirlem7  38384  poimirlem8  38385  poimirlem9  38386  poimirlem10  38387  poimirlem11  38388  poimirlem12  38389  poimirlem15  38392  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem22  38399  poimirlem23  38400  poimirlem24  38401  poimirlem25  38402  poimirlem28  38405  poimirlem29  38406  poimirlem31  38408  mblfinlem2  38415  itg2addnclem2  38429  isbnd3  38542  aks4d1p1p3  42943  aks4d1p1p2  42944  aks4d1p1p6  42947  aks4d1p1p7  42948  aks4d1p1p5  42949  2np3bcnp1  43018  sticksstones6  43025  sticksstones7  43026  sticksstones10  43029  sticksstones12a  43031  sticksstones22  43042  sumcubes  43196  3cubeslem1  43537  eldioph2lem1  43613  pell14qrgapw  43725  rmygeid  43813  monoords  46138  infxr  46204  supxrunb3  46236  uzubioo  46403  limsup10exlem  46608  xlimxrre  46667  xlimpnfv  46674  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvnxpaek  46778  dvnmul  46779  iblspltprt  46809  itgspltprt  46815  wallispilem5  46905  stirlinglem1  46910  stirlinglem3  46912  stirlinglem5  46914  stirlinglem6  46915  stirlinglem7  46916  stirlinglem10  46919  fourierdlem11  46954  fourierdlem12  46955  fourierdlem20  46963  fourierdlem30  46973  fourierdlem50  46992  fourierdlem54  46996  fourierdlem64  47006  fourierdlem65  47007  fourierdlem76  47018  fourierdlem77  47019  fourierdlem79  47021  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem114  47056  etransclem46  47116  ioorrnopnxrlem  47142  caratheodorylem1  47362  vonioolem2  47517  vonicclem2  47520  smflimsuplem4  47659  ormklocald  47712  ormkglobd  47713  perfectALTVlem2  48646  aacllem  50780