Theorem 0lt1 11676

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 11150	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11113	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11674	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 692	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11102	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11154	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5127	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2109   ≠ wne 2925   class class class wbr 5102  (class class class)co 7369  ℝcr 11043  0cc0 11044  1c1 11045   · cmul 11049   < clt 11184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  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 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384

This theorem is referenced by:  0le1  11677  eqneg  11878  elimgt0  11996  ltp1  11998  ltm1  12000  recgt0  12004  mulgt1OLD  12017  mulgt1  12020  reclt1  12054  recgt1  12055  recgt1i  12056  recp1lt1  12057  recreclt  12058  recgt0ii  12065  neg1lt0  12150  nnge1  12190  nngt0  12193  0nnnALT  12199  nnrecgt0  12205  2pos  12265  3pos  12267  4pos  12269  5pos  12271  6pos  12272  7pos  12273  8pos  12274  9pos  12275  halflt1  12375  nn0p1gt0  12447  elnnnn0c  12463  elnnz1  12535  nn0lt10b  12572  recnz  12585  1rp  12931  divlt1lt  12998  divle1le  12999  ledivge1le  13000  nnledivrp  13041  xmulrid  13215  0nelfz1  13480  fz10  13482  fzpreddisj  13510  elfznelfzob  13710  1mod  13841  expgt1  14041  ltexp2a  14107  expcan  14110  ltexp2  14111  leexp2  14112  leexp2a  14113  expnbnd  14173  expnlbnd  14174  expnlbnd2  14175  expmulnbnd  14176  discr1  14180  bcn1  14254  hashnn0n0nn  14332  s2fv0  14829  swrd2lsw  14894  2swrd2eqwrdeq  14895  sgn1  15034  resqrex  15192  mulcn2  15538  cvgrat  15825  bpoly4  16001  cos1bnd  16131  sin01gt0  16134  sincos1sgn  16137  ruclem8  16181  p1modz1  16205  nnoddm1d2  16332  sadcadd  16404  dvdsnprmd  16636  isprm7  16654  divdenle  16695  43prm  17068  plendxnocndx  17323  ipostr  18464  srgbinomlem4  20114  abvtrivd  20717  gzrngunit  21326  znidomb  21447  psgnodpmr  21475  leordtval2  23075  mopnex  24383  dscopn  24437  metnrmlem1a  24723  xrhmph  24821  evth  24834  xlebnum  24840  vitalilem5  25489  vitali  25490  ply1remlem  26046  plyremlem  26188  plyrem  26189  vieta1lem2  26195  reeff1olem  26332  sinhalfpilem  26348  rplogcl  26489  logtayllem  26544  cxplt  26579  cxple  26580  atanlogaddlem  26799  ressatans  26820  rlimcnp  26851  rlimcnp2  26852  cxp2limlem  26862  cxp2lim  26863  cxploglim2  26865  amgmlem  26876  emcllem2  26883  harmonicubnd  26896  fsumharmonic  26898  zetacvg  26901  ftalem1  26959  ftalem2  26960  chpchtsum  27106  chpub  27107  mersenne  27114  perfectlem2  27117  efexple  27168  chebbnd1  27359  dchrmusumlema  27380  dchrvmasumlem2  27385  dchrvmasumiflem1  27388  dchrisum0flblem2  27396  dchrisum0lema  27401  dchrisum0lem1  27403  dchrisum0lem2a  27404  mulog2sumlem1  27421  chpdifbndlem1  27440  chpdifbnd  27442  selberg3lem1  27444  pntrmax  27451  pntrsumo1  27452  pntpbnd1a  27472  pntpbnd2  27474  pntibndlem1  27476  pntlem3  27496  pnt  27501  ostth2lem1  27505  ostth2lem3  27522  ostth2lem4  27523  axcontlem2  28868  wwlksn0s  29764  clwwlkf1  29951  sgnnbi  32736  sgnpbi  32737  sgnmulsgp  32741  cos9thpiminplylem1  33745  cos9thpiminply  33751  esumcst  34026  hasheuni  34048  ballotlemi1  34467  ballotlemic  34471  signsply0  34515  signswch  34525  hgt750lem  34615  unblimceq0  36468  knoppndvlem1  36473  knoppndvlem2  36474  knoppndvlem7  36479  knoppndvlem13  36485  knoppndvlem14  36486  knoppndvlem15  36487  knoppndvlem17  36489  knoppndvlem20  36492  irrdiff  37287  poimirlem22  37609  poimirlem31  37618  asindmre  37670  areacirclem4  37678  60gcd7e1  41966  3lexlogpow5ineq2  42016  aks4d1p1p2  42031  aks4d1p7  42044  aks4d1p8d2  42046  aks4d1p8d3  42047  aks4d1p8  42048  aks4d1p9  42049  aks6d1c5lem3  42098  sticksstones11  42117  aks6d1c6lem1  42131  aks6d1c6lem4  42134  aks6d1c7lem2  42142  explt1d  42284  3cubeslem1  42645  pellexlem2  42791  pellexlem6  42795  pell14qrgt0  42820  elpell1qr2  42833  pellfundex  42847  pellfundrp  42849  rmxypos  42909  relexp01min  43675  imo72b2  44134  radcnvrat  44276  reclt0d  45356  sqrlearg  45524  sumnnodd  45601  liminf10ex  45745  liminfltlimsupex  45752  dvnmul  45914  stoweidlem7  45978  stoweidlem36  46007  stoweidlem38  46009  stoweidlem42  46013  stoweidlem51  46022  stoweidlem59  46030  stirlinglem5  46049  stirlinglem7  46051  stirlinglem10  46054  stirlinglem11  46055  stirlinglem12  46056  stirlinglem15  46059  dirkeritg  46073  fourierdlem11  46089  fourierdlem30  46108  fourierdlem47  46124  fourierdlem79  46156  fourierdlem103  46180  fourierdlem104  46181  fouriersw  46202  etransclem4  46209  etransclem31  46236  etransclem32  46237  etransclem35  46240  etransclem41  46246  salexct2  46310  hoidmvlelem1  46566  tworepnotupword  46857  cjnpoly  46863  m1mod0mod1  47328  m1modmmod  47332  nfermltl2rev  47717  regt1loggt0  48498  rege1logbrege0  48520  nnlog2ge0lt1  48528  eenglngeehlnmlem2  48700  amgmwlem  49764