Theorem lep1d 12163

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5111  (class class class)co 7419  ℝcr 11116  1c1 11118   + caddc 11120   ≤ cle 11261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-mulcom 11181  ax-addass 11182  ax-mulass 11183  ax-distr 11184  ax-i2m1 11185  ax-1ne0 11186  ax-1rid 11187  ax-rnegex 11188  ax-rrecex 11189  ax-cnre 11190  ax-pre-lttri 11191  ax-pre-lttrn 11192  ax-pre-ltadd 11193  ax-pre-mulgt0 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266  df-sub 11460  df-neg 11461

This theorem is used by:  fzossfzop1  13791  modltm1p1mod  13979  facubnd  14356  swrds2  15003  lo1bddrp  15602  mulcn2  15673  harmonic  15938  expcnv  15943  prmfac1  16803  eulerthlem2  16865  telgsumfzs  20105  nlmvscnlem2  24895  nghmcn  24955  ipcnlem2  25456  ovolicc2lem3  25731  ovolicopnf  25736  dyadf  25803  dyadovol  25805  dyadmaxlem  25809  volsup2  25817  mbfi1fseqlem5  25931  itg2gt0  25972  itg2cnlem1  25973  dvfsumle  26233  dvfsumabs  26235  dvfsumlem3  26240  leibpi  27160  efrlim  27187  zetacvg  27232  lgamgulmlem3  27248  lgamgulmlem5  27250  basellem2  27299  basellem3  27300  basellem5  27302  basellem6  27303  ppip1le  27378  bcmono  27494  rplogsumlem2  27702  dchrisumlem1  27706  dchrisumlem2  27707  dchrisumlem3  27708  selberg2lem  27767  logdivbnd  27773  pntrlog2bndlem2  27795  pntrlog2bndlem5  27798  pntlemk  27823  pntleml  27828  crctcshwlkn0lem3  30230  crctcshwlkn0lem5  30232  wwlksnred  30310  wwlksnextproplem1  30327  wwlksnextproplem2  30328  wwlksnextproplem3  30329  clwlkclwwlkf1lem2  30425  clwwlkf  30467  clwwlkf1  30469  wwlksubclwwlk  30478  eupth2lems  30662  numclwlk2lem2f  30801  pmtrto1cl  33485  psgnfzto1stlem  33486  fzto1st  33489  psgnfzto1st  33491  constrresqrtcl  34233  sxbrsigalem2  34743  dstfrvclim1  34935  fsum2dsub  35061  breprexplemc  35086  poimirlem7  38337  poimirlem15  38345  rrntotbnd  38547  aks4d1p1p7  42901  aks4d1p1p5  42902  aks4d1p1  42903  2np3bcnp1  42971  sticksstones6  42978  sticksstones7  42979  sticksstones10  42982  sticksstones12a  42984  sticksstones12  42985  sticksstones22  42995  jm2.17a  43747  hbt  43917  fmul01lt1lem1  46360  sumnnodd  46406  itgspltprt  46753  stoweidlem20  46794  stoweidlem26  46800  fzopredsuc  48121  smonoord  48174  lighneallem4a  48420