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

Theorem 0lt1 11156
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 10635 . . 3 1 ∈ ℝ
2 ax-1ne0 10600 . . 3 1 ≠ 0
3 msqgt0 11154 . . 3 ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
41, 2, 3mp2an 690 . 2 0 < (1 · 1)
5 ax-1cn 10589 . . 3 1 ∈ ℂ
65mulid1i 10639 . 2 (1 · 1) = 1
74, 6breqtri 5083 1 0 < 1
Colors of variables: wff setvar class
Syntax hints:  wcel 2110  wne 3016   class class class wbr 5058  (class class class)co 7150  cr 10530  0cc0 10531  1c1 10532   · cmul 10536   < clt 10669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-po 5468  df-so 5469  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867
This theorem is referenced by:  0le1  11157  eqneg  11354  elimgt0  11472  ltp1  11474  ltm1  11476  recgt0  11480  mulgt1  11493  reclt1  11529  recgt1  11530  recgt1i  11531  recp1lt1  11532  recreclt  11533  recgt0ii  11540  inelr  11622  nnge1  11659  nngt0  11662  0nnnALT  11668  nnrecgt0  11674  2pos  11734  3pos  11736  4pos  11738  5pos  11740  6pos  11741  7pos  11742  8pos  11743  9pos  11744  neg1lt0  11748  halflt1  11849  nn0p1gt0  11920  elnnnn0c  11936  elnnz1  12002  nn0lt10b  12038  recnz  12051  1rp  12387  divlt1lt  12452  divle1le  12453  ledivge1le  12454  nnledivrp  12495  xmulid1  12666  0nelfz1  12920  fz10  12922  fzpreddisj  12950  elfznelfzob  13137  1mod  13265  expgt1  13461  ltexp2a  13524  expcan  13527  ltexp2  13528  leexp2  13529  leexp2a  13530  expnbnd  13587  expnlbnd  13588  expnlbnd2  13589  expmulnbnd  13590  discr1  13594  bcn1  13667  hashnn0n0nn  13746  brfi1indALT  13852  s2fv0  14243  swrd2lsw  14308  2swrd2eqwrdeq  14309  sgn1  14445  resqrex  14604  mulcn2  14946  cvgrat  15233  bpoly4  15407  cos1bnd  15534  sin01gt0  15537  sincos1sgn  15540  ruclem8  15584  p1modz1  15608  nnoddm1d2  15731  sadcadd  15801  dvdsnprmd  16028  isprm7  16046  divdenle  16083  43prm  16449  ipostr  17757  srgbinomlem4  19287  abvtrivd  19605  gzrngunit  20605  znidomb  20702  psgnodpmr  20728  thlle  20835  leordtval2  21814  mopnex  23123  dscopn  23177  metnrmlem1a  23460  xrhmph  23545  evth  23557  xlebnum  23563  vitalilem5  24207  vitali  24208  ply1remlem  24750  plyremlem  24887  plyrem  24888  vieta1lem2  24894  reeff1olem  25028  sinhalfpilem  25043  rplogcl  25181  logtayllem  25236  cxplt  25271  cxple  25272  atanlogaddlem  25485  ressatans  25506  rlimcnp  25537  rlimcnp2  25538  cxp2limlem  25547  cxp2lim  25548  cxploglim2  25550  amgmlem  25561  emcllem2  25568  harmonicubnd  25581  fsumharmonic  25583  zetacvg  25586  ftalem1  25644  ftalem2  25645  chpchtsum  25789  chpub  25790  mersenne  25797  perfectlem2  25800  efexple  25851  chebbnd1  26042  dchrmusumlema  26063  dchrvmasumlem2  26068  dchrvmasumiflem1  26071  dchrisum0flblem2  26079  dchrisum0lema  26084  dchrisum0lem1  26086  dchrisum0lem2a  26087  mulog2sumlem1  26104  chpdifbndlem1  26123  chpdifbnd  26125  selberg3lem1  26127  pntrmax  26134  pntrsumo1  26135  pntpbnd1a  26155  pntpbnd2  26157  pntibndlem1  26159  pntlem3  26179  pnt  26184  ostth2lem1  26188  ostth2lem3  26205  ostth2lem4  26206  axcontlem2  26745  wwlksn0s  27633  clwwlkf1  27822  esumcst  31317  hasheuni  31339  ballotlemi1  31755  ballotlemic  31759  sgnnbi  31798  sgnpbi  31799  sgnmulsgp  31803  signsply0  31816  signswch  31826  hgt750lem  31917  unblimceq0  33841  knoppndvlem1  33846  knoppndvlem2  33847  knoppndvlem7  33852  knoppndvlem13  33858  knoppndvlem14  33859  knoppndvlem15  33860  knoppndvlem17  33862  knoppndvlem20  33865  poimirlem22  34908  poimirlem31  34917  asindmre  34971  areacirclem4  34979  3cubeslem1  39274  pellexlem2  39420  pellexlem6  39424  pell14qrgt0  39449  elpell1qr2  39462  pellfundex  39476  pellfundrp  39478  rmxypos  39537  relexp01min  40051  imo72b2  40518  radcnvrat  40639  reclt0d  41651  sqrlearg  41822  sumnnodd  41904  liminf10ex  42048  liminfltlimsupex  42055  dvnmul  42221  stoweidlem7  42286  stoweidlem36  42315  stoweidlem38  42317  stoweidlem42  42321  stoweidlem51  42330  stoweidlem59  42338  stirlinglem5  42357  stirlinglem7  42359  stirlinglem10  42362  stirlinglem11  42363  stirlinglem12  42364  stirlinglem15  42367  dirkeritg  42381  fourierdlem11  42397  fourierdlem30  42416  fourierdlem47  42432  fourierdlem79  42464  fourierdlem103  42488  fourierdlem104  42489  fouriersw  42510  etransclem4  42517  etransclem31  42544  etransclem32  42545  etransclem35  42548  etransclem41  42554  salexct2  42616  hoidmvlelem1  42871  m1mod0mod1  43523  nfermltl2rev  43902  m1modmmod  44575  regt1loggt0  44590  rege1logbrege0  44612  nnlog2ge0lt1  44620  eenglngeehlnmlem2  44719  amgmwlem  44897
  Copyright terms: Public domain W3C validator