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

Theorem 0lt1 9443
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 8984 . . 3  |-  1  e.  RR
2 ax-1ne0 8953 . . 3  |-  1  =/=  0
3 msqgt0 9441 . . 3  |-  ( ( 1  e.  RR  /\  1  =/=  0 )  -> 
0  <  ( 1  x.  1 ) )
41, 2, 3mp2an 653 . 2  |-  0  <  ( 1  x.  1 )
5 ax-1cn 8942 . . 3  |-  1  e.  CC
65mulid1i 8986 . 2  |-  ( 1  x.  1 )  =  1
74, 6breqtri 4148 1  |-  0  <  1
Colors of variables: wff set class
Syntax hints:    e. wcel 1715    =/= wne 2529   class class class wbr 4125  (class class class)co 5981   RRcr 8883   0cc0 8884   1c1 8885    x. cmul 8889    < clt 9014
This theorem is referenced by:  0le1  9444  eqneg  9627  elimgt0  9739  ltp1  9741  ltm1  9743  recgt0  9747  mulgt1  9762  reclt1  9798  recgt1  9799  recgt1i  9800  recp1lt1  9801  recreclt  9802  recgt0ii  9809  inelr  9883  nnge1  9919  nngt0  9922  0nnn  9924  nnrecgt0  9930  2pos  9975  3pos  9977  4pos  9979  5pos  9980  6pos  9981  7pos  9982  8pos  9983  9pos  9984  10pos  9985  halflt1  10082  elnnnn0c  10158  elnnz1  10200  recnz  10238  1rp  10509  xmulid1  10751  fz10  10967  elfznelfzob  11080  1mod  11160  expgt1  11305  ltexp2a  11318  expcan  11319  ltexp2  11320  leexp2  11321  leexp2a  11322  expnbnd  11395  expnlbnd  11396  expnlbnd2  11397  expmulnbnd  11398  discr1  11402  bcn1  11491  hashnn0n0nn  11551  brfi1uzind  11602  s2fv0  11736  resqrex  11943  mulcn2  12276  cvgrat  12547  cos1bnd  12675  sin01gt0  12678  sincos1sgn  12681  ruclem8  12723  nthruz  12738  sadcadd  12857  divdenle  13028  43prm  13331  ipostr  14466  abvtrivd  15815  gzrngunit  16654  znidomb  16732  thlle  16814  leordtval2  17159  mopnex  18278  dscopn  18309  metnrmlem1a  18576  xrhmph  18660  evth  18672  xlebnum  18678  vitalilem4  19181  vitalilem5  19182  vitali  19183  ply1remlem  19763  plyremlem  19899  plyrem  19900  vieta1lem2  19906  reeff1olem  20040  sinhalfpilem  20052  rplogcl  20177  logtayllem  20228  cxplt  20263  cxple  20264  atanre  20403  atanlogaddlem  20431  ressatans  20452  rlimcnp  20482  rlimcnp2  20483  cxp2limlem  20492  cxp2lim  20493  cxploglim2  20495  amgmlem  20506  emcllem2  20513  harmonicubnd  20526  fsumharmonic  20528  ftalem1  20533  ftalem2  20534  chpchtsum  20681  chpub  20682  mersenne  20689  perfectlem2  20692  efexple  20743  lgsdir2lem3  20787  chebbnd1  20844  dchrmusumlema  20865  dchrvmasumlem2  20870  dchrvmasumiflem1  20873  dchrisum0flblem2  20881  dchrisum0lema  20886  dchrisum0lem1  20888  dchrisum0lem2a  20889  mulog2sumlem1  20906  chpdifbndlem1  20925  chpdifbnd  20927  selberg3lem1  20929  pntrmax  20936  pntrsumo1  20937  pntpbnd1a  20957  pntpbnd2  20959  pntibndlem1  20961  pntlem3  20981  pnt  20986  ostth2lem1  20990  ostth2lem3  21007  ostth2lem4  21008  esumcst  23920  hasheuni  23940  ballotlemi1  24208  ballotlemic  24212  ballotlem1c  24213  zetacvg  24247  fz0n  24686  risefall0lem  24814  axcontlem2  25335  bpoly4  25536  areacirclem5  25704  pellexlem2  26421  pellexlem6  26425  pell14qrgt0  26450  elpell1qr2  26463  pellfundex  26477  pellfundrp  26479  rmxypos  26540  stoweidlem7  27262  stoweidlem34  27289  stoweidlem36  27291  stoweidlem38  27293  stoweidlem42  27297  stoweidlem44  27299  stoweidlem51  27306  stoweidlem59  27314  stirlinglem5  27333  stirlinglem6  27334  stirlinglem7  27335  stirlinglem10  27338  stirlinglem11  27339  stirlinglem12  27340  stirlinglem15  27343  spthispth  27717  usgrcyclnl1  27766  sgn1  27951
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-13 1717  ax-14 1719  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347  ax-sep 4243  ax-nul 4251  ax-pow 4290  ax-pr 4316  ax-un 4615  ax-resscn 8941  ax-1cn 8942  ax-icn 8943  ax-addcl 8944  ax-addrcl 8945  ax-mulcl 8946  ax-mulrcl 8947  ax-mulcom 8948  ax-addass 8949  ax-mulass 8950  ax-distr 8951  ax-i2m1 8952  ax-1ne0 8953  ax-1rid 8954  ax-rnegex 8955  ax-rrecex 8956  ax-cnre 8957  ax-pre-lttri 8958  ax-pre-lttrn 8959  ax-pre-ltadd 8960  ax-pre-mulgt0 8961
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 936  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-eu 2221  df-mo 2222  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-nel 2532  df-ral 2633  df-rex 2634  df-reu 2635  df-rab 2637  df-v 2875  df-sbc 3078  df-csb 3168  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-pw 3716  df-sn 3735  df-pr 3736  df-op 3738  df-uni 3930  df-br 4126  df-opab 4180  df-mpt 4181  df-id 4412  df-po 4417  df-so 4418  df-xp 4798  df-rel 4799  df-cnv 4800  df-co 4801  df-dm 4802  df-rn 4803  df-res 4804  df-ima 4805  df-iota 5322  df-fun 5360  df-fn 5361  df-f 5362  df-f1 5363  df-fo 5364  df-f1o 5365  df-fv 5366  df-ov 5984  df-oprab 5985  df-mpt2 5986  df-riota 6446  df-er 6802  df-en 7007  df-dom 7008  df-sdom 7009  df-pnf 9016  df-mnf 9017  df-xr 9018  df-ltxr 9019  df-le 9020  df-sub 9186  df-neg 9187
  Copyright terms: Public domain W3C validator