Theorem 1le1 11299

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

Syntax hints:   class class class wbr 5033  1c1 10569   ≤ cle 10707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-mulcl 10630  ax-mulrcl 10631  ax-i2m1 10636  ax-1ne0 10637  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712

This theorem is referenced by:  nnge1  11695  1elunit  12895  fldiv4p1lem1div2  13247  expge1  13509  leexp1a  13582  bernneq  13633  faclbnd3  13695  facubnd  13703  hashsnle1  13821  wrdlen1  13946  wrdl1exs1  14007  fprodge1  15390  cos1bnd  15581  sincos1sgn  15587  eirrlem  15598  xrhmeo  23640  pcoval2  23710  pige3ALT  25204  cxplea  25379  cxple2a  25382  cxpaddlelem  25432  abscxpbnd  25434  mule1  25825  sqff1o  25859  logfacbnd3  25899  logexprlim  25901  dchrabs2  25938  bposlem5  25964  zabsle1  25972  lgslem2  25974  lgsfcl2  25979  lgseisen  26055  dchrisum0flblem1  26184  log2sumbnd  26220  clwwlknon1le1  27978  nmopun  29889  branmfn  29980  stge1i  30113  dstfrvunirn  31953  subfaclim  32659  jm2.17a  40267  jm2.17b  40268  fmuldfeq  42584  stoweidlem3  43004  stoweidlem18  43019