Theorem lep1d 11763

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

Syntax hints:   → wi 4   ∈ wcel 2110   class class class wbr 5053  (class class class)co 7213  ℝcr 10728  1c1 10730   + caddc 10732   ≤ cle 10868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-po 5468  df-so 5469  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065

This theorem is referenced by:  fzossfzop1  13320  modltm1p1mod  13496  facubnd  13866  swrds2  14505  lo1bddrp  15086  mulcn2  15157  harmonic  15423  expcnv  15428  prmfac1  16278  eulerthlem2  16335  telgsumfzs  19374  nlmvscnlem2  23583  nghmcn  23643  ipcnlem2  24141  ovolicc2lem3  24416  ovolicopnf  24421  dyadf  24488  dyadovol  24490  dyadmaxlem  24494  volsup2  24502  mbfi1fseqlem5  24617  itg2gt0  24658  itg2cnlem1  24659  dvfsumle  24918  dvfsumabs  24920  dvfsumlem3  24925  leibpi  25825  efrlim  25852  zetacvg  25897  lgamgulmlem3  25913  lgamgulmlem5  25915  basellem2  25964  basellem3  25965  basellem5  25967  basellem6  25968  ppip1le  26043  bcmono  26158  rplogsumlem2  26366  dchrisumlem1  26370  dchrisumlem2  26371  dchrisumlem3  26372  selberg2lem  26431  logdivbnd  26437  pntrlog2bndlem2  26459  pntrlog2bndlem5  26462  pntlemk  26487  pntleml  26492  crctcshwlkn0lem3  27896  crctcshwlkn0lem5  27898  wwlksnred  27976  wwlksnextproplem1  27993  wwlksnextproplem2  27994  wwlksnextproplem3  27995  clwlkclwwlkf1lem2  28088  clwwlkf  28130  clwwlkf1  28132  wwlksubclwwlk  28141  eupth2lems  28321  numclwlk2lem2f  28460  pmtrto1cl  31085  psgnfzto1stlem  31086  fzto1st  31089  psgnfzto1st  31091  sxbrsigalem2  31965  dstfrvclim1  32156  fsum2dsub  32299  breprexplemc  32324  poimirlem7  35521  poimirlem15  35529  rrntotbnd  35731  aks4d1p1p7  39815  aks4d1p1p5  39816  aks4d1p1  39817  2np3bcnp1  39822  sticksstones6  39829  sticksstones7  39830  sticksstones10  39833  sticksstones12a  39835  sticksstones12  39836  sticksstones22  39846  metakunt12  39858  jm2.17a  40485  hbt  40658  fmul01lt1lem1  42800  sumnnodd  42846  itgspltprt  43195  stoweidlem20  43236  stoweidlem26  43242  fzopredsuc  44488  smonoord  44496  lighneallem4a  44733