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

Theorem 0lt1 10399
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 9895 . . 3 1 ∈ ℝ
2 ax-1ne0 9861 . . 3 1 ≠ 0
3 msqgt0 10397 . . 3 ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
41, 2, 3mp2an 703 . 2 0 < (1 · 1)
5 ax-1cn 9850 . . 3 1 ∈ ℂ
65mulid1i 9898 . 2 (1 · 1) = 1
74, 6breqtri 4602 1 0 < 1
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  wne 2779   class class class wbr 4577  (class class class)co 6527  cr 9791  0cc0 9792  1c1 9793   · cmul 9797   < clt 9930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120
This theorem is referenced by:  0le1  10400  eqneg  10594  elimgt0  10708  ltp1  10710  ltm1  10712  recgt0  10716  mulgt1  10731  reclt1  10767  recgt1  10768  recgt1i  10769  recp1lt1  10770  recreclt  10771  recgt0ii  10778  inelr  10857  nnge1  10893  nngt0  10896  0nnn  10899  nnrecgt0  10905  2pos  10959  3pos  10961  4pos  10963  5pos  10965  6pos  10966  7pos  10967  8pos  10968  9pos  10969  10posOLD  10970  neg1lt0  10974  halflt1  11097  nn0p1gt0  11169  elnnnn0c  11185  elnnz1  11236  nn0lt10b  11272  recnz  11284  1rp  11668  divlt1lt  11731  divle1le  11732  ledivge1le  11733  nnledivrp  11772  xmulid1  11938  0nelfz1  12186  fz10  12188  fzpreddisj  12215  elfz1b  12234  elfznelfzob  12395  1mod  12519  expgt1  12715  ltexp2a  12729  expcan  12730  ltexp2  12731  leexp2  12732  leexp2a  12733  expnbnd  12810  expnlbnd  12811  expnlbnd2  12812  expmulnbnd  12813  discr1  12817  bcn1  12917  hashnn0n0nn  12993  brfi1indALT  13083  brfi1indALTOLD  13089  s2fv0  13428  swrd2lsw  13489  2swrd2eqwrdeq  13490  sgn1  13626  resqrex  13785  mulcn2  14120  cvgrat  14400  bpoly4  14575  cos1bnd  14702  sin01gt0  14705  sincos1sgn  14708  ruclem8  14751  nnoddm1d2  14886  sadcadd  14964  dvdsnprmd  15187  isprm7  15204  divdenle  15241  43prm  15613  ipostr  16922  srgbinomlem4  18312  abvtrivd  18609  gzrngunit  19577  znidomb  19674  psgnodpmr  19700  thlle  19802  leordtval2  20768  mopnex  22075  dscopn  22129  metnrmlem1a  22400  xrhmph  22485  evth  22497  xlebnum  22503  vitalilem5  23104  vitali  23105  ply1remlem  23643  plyremlem  23780  plyrem  23781  vieta1lem2  23787  reeff1olem  23921  sinhalfpilem  23936  rplogcl  24071  logtayllem  24122  cxplt  24157  cxple  24158  atanlogaddlem  24357  ressatans  24378  rlimcnp  24409  rlimcnp2  24410  cxp2limlem  24419  cxp2lim  24420  cxploglim2  24422  amgmlem  24433  emcllem2  24440  harmonicubnd  24453  fsumharmonic  24455  zetacvg  24458  ftalem1  24516  ftalem2  24517  chpchtsum  24661  chpub  24662  mersenne  24669  perfectlem2  24672  efexple  24723  chebbnd1  24878  dchrmusumlema  24899  dchrvmasumlem2  24904  dchrvmasumiflem1  24907  dchrisum0flblem2  24915  dchrisum0lema  24920  dchrisum0lem1  24922  dchrisum0lem2a  24923  mulog2sumlem1  24940  chpdifbndlem1  24959  chpdifbnd  24961  selberg3lem1  24963  pntrmax  24970  pntrsumo1  24971  pntpbnd1a  24991  pntpbnd2  24993  pntibndlem1  24995  pntlem3  25015  pnt  25020  ostth2lem1  25024  ostth2lem3  25041  ostth2lem4  25042  axcontlem2  25563  spthispth  25869  usgrcyclnl1  25934  clwwlkf1  26090  esumcst  29258  hasheuni  29280  ballotlemi1  29697  ballotlemic  29701  sgnnbi  29740  sgnpbi  29741  sgnmulsgp  29745  signsply0  29760  signswch  29770  unblimceq0  31474  knoppndvlem1  31479  knoppndvlem2  31480  knoppndvlem7  31485  knoppndvlem13  31491  knoppndvlem14  31492  knoppndvlem15  31493  knoppndvlem17  31495  knoppndvlem20  31498  poimirlem22  32397  poimirlem31  32406  asindmre  32461  areacirclem4  32469  pellexlem2  36208  pellexlem6  36212  pell14qrgt0  36237  elpell1qr2  36250  pellfundex  36264  pellfundrp  36266  rmxypos  36328  relexp01min  36820  imo72b2  37293  radcnvrat  37331  reclt0d  38345  sqrlearg  38424  sumnnodd  38494  dvnmul  38630  stoweidlem7  38697  stoweidlem36  38726  stoweidlem38  38728  stoweidlem42  38732  stoweidlem51  38741  stoweidlem59  38749  stirlinglem5  38768  stirlinglem7  38770  stirlinglem10  38773  stirlinglem11  38774  stirlinglem12  38775  stirlinglem15  38778  dirkeritg  38792  fourierdlem11  38808  fourierdlem30  38827  fourierdlem47  38843  fourierdlem79  38875  fourierdlem103  38899  fourierdlem104  38900  fouriersw  38921  etransclem4  38928  etransclem31  38955  etransclem32  38956  etransclem35  38959  etransclem41  38965  salexct2  39030  hoidmvlelem1  39282  m1mod0mod1  39747  wwlksn0s  41052  clwwlksf1  41219  m1modmmod  42105  regt1loggt0  42123  rege1logbrege0  42145  nnlog2ge0lt1  42153  amgmwlem  42313
  Copyright terms: Public domain W3C validator