Theorem lep1d 12141

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  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 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439

This theorem is referenced by:  fzossfzop1  13768  modltm1p1mod  13955  facubnd  14332  swrds2  14973  lo1bddrp  15572  mulcn2  15643  harmonic  15909  expcnv  15914  prmfac1  16774  eulerthlem2  16836  telgsumfzs  20054  nlmvscnlem2  24842  nghmcn  24902  ipcnlem2  25403  ovolicc2lem3  25678  ovolicopnf  25683  dyadf  25750  dyadovol  25752  dyadmaxlem  25756  volsup2  25764  mbfi1fseqlem5  25878  itg2gt0  25919  itg2cnlem1  25920  dvfsumle  26180  dvfsumabs  26182  dvfsumlem3  26187  leibpi  27107  efrlim  27134  zetacvg  27179  lgamgulmlem3  27195  lgamgulmlem5  27197  basellem2  27246  basellem3  27247  basellem5  27249  basellem6  27250  ppip1le  27325  bcmono  27441  rplogsumlem2  27649  dchrisumlem1  27653  dchrisumlem2  27654  dchrisumlem3  27655  selberg2lem  27714  logdivbnd  27720  pntrlog2bndlem2  27742  pntrlog2bndlem5  27745  pntlemk  27770  pntleml  27775  crctcshwlkn0lem3  30161  crctcshwlkn0lem5  30163  wwlksnred  30241  wwlksnextproplem1  30258  wwlksnextproplem2  30259  wwlksnextproplem3  30260  clwlkclwwlkf1lem2  30356  clwwlkf  30398  clwwlkf1  30400  wwlksubclwwlk  30409  eupth2lems  30589  numclwlk2lem2f  30728  pmtrto1cl  33419  psgnfzto1stlem  33420  fzto1st  33423  psgnfzto1st  33425  constrresqrtcl  34167  sxbrsigalem2  34676  dstfrvclim1  34868  fsum2dsub  34994  breprexplemc  35019  poimirlem7  38298  poimirlem15  38306  rrntotbnd  38507  aks4d1p1p7  42861  aks4d1p1p5  42862  aks4d1p1  42863  2np3bcnp1  42931  sticksstones6  42938  sticksstones7  42939  sticksstones10  42942  sticksstones12a  42944  sticksstones12  42945  sticksstones22  42955  jm2.17a  43707  hbt  43877  fmul01lt1lem1  46320  sumnnodd  46366  itgspltprt  46713  stoweidlem20  46754  stoweidlem26  46760  fzopredsuc  48081  smonoord  48134  lighneallem4a  48380