ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0le1 Unicode version

Theorem 0le1 8412
Description: 0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015.)
Assertion
Ref Expression
0le1  |-  0  <_  1

Proof of Theorem 0le1
StepHypRef Expression
1 0re 7932 . 2  |-  0  e.  RR
2 1re 7931 . 2  |-  1  e.  RR
3 0lt1 8058 . 2  |-  0  <  1
41, 2, 3ltleii 8034 1  |-  0  <_  1
Colors of variables: wff set class
Syntax hints:   class class class wbr 3998   0cc0 7786   1c1 7787    <_ cle 7967
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530  ax-cnex 7877  ax-resscn 7878  ax-1re 7880  ax-addrcl 7883  ax-0lt1 7892  ax-rnegex 7895  ax-pre-ltirr 7898  ax-pre-lttrn 7900
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-nel 2441  df-ral 2458  df-rex 2459  df-rab 2462  df-v 2737  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-br 3999  df-opab 4060  df-xp 4626  df-cnv 4628  df-pnf 7968  df-mnf 7969  df-xr 7970  df-ltxr 7971  df-le 7972
This theorem is referenced by:  lemulge11  8794  sup3exmid  8885  0le2  8980  1eluzge0  9545  0elunit  9955  1elunit  9956  fldiv4p1lem1div2  10273  q1mod  10324  expge0  10524  expge1  10525  faclbnd3  10689  sqrt1  11022  sqrt2gt1lt2  11025  abs1  11048  cvgratnnlembern  11498  fprodge0  11612  fprodge1  11614  ege2le3  11646  sinbnd  11727  cosbnd  11728  cos2bnd  11735  nn0oddm1d2  11880  flodddiv4  11905  sqnprm  12102  isprm5lem  12107  sqrt2irrap  12146  nn0sqrtelqelz  12172  pythagtriplem3  12233  sinhalfpilem  13705  zabsle1  13893  lgslem2  13895  lgsfcl2  13900  lgsdir2lem1  13922  lgsne0  13932  lgsdinn0  13942  trilpolemclim  14267  trilpolemlt1  14272  nconstwlpolemgt0  14294
  Copyright terms: Public domain W3C validator