Theorem 1le1 11837

Description: One is less than or equal to one. (Contributed by David A. Wheeler, 16-Jul-2016.)

Assertion

Ref	Expression
1le1	⊢ 1 ≤ 1

Proof of Theorem 1le1

Step	Hyp	Ref	Expression
1		1re 11203	. 2 ⊢ 1 ∈ ℝ
2	1	leidi 11743	1 ⊢ 1 ≤ 1

Syntax hints:   class class class wbr 5109  1c1 11096   ≤ 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-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  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-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-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-ov 7413  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

This theorem is referenced by:  nnge1  12259  1elunit  13492  fldiv4p1lem1div2  13864  expge1  14131  leexp1a  14207  bernneq  14261  faclbnd3  14324  facubnd  14332  hashsnle1  14450  wrdlen1  14587  wrdl1exs1  14647  fprodge1  16045  cos1bnd  16238  sincos1sgn  16244  eirrlem  16255  psdmvr  22332  xrhmeo  25105  pcoval2  25175  pige3ALT  26685  cxplea  26861  cxple2a  26864  cxpaddlelem  26916  abscxpbnd  26918  mule1  27312  sqff1o  27346  logfacbnd3  27387  logexprlim  27389  dchrabs2  27426  bposlem5  27452  zabsle1  27460  lgslem2  27462  lgsfcl2  27467  lgseisen  27543  dchrisum0flblem1  27672  log2sumbnd  27708  clwwlknon1le1  30452  nmopun  32366  branmfn  32457  stge1i  32590  dstfrvunirn  34865  subfaclim  35680  sticksstones12a  42924  jm2.17a  43687  jm2.17b  43688  fmuldfeq  46299  stoweidlem3  46717  stoweidlem18  46732  ceilhalfnn  48077  m1modne  48091  sepfsepc  49706  seppcld  49708