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

Theorem 0lt1 10588
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 10077 . . 3 1 ∈ ℝ
2 ax-1ne0 10043 . . 3 1 ≠ 0
3 msqgt0 10586 . . 3 ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
41, 2, 3mp2an 708 . 2 0 < (1 · 1)
5 ax-1cn 10032 . . 3 1 ∈ ℂ
65mulid1i 10080 . 2 (1 · 1) = 1
74, 6breqtri 4710 1 0 < 1
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  wne 2823   class class class wbr 4685  (class class class)co 6690  cr 9973  0cc0 9974  1c1 9975   · cmul 9979   < clt 10112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307
This theorem is referenced by:  0le1  10589  eqneg  10783  elimgt0  10897  ltp1  10899  ltm1  10901  recgt0  10905  mulgt1  10920  reclt1  10956  recgt1  10957  recgt1i  10958  recp1lt1  10959  recreclt  10960  recgt0ii  10967  inelr  11048  nnge1  11084  nngt0  11087  0nnn  11090  nnrecgt0  11096  2pos  11150  3pos  11152  4pos  11154  5pos  11156  6pos  11157  7pos  11158  8pos  11159  9pos  11160  10posOLD  11161  neg1lt0  11165  halflt1  11288  nn0p1gt0  11360  elnnnn0c  11376  elnnz1  11441  nn0lt10b  11477  recnz  11490  1rp  11874  divlt1lt  11937  divle1le  11938  ledivge1le  11939  nnledivrp  11978  xmulid1  12147  0nelfz1  12398  fz10  12400  fzpreddisj  12428  elfznelfzob  12614  1mod  12742  expgt1  12938  ltexp2a  12952  expcan  12953  ltexp2  12954  leexp2  12955  leexp2a  12956  expnbnd  13033  expnlbnd  13034  expnlbnd2  13035  expmulnbnd  13036  discr1  13040  bcn1  13140  hashnn0n0nn  13218  brfi1indALT  13320  s2fv0  13678  swrd2lsw  13741  2swrd2eqwrdeq  13742  sgn1  13876  resqrex  14035  mulcn2  14370  cvgrat  14659  bpoly4  14834  cos1bnd  14961  sin01gt0  14964  sincos1sgn  14967  ruclem8  15010  p1modz1  15034  nnoddm1d2  15149  sadcadd  15227  dvdsnprmd  15450  isprm7  15467  divdenle  15504  43prm  15876  ipostr  17200  srgbinomlem4  18589  abvtrivd  18888  gzrngunit  19860  znidomb  19958  psgnodpmr  19984  thlle  20089  leordtval2  21064  mopnex  22371  dscopn  22425  metnrmlem1a  22708  xrhmph  22793  evth  22805  xlebnum  22811  vitalilem5  23426  vitali  23427  ply1remlem  23967  plyremlem  24104  plyrem  24105  vieta1lem2  24111  reeff1olem  24245  sinhalfpilem  24260  rplogcl  24395  logtayllem  24450  cxplt  24485  cxple  24486  atanlogaddlem  24685  ressatans  24706  rlimcnp  24737  rlimcnp2  24738  cxp2limlem  24747  cxp2lim  24748  cxploglim2  24750  amgmlem  24761  emcllem2  24768  harmonicubnd  24781  fsumharmonic  24783  zetacvg  24786  ftalem1  24844  ftalem2  24845  chpchtsum  24989  chpub  24990  mersenne  24997  perfectlem2  25000  efexple  25051  chebbnd1  25206  dchrmusumlema  25227  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  dchrisum0flblem2  25243  dchrisum0lema  25248  dchrisum0lem1  25250  dchrisum0lem2a  25251  mulog2sumlem1  25268  chpdifbndlem1  25287  chpdifbnd  25289  selberg3lem1  25291  pntrmax  25298  pntrsumo1  25299  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem1  25323  pntlem3  25343  pnt  25348  ostth2lem1  25352  ostth2lem3  25369  ostth2lem4  25370  axcontlem2  25890  wwlksn0s  26815  clwwlkf1  27012  esumcst  30253  hasheuni  30275  ballotlemi1  30692  ballotlemic  30696  sgnnbi  30735  sgnpbi  30736  sgnmulsgp  30740  signsply0  30756  signswch  30766  hgt750lem  30857  unblimceq0  32623  knoppndvlem1  32628  knoppndvlem2  32629  knoppndvlem7  32634  knoppndvlem13  32640  knoppndvlem14  32641  knoppndvlem15  32642  knoppndvlem17  32644  knoppndvlem20  32647  poimirlem22  33561  poimirlem31  33570  asindmre  33625  areacirclem4  33633  pellexlem2  37711  pellexlem6  37715  pell14qrgt0  37740  elpell1qr2  37753  pellfundex  37767  pellfundrp  37769  rmxypos  37831  relexp01min  38322  imo72b2  38792  radcnvrat  38830  reclt0d  39920  sqrlearg  40098  sumnnodd  40180  liminf10ex  40324  liminfltlimsupex  40331  dvnmul  40476  stoweidlem7  40542  stoweidlem36  40571  stoweidlem38  40573  stoweidlem42  40577  stoweidlem51  40586  stoweidlem59  40594  stirlinglem5  40613  stirlinglem7  40615  stirlinglem10  40618  stirlinglem11  40619  stirlinglem12  40620  stirlinglem15  40623  dirkeritg  40637  fourierdlem11  40653  fourierdlem30  40672  fourierdlem47  40688  fourierdlem79  40720  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  etransclem4  40773  etransclem31  40800  etransclem32  40801  etransclem35  40804  etransclem41  40810  salexct2  40875  hoidmvlelem1  41130  m1mod0mod1  41664  m1modmmod  42641  regt1loggt0  42655  rege1logbrege0  42677  nnlog2ge0lt1  42685  amgmwlem  42876
  Copyright terms: Public domain W3C validator