Theorem 0lt1 11672

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

Step	Hyp	Ref	Expression
1		1re 11144	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11107	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11670	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 693	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11149	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5110	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2114   ≠ wne 2932   class class class wbr 5085  (class class class)co 7367  ℝcr 11037  0cc0 11038  1c1 11039   · cmul 11043   < clt 11179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380

This theorem is referenced by:  0le1  11673  eqneg  11875  elimgt0  11993  ltp1  11995  ltm1  11997  recgt0  12001  mulgt1OLD  12014  mulgt1  12017  reclt1  12051  recgt1  12052  recgt1i  12053  recp1lt1  12054  recreclt  12055  recgt0ii  12062  neg1lt0  12147  nnge1  12205  nngt0  12208  0nnnALT  12214  nnrecgt0  12220  2pos  12284  3pos  12286  4pos  12288  5pos  12290  6pos  12291  7pos  12292  8pos  12293  9pos  12294  halflt1  12394  nn0p1gt0  12466  elnnnn0c  12482  elnnz1  12553  nn0lt10b  12591  recnz  12604  1rp  12946  divlt1lt  13013  divle1le  13014  ledivge1le  13015  nnledivrp  13056  xmulrid  13231  0nelfz1  13497  fz10  13499  fzpreddisj  13527  elfznelfzob  13729  1mod  13862  expgt1  14062  ltexp2a  14128  expcan  14131  ltexp2  14132  leexp2  14133  leexp2a  14134  expnbnd  14194  expnlbnd  14195  expnlbnd2  14196  expmulnbnd  14197  discr1  14201  bcn1  14275  hashnn0n0nn  14353  s2fv0  14849  swrd2lsw  14914  2swrd2eqwrdeq  14915  sgn1  15054  resqrex  15212  mulcn2  15558  cvgrat  15848  bpoly4  16024  cos1bnd  16154  sin01gt0  16157  sincos1sgn  16160  ruclem8  16204  p1modz1  16228  nnoddm1d2  16355  sadcadd  16427  dvdsnprmd  16659  isprm7  16678  divdenle  16719  43prm  17092  plendxnocndx  17347  ipostr  18495  srgbinomlem4  20210  abvtrivd  20809  gzrngunit  21413  znidomb  21541  psgnodpmr  21570  leordtval2  23177  mopnex  24484  dscopn  24538  metnrmlem1a  24824  xrhmph  24914  evth  24926  xlebnum  24932  vitalilem5  25579  vitali  25580  ply1remlem  26130  plyremlem  26270  plyrem  26271  vieta1lem2  26277  reeff1olem  26411  sinhalfpilem  26427  rplogcl  26568  logtayllem  26623  cxplt  26658  cxple  26659  atanlogaddlem  26877  ressatans  26898  rlimcnp  26929  rlimcnp2  26930  cxp2limlem  26939  cxp2lim  26940  cxploglim2  26942  amgmlem  26953  emcllem2  26960  harmonicubnd  26973  fsumharmonic  26975  zetacvg  26978  ftalem1  27036  ftalem2  27037  chpchtsum  27182  chpub  27183  mersenne  27190  perfectlem2  27193  efexple  27244  chebbnd1  27435  dchrmusumlema  27456  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0flblem2  27472  dchrisum0lema  27477  dchrisum0lem1  27479  dchrisum0lem2a  27480  mulog2sumlem1  27497  chpdifbndlem1  27516  chpdifbnd  27518  selberg3lem1  27520  pntrmax  27527  pntrsumo1  27528  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem1  27552  pntlem3  27572  pnt  27577  ostth2lem1  27581  ostth2lem3  27598  ostth2lem4  27599  axcontlem2  29034  wwlksn0s  29929  clwwlkf1  30119  sgnnbi  32911  sgnpbi  32912  sgnmulsgp  32916  vietadeg1  33722  cos9thpiminplylem1  33926  cos9thpiminply  33932  esumcst  34207  hasheuni  34229  ballotlemi1  34647  ballotlemic  34651  signsply0  34695  signswch  34705  hgt750lem  34795  unblimceq0  36767  knoppndvlem1  36772  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem13  36784  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem20  36791  irrdiff  37640  poimirlem22  37963  poimirlem31  37972  asindmre  38024  areacirclem4  38032  60gcd7e1  42444  3lexlogpow5ineq2  42494  aks4d1p1p2  42509  aks4d1p7  42522  aks4d1p8d2  42524  aks4d1p8d3  42525  aks4d1p8  42526  aks4d1p9  42527  aks6d1c5lem3  42576  sticksstones11  42595  aks6d1c6lem1  42609  aks6d1c6lem4  42612  aks6d1c7lem2  42620  explt1d  42755  3cubeslem1  43116  pellexlem2  43258  pellexlem6  43262  pell14qrgt0  43287  elpell1qr2  43300  pellfundex  43314  pellfundrp  43316  rmxypos  43375  relexp01min  44140  imo72b2  44599  radcnvrat  44741  reclt0d  45816  sqrlearg  45983  sumnnodd  46060  liminf10ex  46202  liminfltlimsupex  46209  dvnmul  46371  stoweidlem7  46435  stoweidlem36  46464  stoweidlem38  46466  stoweidlem42  46470  stoweidlem51  46479  stoweidlem59  46487  stirlinglem5  46506  stirlinglem7  46508  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  stirlinglem15  46516  dirkeritg  46530  fourierdlem11  46546  fourierdlem30  46565  fourierdlem47  46581  fourierdlem79  46613  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  etransclem4  46666  etransclem31  46693  etransclem32  46694  etransclem35  46697  etransclem41  46703  salexct2  46767  hoidmvlelem1  47023  cjnpoly  47337  m1mod0mod1  47808  m1modmmod  47812  muldvdsfacgt  47834  muldvdsfacm1  47835  nfermltl2rev  48219  regt1loggt0  49012  rege1logbrege0  49034  nnlog2ge0lt1  49042  eenglngeehlnmlem2  49214  amgmwlem  50277