Theorem lep1d 12255

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

Hypothesis

Ref	Expression
ltp1d.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
lep1d	⊢ (𝜑 → 𝐴 ≤ (𝐴 + 1))

Proof of Theorem lep1d

Step	Hyp	Ref	Expression
1		ltp1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		lep1 12165	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ≤ (𝐴 + 1))
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝐴 ≤ (𝐴 + 1))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  (class class class)co 7424  ℝcr 11206  1c1 11208   + caddc 11210   ≤ cle 11351

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-1cn 11265  ax-icn 11266  ax-addcl 11267  ax-addrcl 11268  ax-mulcl 11269  ax-mulrcl 11270  ax-mulcom 11271  ax-addass 11272  ax-mulass 11273  ax-distr 11274  ax-i2m1 11275  ax-1ne0 11276  ax-1rid 11277  ax-rnegex 11278  ax-rrecex 11279  ax-cnre 11280  ax-pre-lttri 11281  ax-pre-lttrn 11282  ax-pre-ltadd 11283  ax-pre-mulgt0 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-er 8725  df-en 8982  df-dom 8983  df-sdom 8984  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356  df-sub 11550  df-neg 11551

This theorem is used by:  fzossfzop1  13885  modltm1p1mod  14073  facubnd  14451  swrds2  15100  lo1bddrp  15701  mulcn2  15772  harmonic  16037  expcnv  16042  prmfac1  16905  eulerthlem2  16968  telgsumfzs  20212  nlmvscnlem2  25013  nghmcn  25073  ipcnlem2  25574  ovolicc2lem3  25849  ovolicopnf  25854  dyadf  25921  dyadovol  25923  dyadmaxlem  25927  volsup2  25935  mbfi1fseqlem5  26049  itg2gt0  26090  itg2cnlem1  26091  dvfsumle  26350  dvfsumabs  26352  dvfsumlem3  26357  leibpi  27279  efrlim  27306  zetacvg  27351  lgamgulmlem3  27367  lgamgulmlem5  27369  basellem2  27418  basellem3  27419  basellem5  27421  basellem6  27422  ppip1le  27497  bcmono  27613  rplogsumlem2  27821  dchrisumlem1  27825  dchrisumlem2  27826  dchrisumlem3  27827  selberg2lem  27886  logdivbnd  27892  pntrlog2bndlem2  27914  pntrlog2bndlem5  27917  pntlemk  27942  pntleml  27947  crctcshwlkn0lem3  30410  crctcshwlkn0lem5  30412  wwlksnred  30490  wwlksnextproplem1  30507  wwlksnextproplem2  30508  wwlksnextproplem3  30509  clwlkclwwlkf1lem2  30605  clwwlkf  30647  clwwlkf1  30649  wwlksubclwwlk  30658  eupth2lems  30848  numclwlk2lem2f  30987  pmtrto1cl  33710  psgnfzto1stlem  33711  fzto1st  33714  psgnfzto1st  33716  constrresqrtcl  34459  sxbrsigalem2  34968  dstfrvclim1  35160  fsum2dsub  35286  breprexplemc  35311  poimirlem7  38682  poimirlem15  38690  rrntotbnd  38907  aks4d1p1p7  43261  aks4d1p1p5  43262  aks4d1p1  43263  2np3bcnp1  43331  sticksstones6  43338  sticksstones7  43339  sticksstones10  43342  sticksstones12a  43344  sticksstones12  43345  sticksstones22  43355  jm2.17a  44104  hbt  44269  fmul01lt1lem1  46732  sumnnodd  46778  itgspltprt  47125  stoweidlem20  47166  stoweidlem26  47172  fzopredsuc  48530  smonoord  48583  lighneallem4a  48829