Theorem ltp1d 12072

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5098  (class class class)co 7358  ℝcr 11025  1c1 11027   + caddc 11029   < clt 11166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367

This theorem is referenced by:  zltp1le  12541  rpnnen1lem5  12894  fznatpl1  13494  fzonn0p1  13658  seqf1olem1  13964  seqf1olem2  13965  bernneq3  14154  expmulnbnd  14158  discr1  14162  discr  14163  bcp1nk  14240  bcpasc  14244  hashfzp1  14354  hashfun  14360  seqcoll  14387  seqcoll2  14388  o1rlimmul  15542  fsum1p  15676  climcndslem2  15773  mertenslem1  15807  fprodntriv  15865  fprod1p  15891  fprodeq0  15898  binomfallfaclem2  15963  fallfacval4  15966  sqrt2irr  16174  nno  16309  iserodd  16763  prmreclem4  16847  prmreclem5  16848  4sqlem11  16883  vdwlem6  16914  vdwlem11  16919  vdwlem12  16920  chnub  18545  sylow1lem1  19527  efgsfo  19668  efgred  19677  telgsums  19922  srgbinomlem3  20163  icopnfcnv  24896  cnheibor  24910  pjthlem1  25393  ovolicopnf  25481  uniioombllem3  25542  dvfsumrlim  25994  plyco0  26153  vieta1lem2  26275  mtest  26369  itgulm  26373  psercnlem1  26391  psercn  26392  abelthlem2  26398  abelthlem7  26404  logcnlem4  26610  atanlogsublem  26881  birthdaylem2  26918  efrlim  26935  efrlimOLD  26936  fsumharmonic  26978  ftalem5  27043  basellem1  27047  basellem3  27049  ppiprm  27117  chtprm  27119  chtdif  27124  ppidif  27129  chtub  27179  perfectlem2  27197  gausslemma2dlem4  27336  gausslemma2dlem6  27339  lgsquadlem2  27348  dchrisum0lem1b  27482  dchrisum0lem3  27486  pntrlog2bndlem6  27550  pntpbnd1  27553  pntpbnd2  27554  pntlemc  27562  pntlemf  27572  ostth2lem1  27585  ostth2lem3  27602  axlowdimlem16  29030  crctcshwlkn0lem3  29885  wwlksnredwwlkn  29968  wwlksext2clwwlk  30132  smcnlem  30772  pjhthlem1  31466  pmtrto1cl  33181  psgnfzto1stlem  33182  cycpmrn  33225  extdgfialglem1  33849  esumpmono  34236  oddpwdc  34511  ballotlemfc0  34650  ballotlemfcc  34651  fsum2dsub  34764  breprexp  34790  subfaclim  35382  erdsze2lem2  35398  cvmliftlem7  35485  cvmliftlem10  35488  relowlssretop  37568  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem9  37830  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem28  37849  poimirlem29  37850  poimirlem31  37852  mblfinlem2  37859  itg2addnclem2  37873  isbnd3  37985  aks4d1p1p3  42323  aks4d1p1p2  42324  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  2np3bcnp1  42398  sticksstones6  42405  sticksstones7  42406  sticksstones10  42409  sticksstones12a  42411  sticksstones22  42422  sumcubes  42568  3cubeslem1  42926  eldioph2lem1  43002  pell14qrgapw  43118  rmygeid  43206  monoords  45545  infxr  45611  supxrunb3  45643  uzubioo  45811  limsup10exlem  46016  xlimxrre  46075  xlimpnfv  46082  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnxpaek  46186  dvnmul  46187  iblspltprt  46217  itgspltprt  46223  wallispilem5  46313  stirlinglem1  46318  stirlinglem3  46320  stirlinglem5  46322  stirlinglem6  46323  stirlinglem7  46324  stirlinglem10  46327  fourierdlem11  46362  fourierdlem12  46363  fourierdlem20  46371  fourierdlem30  46381  fourierdlem50  46400  fourierdlem54  46404  fourierdlem64  46414  fourierdlem65  46415  fourierdlem76  46426  fourierdlem77  46427  fourierdlem79  46429  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  etransclem46  46524  ioorrnopnxrlem  46550  caratheodorylem1  46770  vonioolem2  46925  vonicclem2  46928  smflimsuplem4  47067  ormklocald  47118  ormkglobd  47119  natglobalincr  47121  perfectALTVlem2  47968  aacllem  50046