MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0lt1 Structured version   Unicode version

Theorem 0lt1 9874
Description: 0 is less than 1. Theorem I.21 of [Apostol] p. 20. (Contributed by NM, 17-Jan-1997.)
Assertion
Ref Expression
0lt1  |-  0  <  1

Proof of Theorem 0lt1
StepHypRef Expression
1 1re 9397 . . 3  |-  1  e.  RR
2 ax-1ne0 9363 . . 3  |-  1  =/=  0
3 msqgt0 9872 . . 3  |-  ( ( 1  e.  RR  /\  1  =/=  0 )  -> 
0  <  ( 1  x.  1 ) )
41, 2, 3mp2an 672 . 2  |-  0  <  ( 1  x.  1 )
5 ax-1cn 9352 . . 3  |-  1  e.  CC
65mulid1i 9400 . 2  |-  ( 1  x.  1 )  =  1
74, 6breqtri 4327 1  |-  0  <  1
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756    =/= wne 2618   class class class wbr 4304  (class class class)co 6103   RRcr 9293   0cc0 9294   1c1 9295    x. cmul 9299    < clt 9430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384  ax-resscn 9351  ax-1cn 9352  ax-icn 9353  ax-addcl 9354  ax-addrcl 9355  ax-mulcl 9356  ax-mulrcl 9357  ax-mulcom 9358  ax-addass 9359  ax-mulass 9360  ax-distr 9361  ax-i2m1 9362  ax-1ne0 9363  ax-1rid 9364  ax-rnegex 9365  ax-rrecex 9366  ax-cnre 9367  ax-pre-lttri 9368  ax-pre-lttrn 9369  ax-pre-ltadd 9370  ax-pre-mulgt0 9371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-nel 2621  df-ral 2732  df-rex 2733  df-reu 2734  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-po 4653  df-so 4654  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438  df-riota 6064  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-er 7113  df-en 7323  df-dom 7324  df-sdom 7325  df-pnf 9432  df-mnf 9433  df-xr 9434  df-ltxr 9435  df-le 9436  df-sub 9609  df-neg 9610
This theorem is referenced by:  0le1  9875  eqneg  10063  elimgt0  10177  ltp1  10179  ltm1  10181  recgt0  10185  mulgt1  10200  reclt1  10239  recgt1  10240  recgt1i  10241  recp1lt1  10242  recreclt  10243  recgt0ii  10250  inelr  10324  nnge1  10360  nngt0  10363  0nnn  10365  nnrecgt0  10371  2pos  10425  3pos  10427  4pos  10429  5pos  10431  6pos  10432  7pos  10433  8pos  10434  9pos  10435  10pos  10436  neg1lt0  10440  halflt1  10555  nn0p1gt0  10621  elnnnn0c  10637  elnnz1  10684  recnz  10729  1rp  11007  xmulid1  11254  fz10  11482  fzpreddisj  11516  elfz1b  11539  elfznelfzob  11643  1mod  11752  expgt1  11914  ltexp2a  11927  expcan  11928  ltexp2  11929  leexp2  11930  leexp2a  11931  expnbnd  12005  expnlbnd  12006  expnlbnd2  12007  expmulnbnd  12008  discr1  12012  bcn1  12101  hashnn0n0nn  12165  brfi1uzind  12231  ccatws1n0  12322  s2fv0  12524  swrd2lsw  12564  2swrd2eqwrdeq  12565  sgn1  12593  resqrex  12752  mulcn2  13085  cvgrat  13355  cos1bnd  13483  sin01gt0  13486  sincos1sgn  13489  ruclem8  13531  sadcadd  13666  divdenle  13839  43prm  14161  ipostr  15335  srgbinomlem4  16653  abvtrivd  16937  gzrngunit  17890  znidomb  18006  psgnodpmr  18032  thlle  18134  leordtval2  18828  mopnex  20106  dscopn  20178  metnrmlem1a  20446  xrhmph  20531  evth  20543  xlebnum  20549  vitalilem5  21104  vitali  21105  ply1remlem  21646  plyremlem  21782  plyrem  21783  vieta1lem2  21789  reeff1olem  21923  sinhalfpilem  21937  rplogcl  22065  logtayllem  22116  cxplt  22151  cxple  22152  atanlogaddlem  22320  ressatans  22341  rlimcnp  22371  rlimcnp2  22372  cxp2limlem  22381  cxp2lim  22382  cxploglim2  22384  amgmlem  22395  emcllem2  22402  harmonicubnd  22415  fsumharmonic  22417  ftalem1  22422  ftalem2  22423  chpchtsum  22570  chpub  22571  mersenne  22578  perfectlem2  22581  efexple  22632  chebbnd1  22733  dchrmusumlema  22754  dchrvmasumlem2  22759  dchrvmasumiflem1  22762  dchrisum0flblem2  22770  dchrisum0lema  22775  dchrisum0lem1  22777  dchrisum0lem2a  22778  mulog2sumlem1  22795  chpdifbndlem1  22814  chpdifbnd  22816  selberg3lem1  22818  pntrmax  22825  pntrsumo1  22826  pntpbnd1a  22846  pntpbnd2  22848  pntibndlem1  22850  pntlem3  22870  pnt  22875  ostth2lem1  22879  ostth2lem3  22896  ostth2lem4  22897  axcontlem2  23223  spthispth  23484  usgrcyclnl1  23538  esumcst  26526  hasheuni  26546  ballotlemi1  26897  ballotlemic  26901  sgnnbi  26940  sgnpbi  26941  sgnsgn  26943  sgnmulsgp  26945  signsply0  26964  signswch  26974  zetacvg  27013  bpoly4  28214  asindmre  28491  areacirclem4  28499  pellexlem2  29183  pellexlem6  29187  pell14qrgt0  29212  elpell1qr2  29225  pellfundex  29239  pellfundrp  29241  rmxypos  29302  stoweidlem7  29814  stoweidlem36  29843  stoweidlem38  29845  stoweidlem42  29849  stoweidlem51  29858  stoweidlem59  29866  stirlinglem5  29885  stirlinglem7  29887  stirlinglem10  29890  stirlinglem11  29891  stirlinglem12  29892  stirlinglem15  29895  elfzom1elp1fzo  30230  clwwlkf1  30470  rusgranumwlks  30586
  Copyright terms: Public domain W3C validator