Theorem ltp1d 11914

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5075  (class class class)co 7284  ℝcr 10879  1c1 10881   + caddc 10883   < clt 11018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217

This theorem is referenced by:  zltp1le  12379  rpnnen1lem5  12730  fznatpl1  13319  fzonn0p1  13473  seqf1olem1  13771  seqf1olem2  13772  bernneq3  13955  expmulnbnd  13959  discr1  13963  discr  13964  bcp1nk  14040  bcpasc  14044  hashfzp1  14155  hashfun  14161  seqcoll  14187  seqcoll2  14188  o1rlimmul  15337  fsum1p  15474  climcndslem2  15571  mertenslem1  15605  fprodntriv  15661  fprod1p  15687  fprodeq0  15694  binomfallfaclem2  15759  fallfacval4  15762  sqrt2irr  15967  nno  16100  iserodd  16545  prmreclem4  16629  prmreclem5  16630  4sqlem11  16665  vdwlem6  16696  vdwlem11  16701  vdwlem12  16702  sylow1lem1  19212  efgsfo  19354  efgred  19363  telgsums  19603  srgbinomlem3  19787  icopnfcnv  24114  cnheibor  24127  pjthlem1  24610  ovolicopnf  24697  uniioombllem3  24758  dvfsumrlim  25204  plyco0  25362  vieta1lem2  25480  mtest  25572  itgulm  25576  psercnlem1  25593  psercn  25594  abelthlem2  25600  abelthlem7  25606  logcnlem4  25809  atanlogsublem  26074  birthdaylem2  26111  efrlim  26128  fsumharmonic  26170  ftalem5  26235  basellem1  26239  basellem3  26241  ppiprm  26309  chtprm  26311  chtdif  26316  ppidif  26321  chtub  26369  perfectlem2  26387  gausslemma2dlem4  26526  gausslemma2dlem6  26529  lgsquadlem2  26538  dchrisum0lem1b  26672  dchrisum0lem3  26676  pntrlog2bndlem6  26740  pntpbnd1  26743  pntpbnd2  26744  pntlemc  26752  pntlemf  26762  ostth2lem1  26775  ostth2lem3  26792  axlowdimlem16  27334  crctcshwlkn0lem3  28186  wwlksnredwwlkn  28269  wwlksext2clwwlk  28430  smcnlem  29068  pjhthlem1  29762  pmtrto1cl  31375  psgnfzto1stlem  31376  cycpmrn  31419  esumpmono  32056  oddpwdc  32330  ballotlemfc0  32468  ballotlemfcc  32469  fsum2dsub  32596  breprexp  32622  subfaclim  33159  erdsze2lem2  33175  cvmliftlem7  33262  cvmliftlem10  33265  relowlssretop  35543  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem9  35795  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem28  35814  poimirlem29  35815  poimirlem31  35817  mblfinlem2  35824  itg2addnclem2  35838  isbnd3  35951  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  2np3bcnp1  40107  sticksstones6  40114  sticksstones7  40115  sticksstones10  40118  sticksstones12a  40120  sticksstones22  40131  metakunt12  40143  metakunt18  40149  prodsplit  40168  3cubeslem1  40513  eldioph2lem1  40589  pell14qrgapw  40705  rmygeid  40793  monoords  42843  infxr  42913  supxrunb3  42946  uzubioo  43112  limsup10exlem  43320  xlimxrre  43379  xlimpnfv  43386  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnxpaek  43490  dvnmul  43491  iblspltprt  43521  itgspltprt  43527  wallispilem5  43617  stirlinglem1  43622  stirlinglem3  43624  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem10  43631  fourierdlem11  43666  fourierdlem12  43667  fourierdlem20  43675  fourierdlem30  43685  fourierdlem50  43704  fourierdlem54  43708  fourierdlem64  43718  fourierdlem65  43719  fourierdlem76  43730  fourierdlem77  43731  fourierdlem79  43733  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem114  43768  etransclem46  43828  ioorrnopnxrlem  43854  caratheodorylem1  44071  vonioolem2  44226  vonicclem2  44229  smflimsuplem4  44367  perfectALTVlem2  45185  aacllem  46516  natglobalincr  46523