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

Theorem 0lt1 11150
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 10629 . . 3 1 ∈ ℝ
2 ax-1ne0 10594 . . 3 1 ≠ 0
3 msqgt0 11148 . . 3 ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
41, 2, 3mp2an 688 . 2 0 < (1 · 1)
5 ax-1cn 10583 . . 3 1 ∈ ℂ
65mulid1i 10633 . 2 (1 · 1) = 1
74, 6breqtri 5082 1 0 < 1
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  wne 3013   class class class wbr 5057  (class class class)co 7145  cr 10524  0cc0 10525  1c1 10526   · cmul 10530   < clt 10663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861
This theorem is referenced by:  0le1  11151  eqneg  11348  elimgt0  11466  ltp1  11468  ltm1  11470  recgt0  11474  mulgt1  11487  reclt1  11523  recgt1  11524  recgt1i  11525  recp1lt1  11526  recreclt  11527  recgt0ii  11534  inelr  11616  nnge1  11653  nngt0  11656  0nnnALT  11662  nnrecgt0  11668  2pos  11728  3pos  11730  4pos  11732  5pos  11734  6pos  11735  7pos  11736  8pos  11737  9pos  11738  neg1lt0  11742  halflt1  11843  nn0p1gt0  11914  elnnnn0c  11930  elnnz1  11996  nn0lt10b  12032  recnz  12045  1rp  12381  divlt1lt  12446  divle1le  12447  ledivge1le  12448  nnledivrp  12489  xmulid1  12660  0nelfz1  12914  fz10  12916  fzpreddisj  12944  elfznelfzob  13131  1mod  13259  expgt1  13455  ltexp2a  13518  expcan  13521  ltexp2  13522  leexp2  13523  leexp2a  13524  expnbnd  13581  expnlbnd  13582  expnlbnd2  13583  expmulnbnd  13584  discr1  13588  bcn1  13661  hashnn0n0nn  13740  brfi1indALT  13846  s2fv0  14237  swrd2lsw  14302  2swrd2eqwrdeq  14303  sgn1  14439  resqrex  14598  mulcn2  14940  cvgrat  15227  bpoly4  15401  cos1bnd  15528  sin01gt0  15531  sincos1sgn  15534  ruclem8  15578  p1modz1  15602  nnoddm1d2  15725  sadcadd  15795  dvdsnprmd  16022  isprm7  16040  divdenle  16077  43prm  16443  ipostr  17751  srgbinomlem4  19222  abvtrivd  19540  gzrngunit  20539  znidomb  20636  psgnodpmr  20662  thlle  20769  leordtval2  21748  mopnex  23056  dscopn  23110  metnrmlem1a  23393  xrhmph  23478  evth  23490  xlebnum  23496  vitalilem5  24140  vitali  24141  ply1remlem  24683  plyremlem  24820  plyrem  24821  vieta1lem2  24827  reeff1olem  24961  sinhalfpilem  24976  rplogcl  25114  logtayllem  25169  cxplt  25204  cxple  25205  atanlogaddlem  25418  ressatans  25439  rlimcnp  25470  rlimcnp2  25471  cxp2limlem  25480  cxp2lim  25481  cxploglim2  25483  amgmlem  25494  emcllem2  25501  harmonicubnd  25514  fsumharmonic  25516  zetacvg  25519  ftalem1  25577  ftalem2  25578  chpchtsum  25722  chpub  25723  mersenne  25730  perfectlem2  25733  efexple  25784  chebbnd1  25975  dchrmusumlema  25996  dchrvmasumlem2  26001  dchrvmasumiflem1  26004  dchrisum0flblem2  26012  dchrisum0lema  26017  dchrisum0lem1  26019  dchrisum0lem2a  26020  mulog2sumlem1  26037  chpdifbndlem1  26056  chpdifbnd  26058  selberg3lem1  26060  pntrmax  26067  pntrsumo1  26068  pntpbnd1a  26088  pntpbnd2  26090  pntibndlem1  26092  pntlem3  26112  pnt  26117  ostth2lem1  26121  ostth2lem3  26138  ostth2lem4  26139  axcontlem2  26678  wwlksn0s  27566  clwwlkf1  27755  esumcst  31221  hasheuni  31243  ballotlemi1  31659  ballotlemic  31663  sgnnbi  31702  sgnpbi  31703  sgnmulsgp  31707  signsply0  31720  signswch  31730  hgt750lem  31821  unblimceq0  33743  knoppndvlem1  33748  knoppndvlem2  33749  knoppndvlem7  33754  knoppndvlem13  33760  knoppndvlem14  33761  knoppndvlem15  33762  knoppndvlem17  33764  knoppndvlem20  33767  poimirlem22  34795  poimirlem31  34804  asindmre  34858  areacirclem4  34866  3cubeslem1  39159  pellexlem2  39305  pellexlem6  39309  pell14qrgt0  39334  elpell1qr2  39347  pellfundex  39361  pellfundrp  39363  rmxypos  39422  relexp01min  39936  imo72b2  40403  radcnvrat  40523  reclt0d  41534  sqrlearg  41705  sumnnodd  41787  liminf10ex  41931  liminfltlimsupex  41938  dvnmul  42104  stoweidlem7  42169  stoweidlem36  42198  stoweidlem38  42200  stoweidlem42  42204  stoweidlem51  42213  stoweidlem59  42221  stirlinglem5  42240  stirlinglem7  42242  stirlinglem10  42245  stirlinglem11  42246  stirlinglem12  42247  stirlinglem15  42250  dirkeritg  42264  fourierdlem11  42280  fourierdlem30  42299  fourierdlem47  42315  fourierdlem79  42347  fourierdlem103  42371  fourierdlem104  42372  fouriersw  42393  etransclem4  42400  etransclem31  42427  etransclem32  42428  etransclem35  42431  etransclem41  42437  salexct2  42499  hoidmvlelem1  42754  m1mod0mod1  43406  nfermltl2rev  43785  m1modmmod  44509  regt1loggt0  44524  rege1logbrege0  44546  nnlog2ge0lt1  44554  eenglngeehlnmlem2  44653  amgmwlem  44831
  Copyright terms: Public domain W3C validator