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

Theorem 0lt1 9858
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 9381 . . 3  |-  1  e.  RR
2 ax-1ne0 9347 . . 3  |-  1  =/=  0
3 msqgt0 9856 . . 3  |-  ( ( 1  e.  RR  /\  1  =/=  0 )  -> 
0  <  ( 1  x.  1 ) )
41, 2, 3mp2an 667 . 2  |-  0  <  ( 1  x.  1 )
5 ax-1cn 9336 . . 3  |-  1  e.  CC
65mulid1i 9384 . 2  |-  ( 1  x.  1 )  =  1
74, 6breqtri 4312 1  |-  0  <  1
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761    =/= wne 2604   class class class wbr 4289  (class class class)co 6090   RRcr 9277   0cc0 9278   1c1 9279    x. cmul 9283    < clt 9414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-po 4637  df-so 4638  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594
This theorem is referenced by:  0le1  9859  eqneg  10047  elimgt0  10161  ltp1  10163  ltm1  10165  recgt0  10169  mulgt1  10184  reclt1  10223  recgt1  10224  recgt1i  10225  recp1lt1  10226  recreclt  10227  recgt0ii  10234  inelr  10308  nnge1  10344  nngt0  10347  0nnn  10349  nnrecgt0  10355  2pos  10409  3pos  10411  4pos  10413  5pos  10415  6pos  10416  7pos  10417  8pos  10418  9pos  10419  10pos  10420  neg1lt0  10424  halflt1  10539  nn0p1gt0  10605  elnnnn0c  10621  elnnz1  10668  recnz  10713  1rp  10991  xmulid1  11238  fz10  11466  fzpreddisj  11500  elfz1b  11523  elfznelfzob  11627  1mod  11736  expgt1  11898  ltexp2a  11911  expcan  11912  ltexp2  11913  leexp2  11914  leexp2a  11915  expnbnd  11989  expnlbnd  11990  expnlbnd2  11991  expmulnbnd  11992  discr1  11996  bcn1  12085  hashnn0n0nn  12149  brfi1uzind  12215  ccatws1n0  12306  s2fv0  12508  swrd2lsw  12548  2swrd2eqwrdeq  12549  sgn1  12577  resqrex  12736  mulcn2  13069  cvgrat  13339  cos1bnd  13467  sin01gt0  13470  sincos1sgn  13473  ruclem8  13515  sadcadd  13650  divdenle  13823  43prm  14145  ipostr  15319  srgbinomlem4  16631  abvtrivd  16905  gzrngunit  17837  znidomb  17953  psgnodpmr  17979  thlle  18081  leordtval2  18775  mopnex  20053  dscopn  20125  metnrmlem1a  20393  xrhmph  20478  evth  20490  xlebnum  20496  vitalilem5  21051  vitali  21052  ply1remlem  21593  plyremlem  21729  plyrem  21730  vieta1lem2  21736  reeff1olem  21870  sinhalfpilem  21884  rplogcl  22012  logtayllem  22063  cxplt  22098  cxple  22099  atanlogaddlem  22267  ressatans  22288  rlimcnp  22318  rlimcnp2  22319  cxp2limlem  22328  cxp2lim  22329  cxploglim2  22331  amgmlem  22342  emcllem2  22349  harmonicubnd  22362  fsumharmonic  22364  ftalem1  22369  ftalem2  22370  chpchtsum  22517  chpub  22518  mersenne  22525  perfectlem2  22528  efexple  22579  chebbnd1  22680  dchrmusumlema  22701  dchrvmasumlem2  22706  dchrvmasumiflem1  22709  dchrisum0flblem2  22717  dchrisum0lema  22722  dchrisum0lem1  22724  dchrisum0lem2a  22725  mulog2sumlem1  22742  chpdifbndlem1  22761  chpdifbnd  22763  selberg3lem1  22765  pntrmax  22772  pntrsumo1  22773  pntpbnd1a  22793  pntpbnd2  22795  pntibndlem1  22797  pntlem3  22817  pnt  22822  ostth2lem1  22826  ostth2lem3  22843  ostth2lem4  22844  axcontlem2  23146  spthispth  23407  usgrcyclnl1  23461  esumcst  26450  hasheuni  26470  ballotlemi1  26815  ballotlemic  26819  sgnnbi  26858  sgnpbi  26859  sgnsgn  26861  sgnmulsgp  26863  signsply0  26882  signswch  26892  zetacvg  26931  bpoly4  28131  asindmre  28404  areacirclem4  28412  pellexlem2  29096  pellexlem6  29100  pell14qrgt0  29125  elpell1qr2  29138  pellfundex  29152  pellfundrp  29154  rmxypos  29215  stoweidlem7  29727  stoweidlem36  29756  stoweidlem38  29758  stoweidlem42  29762  stoweidlem51  29771  stoweidlem59  29779  stirlinglem5  29798  stirlinglem7  29800  stirlinglem10  29803  stirlinglem11  29804  stirlinglem12  29805  stirlinglem15  29808  elfzom1elp1fzo  30143  clwwlkf1  30383  rusgranumwlks  30499
  Copyright terms: Public domain W3C validator