Theorem 1le1 11740

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

Syntax hints:   class class class wbr 5086  1c1 11002   ≤ cle 11142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-mulcl 11063  ax-mulrcl 11064  ax-i2m1 11069  ax-1ne0 11070  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147

This theorem is referenced by:  nnge1  12148  1elunit  13365  fldiv4p1lem1div2  13734  expge1  14001  leexp1a  14077  bernneq  14131  faclbnd3  14194  facubnd  14202  hashsnle1  14319  wrdlen1  14456  wrdl1exs1  14516  fprodge1  15897  cos1bnd  16091  sincos1sgn  16097  eirrlem  16108  psdmvr  22079  xrhmeo  24866  pcoval2  24938  pige3ALT  26451  cxplea  26627  cxple2a  26630  cxpaddlelem  26683  abscxpbnd  26685  mule1  27080  sqff1o  27114  logfacbnd3  27156  logexprlim  27158  dchrabs2  27195  bposlem5  27221  zabsle1  27229  lgslem2  27231  lgsfcl2  27236  lgseisen  27312  dchrisum0flblem1  27441  log2sumbnd  27477  clwwlknon1le1  30073  nmopun  31986  branmfn  32077  stge1i  32210  dstfrvunirn  34480  subfaclim  35224  sticksstones12a  42190  jm2.17a  42993  jm2.17b  42994  fmuldfeq  45623  stoweidlem3  46041  stoweidlem18  46056  ceilhalfnn  47367  m1modne  47379  sepfsepc  48959  seppcld  48961