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

Theorem 0lt1 10136
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 9642 . . 3  |-  1  e.  RR
2 ax-1ne0 9608 . . 3  |-  1  =/=  0
3 msqgt0 10134 . . 3  |-  ( ( 1  e.  RR  /\  1  =/=  0 )  -> 
0  <  ( 1  x.  1 ) )
41, 2, 3mp2an 678 . 2  |-  0  <  ( 1  x.  1 )
5 ax-1cn 9597 . . 3  |-  1  e.  CC
65mulid1i 9645 . 2  |-  ( 1  x.  1 )  =  1
74, 6breqtri 4426 1  |-  0  <  1
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1887    =/= wne 2622   class class class wbr 4402  (class class class)co 6290   RRcr 9538   0cc0 9539   1c1 9540    x. cmul 9544    < clt 9675
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-po 4755  df-so 4756  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863
This theorem is referenced by:  0le1  10137  eqneg  10327  elimgt0  10441  ltp1  10443  ltm1  10445  recgt0  10449  mulgt1  10464  reclt1  10501  recgt1  10502  recgt1i  10503  recp1lt1  10504  recreclt  10505  recgt0ii  10512  inelr  10599  nnge1  10635  nngt0  10638  0nnn  10641  nnrecgt0  10647  2pos  10701  3pos  10703  4pos  10705  5pos  10707  6pos  10708  7pos  10709  8pos  10710  9pos  10711  10pos  10712  neg1lt0  10716  halflt1  10831  nn0p1gt0  10899  elnnnn0c  10915  elnnz1  10963  nn0lt10b  10998  recnz  11011  1rp  11306  xmulid1  11565  0nelfz1  11818  fz10  11820  fzpreddisj  11845  elfz1b  11864  elfznelfzob  12015  1mod  12129  expgt1  12310  ltexp2a  12324  expcan  12325  ltexp2  12326  leexp2  12327  leexp2a  12328  expnbnd  12401  expnlbnd  12402  expnlbnd2  12403  expmulnbnd  12404  discr1  12408  bcn1  12498  hashnn0n0nn  12570  brfi1indALT  12653  s2fv0  12981  swrd2lsw  13027  2swrd2eqwrdeq  13028  sgn1  13155  resqrex  13314  mulcn2  13659  cvgrat  13939  bpoly4  14112  cos1bnd  14241  sin01gt0  14244  sincos1sgn  14247  ruclem8  14289  sadcadd  14432  divdenle  14698  43prm  15093  ipostr  16399  srgbinomlem4  17776  abvtrivd  18068  gzrngunit  19033  znidomb  19132  psgnodpmr  19158  thlle  19260  leordtval2  20228  mopnex  21534  dscopn  21588  metnrmlem1a  21875  metnrmlem1aOLD  21890  xrhmph  21975  evth  21987  xlebnum  21996  vitalilem5  22570  vitali  22571  ply1remlem  23113  plyremlem  23257  plyrem  23258  vieta1lem2  23264  reeff1olem  23401  sinhalfpilem  23418  rplogcl  23553  logtayllem  23604  cxplt  23639  cxple  23640  atanlogaddlem  23839  ressatans  23860  rlimcnp  23891  rlimcnp2  23892  cxp2limlem  23901  cxp2lim  23902  cxploglim2  23904  amgmlem  23915  emcllem2  23922  harmonicubnd  23935  fsumharmonic  23937  zetacvg  23940  ftalem1  23997  ftalem2  23998  chpchtsum  24147  chpub  24148  mersenne  24155  perfectlem2  24158  efexple  24209  chebbnd1  24310  dchrmusumlema  24331  dchrvmasumlem2  24336  dchrvmasumiflem1  24339  dchrisum0flblem2  24347  dchrisum0lema  24352  dchrisum0lem1  24354  dchrisum0lem2a  24355  mulog2sumlem1  24372  chpdifbndlem1  24391  chpdifbnd  24393  selberg3lem1  24395  pntrmax  24402  pntrsumo1  24403  pntpbnd1a  24423  pntpbnd2  24425  pntibndlem1  24427  pntlem3  24447  pnt  24452  ostth2lem1  24456  ostth2lem3  24473  ostth2lem4  24474  axcontlem2  24995  spthispth  25303  usgrcyclnl1  25368  clwwlkf1  25524  esumcst  28884  hasheuni  28906  ballotlemi1  29335  ballotlemic  29339  ballotlemi1OLD  29373  ballotlemicOLD  29377  sgnnbi  29416  sgnpbi  29417  sgnmulsgp  29421  signsply0  29440  signswch  29450  poimirlem22  31962  poimirlem31  31971  asindmre  32027  areacirclem4  32035  pellexlem2  35674  pellexlem6  35678  pell14qrgt0  35705  elpell1qr2  35718  pellfundex  35734  pellfundrp  35736  rmxypos  35797  relexp01min  36305  imo72b2  36619  isprm7  36660  radcnvrat  36663  sumnnodd  37710  dvnmul  37818  stoweidlem7  37867  stoweidlem36  37897  stoweidlem38  37899  stoweidlem42  37903  stoweidlem51  37912  stoweidlem59  37920  stirlinglem5  37940  stirlinglem7  37942  stirlinglem10  37945  stirlinglem11  37946  stirlinglem12  37947  stirlinglem15  37950  dirkeritg  37964  fourierdlem11  37980  fourierdlem30  37999  fourierdlem47  38017  fourierdlem79  38049  fourierdlem103  38073  fourierdlem104  38074  fouriersw  38095  etransclem4  38103  etransclem31  38130  etransclem32  38131  etransclem35  38134  etransclem41  38140  salexct2  38198  hoidmvlelem1  38417  m1mod0mod1  38723  divlt1lt  40363  m1modmmod  40377  regt1loggt0  40400  rege1logbrege0  40422  nnlog2ge0lt1  40430
  Copyright terms: Public domain W3C validator