Theorem 1le1 11842

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 11208	. 2 ⊢ 1 ∈ ℝ
2	1	leidi 11748	1 ⊢ 1 ≤ 1

Syntax hints:   class class class wbr 5111  1c1 11101   ≤ cle 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-mulcl 11162  ax-mulrcl 11163  ax-i2m1 11168  ax-1ne0 11169  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-er 8694  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249

This theorem is referenced by:  nnge1  12264  1elunit  13497  fldiv4p1lem1div2  13868  expge1  14135  leexp1a  14211  bernneq  14265  faclbnd3  14328  facubnd  14336  hashsnle1  14454  wrdlen1  14591  wrdl1exs1  14651  fprodge1  16049  cos1bnd  16243  sincos1sgn  16249  eirrlem  16260  psdmvr  22301  xrhmeo  25074  pcoval2  25144  pige3ALT  26651  cxplea  26827  cxple2a  26830  cxpaddlelem  26882  abscxpbnd  26884  mule1  27278  sqff1o  27312  logfacbnd3  27353  logexprlim  27355  dchrabs2  27392  bposlem5  27418  zabsle1  27426  lgslem2  27428  lgsfcl2  27433  lgseisen  27509  dchrisum0flblem1  27638  log2sumbnd  27674  clwwlknon1le1  30393  nmopun  32307  branmfn  32398  stge1i  32531  dstfrvunirn  34810  subfaclim  35613  sticksstones12a  42849  jm2.17a  43614  jm2.17b  43615  fmuldfeq  46226  stoweidlem3  46644  stoweidlem18  46659  ceilhalfnn  48001  m1modne  48015  sepfsepc  49626  seppcld  49628