Theorem ltp1d 9002

Description: A number is less than itself plus 1. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
ltp1d.1	|- ( ph -> A e. RR )

Assertion

Ref	Expression
ltp1d	|- ( ph -> A < ( A + 1 ) )

Proof of Theorem ltp1d

Step	Hyp	Ref	Expression
1		ltp1d.1	. 2 |- ( ph -> A e. RR )
2		ltp1 8916	. 2 |- ( A e. RR -> A < ( A + 1 ) )
3	1, 2	syl 14	1 |- ( ph -> A < ( A + 1 ) )

Syntax hints:   -> wi 4   e. wcel 2175   class class class wbr 4043  (class class class)co 5943   RRcr 7923   1c1 7925   + caddc 7927   < clt 8106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4479  ax-setind 4584  ax-cnex 8015  ax-resscn 8016  ax-1cn 8017  ax-1re 8018  ax-icn 8019  ax-addcl 8020  ax-addrcl 8021  ax-mulcl 8022  ax-addcom 8024  ax-addass 8026  ax-i2m1 8029  ax-0lt1 8030  ax-0id 8032  ax-rnegex 8033  ax-pre-ltadd 8040

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-rab 2492  df-v 2773  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-opab 4105  df-xp 4680  df-iota 5231  df-fv 5278  df-ov 5946  df-pnf 8108  df-mnf 8109  df-ltxr 8111

This theorem is referenced by:  zltp1le  9426  fznatpl1  10197  fzp1disj  10201  fzneuz  10222  fzp1nel  10225  fzonn0p1  10338  zssinfcl  10373  rebtwn2z  10395  seq3f1olemqsumk  10655  seqf1oglem1  10662  seqf1oglem2  10663  bernneq3  10805  bcp1nk  10905  bcpasc  10909  hashfzp1  10967  seq3coll  10985  resqrexlemover  11292  fsum1p  11700  cvgratnnlembern  11805  cvgratnnlemseq  11808  cvgratnnlemfm  11811  cvgratz  11814  mertenslemi1  11817  fprodntrivap  11866  fprod1p  11881  fprodeq0  11899  efcllemp  11940  nno  12188  sqrt2irr  12455  pcprendvds  12584  pcmpt  12637  1arith  12661  4sqlem11  12695  exmidunben  12768  nninfdclemp1  12792  suplociccreex  15067  perfectlem2  15443  gausslemma2dlem4  15512  gausslemma2dlem6  15515  lgsquadlem2  15526  cvgcmp2nlemabs  15933