Theorem 1le1 11838

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

Syntax hints:   class class class wbr 5110  1c1 11097   ≤ cle 11240

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 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-mulcl 11158  ax-mulrcl 11159  ax-i2m1 11164  ax-1ne0 11165  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170

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 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7411  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245

This theorem is referenced by:  nnge1  12260  1elunit  13493  fldiv4p1lem1div2  13864  expge1  14131  leexp1a  14207  bernneq  14261  faclbnd3  14324  facubnd  14332  hashsnle1  14450  wrdlen1  14587  wrdl1exs1  14647  fprodge1  16045  cos1bnd  16239  sincos1sgn  16245  eirrlem  16256  psdmvr  22297  xrhmeo  25070  pcoval2  25140  pige3ALT  26647  cxplea  26823  cxple2a  26826  cxpaddlelem  26878  abscxpbnd  26880  mule1  27274  sqff1o  27308  logfacbnd3  27349  logexprlim  27351  dchrabs2  27388  bposlem5  27414  zabsle1  27422  lgslem2  27424  lgsfcl2  27429  lgseisen  27505  dchrisum0flblem1  27634  log2sumbnd  27670  clwwlknon1le1  30389  nmopun  32303  branmfn  32394  stge1i  32527  dstfrvunirn  34806  subfaclim  35575  sticksstones12a  42809  jm2.17a  43574  jm2.17b  43575  fmuldfeq  46186  stoweidlem3  46604  stoweidlem18  46619  ceilhalfnn  47961  m1modne  47975  sepfsepc  49586  seppcld  49588