MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1le1 Structured version   Visualization version   GIF version

Theorem 1le1 11791
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
StepHypRef Expression
1 1re 11163 . 2 1 ∈ ℝ
21leidi 11697 1 1 ≤ 1
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 5109  1c1 11060  cle 11198
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-mulcl 11121  ax-mulrcl 11122  ax-i2m1 11127  ax-1ne0 11128  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-er 8654  df-en 8890  df-dom 8891  df-sdom 8892  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203
This theorem is referenced by:  nnge1  12189  1elunit  13396  fldiv4p1lem1div2  13749  expge1  14014  leexp1a  14089  bernneq  14141  faclbnd3  14201  facubnd  14209  hashsnle1  14326  wrdlen1  14451  wrdl1exs1  14510  fprodge1  15886  cos1bnd  16077  sincos1sgn  16083  eirrlem  16094  xrhmeo  24332  pcoval2  24402  pige3ALT  25899  cxplea  26074  cxple2a  26077  cxpaddlelem  26127  abscxpbnd  26129  mule1  26520  sqff1o  26554  logfacbnd3  26594  logexprlim  26596  dchrabs2  26633  bposlem5  26659  zabsle1  26667  lgslem2  26669  lgsfcl2  26674  lgseisen  26750  dchrisum0flblem1  26879  log2sumbnd  26915  clwwlknon1le1  29094  nmopun  31005  branmfn  31096  stge1i  31229  dstfrvunirn  33138  subfaclim  33846  sticksstones12a  40615  jm2.17a  41331  jm2.17b  41332  fmuldfeq  43914  stoweidlem3  44334  stoweidlem18  44349  sepfsepc  47050  seppcld  47052
  Copyright terms: Public domain W3C validator