Theorem lep1d 12178

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5124  (class class class)co 7410  ℝcr 11133  1c1 11135   + caddc 11137   ≤ cle 11275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474

This theorem is referenced by:  fzossfzop1  13764  modltm1p1mod  13946  facubnd  14323  swrds2  14964  lo1bddrp  15546  mulcn2  15617  harmonic  15880  expcnv  15885  prmfac1  16744  eulerthlem2  16806  telgsumfzs  19975  nlmvscnlem2  24629  nghmcn  24689  ipcnlem2  25201  ovolicc2lem3  25477  ovolicopnf  25482  dyadf  25549  dyadovol  25551  dyadmaxlem  25555  volsup2  25563  mbfi1fseqlem5  25677  itg2gt0  25718  itg2cnlem1  25719  dvfsumle  25983  dvfsumleOLD  25984  dvfsumabs  25986  dvfsumlem3  25992  leibpi  26909  efrlim  26936  efrlimOLD  26937  zetacvg  26982  lgamgulmlem3  26998  lgamgulmlem5  27000  basellem2  27049  basellem3  27050  basellem5  27052  basellem6  27053  ppip1le  27128  bcmono  27245  rplogsumlem2  27453  dchrisumlem1  27457  dchrisumlem2  27458  dchrisumlem3  27459  selberg2lem  27518  logdivbnd  27524  pntrlog2bndlem2  27546  pntrlog2bndlem5  27549  pntlemk  27574  pntleml  27579  crctcshwlkn0lem3  29799  crctcshwlkn0lem5  29801  wwlksnred  29879  wwlksnextproplem1  29896  wwlksnextproplem2  29897  wwlksnextproplem3  29898  clwlkclwwlkf1lem2  29991  clwwlkf  30033  clwwlkf1  30035  wwlksubclwwlk  30044  eupth2lems  30224  numclwlk2lem2f  30363  pmtrto1cl  33115  psgnfzto1stlem  33116  fzto1st  33119  psgnfzto1st  33121  constrresqrtcl  33816  sxbrsigalem2  34323  dstfrvclim1  34515  fsum2dsub  34644  breprexplemc  34669  poimirlem7  37656  poimirlem15  37664  rrntotbnd  37865  aks4d1p1p7  42092  aks4d1p1p5  42093  aks4d1p1  42094  2np3bcnp1  42162  sticksstones6  42169  sticksstones7  42170  sticksstones10  42173  sticksstones12a  42175  sticksstones12  42176  sticksstones22  42186  jm2.17a  42951  hbt  43121  fmul01lt1lem1  45580  sumnnodd  45626  itgspltprt  45975  stoweidlem20  46016  stoweidlem26  46022  fzopredsuc  47319  smonoord  47352  lighneallem4a  47589