Theorem lep1d 12123

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

Syntax hints:   → wi 4   ∈ wcel 2142   class class class wbr 5100  (class class class)co 7396  ℝcr 11072  1c1 11074   + caddc 11076   ≤ cle 11217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-po 5555  df-so 5556  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-er 8678  df-en 8928  df-dom 8929  df-sdom 8930  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417

This theorem is referenced by:  fzossfzop1  13749  modltm1p1mod  13936  facubnd  14313  swrds2  14953  lo1bddrp  15552  mulcn2  15623  harmonic  15889  expcnv  15894  prmfac1  16755  eulerthlem2  16817  telgsumfzs  20029  nlmvscnlem2  24745  nghmcn  24805  ipcnlem2  25306  ovolicc2lem3  25581  ovolicopnf  25586  dyadf  25653  dyadovol  25655  dyadmaxlem  25659  volsup2  25667  mbfi1fseqlem5  25781  itg2gt0  25822  itg2cnlem1  25823  dvfsumle  26083  dvfsumabs  26085  dvfsumlem3  26090  leibpi  27007  efrlim  27034  zetacvg  27079  lgamgulmlem3  27095  lgamgulmlem5  27097  basellem2  27146  basellem3  27147  basellem5  27149  basellem6  27150  ppip1le  27225  bcmono  27341  rplogsumlem2  27549  dchrisumlem1  27553  dchrisumlem2  27554  dchrisumlem3  27555  selberg2lem  27614  logdivbnd  27620  pntrlog2bndlem2  27642  pntrlog2bndlem5  27645  pntlemk  27670  pntleml  27675  crctcshwlkn0lem3  30012  crctcshwlkn0lem5  30014  wwlksnred  30092  wwlksnextproplem1  30109  wwlksnextproplem2  30110  wwlksnextproplem3  30111  clwlkclwwlkf1lem2  30207  clwwlkf  30249  clwwlkf1  30251  wwlksubclwwlk  30260  eupth2lems  30440  numclwlk2lem2f  30579  pmtrto1cl  33279  psgnfzto1stlem  33280  fzto1st  33283  psgnfzto1st  33285  constrresqrtcl  34074  sxbrsigalem2  34583  dstfrvclim1  34775  fsum2dsub  34901  breprexplemc  34926  poimirlem7  38126  poimirlem15  38134  rrntotbnd  38335  aks4d1p1p7  42691  aks4d1p1p5  42692  aks4d1p1  42693  2np3bcnp1  42761  sticksstones6  42768  sticksstones7  42769  sticksstones10  42772  sticksstones12a  42774  sticksstones12  42775  sticksstones22  42785  jm2.17a  43537  hbt  43707  fmul01lt1lem1  46160  sumnnodd  46206  itgspltprt  46553  stoweidlem20  46594  stoweidlem26  46600  fzopredsuc  47918  smonoord  47971  lighneallem4a  48217