Theorem 1le1 11894

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

Syntax hints:   class class class wbr 5154  1c1 11161   ≤ cle 11301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7749  ax-resscn 11217  ax-1cn 11218  ax-icn 11219  ax-addcl 11220  ax-mulcl 11222  ax-mulrcl 11223  ax-i2m1 11228  ax-1ne0 11229  ax-rrecex 11232  ax-cnre 11233  ax-pre-lttri 11234

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-sbc 3788  df-csb 3904  df-dif 3961  df-un 3963  df-in 3965  df-ss 3975  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4917  df-br 5155  df-opab 5217  df-mpt 5238  df-id 5582  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6509  df-fun 6559  df-fn 6560  df-f 6561  df-f1 6562  df-fo 6563  df-f1o 6564  df-fv 6565  df-ov 7431  df-er 8739  df-en 8980  df-dom 8981  df-sdom 8982  df-pnf 11302  df-mnf 11303  df-xr 11304  df-ltxr 11305  df-le 11306

This theorem is referenced by:  nnge1  12297  1elunit  13506  fldiv4p1lem1div2  13861  expge1  14125  leexp1a  14200  bernneq  14253  faclbnd3  14316  facubnd  14324  hashsnle1  14441  wrdlen1  14576  wrdl1exs1  14635  fprodge1  16011  cos1bnd  16203  sincos1sgn  16209  eirrlem  16220  xrhmeo  24963  pcoval2  25035  pige3ALT  26545  cxplea  26721  cxple2a  26724  cxpaddlelem  26777  abscxpbnd  26779  mule1  27174  sqff1o  27208  logfacbnd3  27250  logexprlim  27252  dchrabs2  27289  bposlem5  27315  zabsle1  27323  lgslem2  27325  lgsfcl2  27330  lgseisen  27406  dchrisum0flblem1  27535  log2sumbnd  27571  clwwlknon1le1  30077  nmopun  31990  branmfn  32081  stge1i  32214  dstfrvunirn  34385  subfaclim  35102  sticksstones12a  41942  jm2.17a  42733  jm2.17b  42734  fmuldfeq  45318  stoweidlem3  45738  stoweidlem18  45753  sepfsepc  48386  seppcld  48388