Theorem 0lt1 11661

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 11134	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11097	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11659	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 692	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11086	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11138	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5120	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2109   ≠ wne 2925   class class class wbr 5095  (class class class)co 7353  ℝcr 11027  0cc0 11028  1c1 11029   · cmul 11033   < clt 11168

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 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

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 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369

This theorem is referenced by:  0le1  11662  eqneg  11863  elimgt0  11981  ltp1  11983  ltm1  11985  recgt0  11989  mulgt1OLD  12002  mulgt1  12005  reclt1  12039  recgt1  12040  recgt1i  12041  recp1lt1  12042  recreclt  12043  recgt0ii  12050  neg1lt0  12135  nnge1  12175  nngt0  12178  0nnnALT  12184  nnrecgt0  12190  2pos  12250  3pos  12252  4pos  12254  5pos  12256  6pos  12257  7pos  12258  8pos  12259  9pos  12260  halflt1  12360  nn0p1gt0  12432  elnnnn0c  12448  elnnz1  12520  nn0lt10b  12557  recnz  12570  1rp  12916  divlt1lt  12983  divle1le  12984  ledivge1le  12985  nnledivrp  13026  xmulrid  13200  0nelfz1  13465  fz10  13467  fzpreddisj  13495  elfznelfzob  13695  1mod  13826  expgt1  14026  ltexp2a  14092  expcan  14095  ltexp2  14096  leexp2  14097  leexp2a  14098  expnbnd  14158  expnlbnd  14159  expnlbnd2  14160  expmulnbnd  14161  discr1  14165  bcn1  14239  hashnn0n0nn  14317  s2fv0  14813  swrd2lsw  14878  2swrd2eqwrdeq  14879  sgn1  15018  resqrex  15176  mulcn2  15522  cvgrat  15809  bpoly4  15985  cos1bnd  16115  sin01gt0  16118  sincos1sgn  16121  ruclem8  16165  p1modz1  16189  nnoddm1d2  16316  sadcadd  16388  dvdsnprmd  16620  isprm7  16638  divdenle  16679  43prm  17052  plendxnocndx  17307  ipostr  18454  srgbinomlem4  20133  abvtrivd  20736  gzrngunit  21359  znidomb  21487  psgnodpmr  21516  leordtval2  23116  mopnex  24424  dscopn  24478  metnrmlem1a  24764  xrhmph  24862  evth  24875  xlebnum  24881  vitalilem5  25530  vitali  25531  ply1remlem  26087  plyremlem  26229  plyrem  26230  vieta1lem2  26236  reeff1olem  26373  sinhalfpilem  26389  rplogcl  26530  logtayllem  26585  cxplt  26620  cxple  26621  atanlogaddlem  26840  ressatans  26861  rlimcnp  26892  rlimcnp2  26893  cxp2limlem  26903  cxp2lim  26904  cxploglim2  26906  amgmlem  26917  emcllem2  26924  harmonicubnd  26937  fsumharmonic  26939  zetacvg  26942  ftalem1  27000  ftalem2  27001  chpchtsum  27147  chpub  27148  mersenne  27155  perfectlem2  27158  efexple  27209  chebbnd1  27400  dchrmusumlema  27421  dchrvmasumlem2  27426  dchrvmasumiflem1  27429  dchrisum0flblem2  27437  dchrisum0lema  27442  dchrisum0lem1  27444  dchrisum0lem2a  27445  mulog2sumlem1  27462  chpdifbndlem1  27481  chpdifbnd  27483  selberg3lem1  27485  pntrmax  27492  pntrsumo1  27493  pntpbnd1a  27513  pntpbnd2  27515  pntibndlem1  27517  pntlem3  27537  pnt  27542  ostth2lem1  27546  ostth2lem3  27563  ostth2lem4  27564  axcontlem2  28929  wwlksn0s  29825  clwwlkf1  30012  sgnnbi  32802  sgnpbi  32803  sgnmulsgp  32807  cos9thpiminplylem1  33768  cos9thpiminply  33774  esumcst  34049  hasheuni  34071  ballotlemi1  34490  ballotlemic  34494  signsply0  34538  signswch  34548  hgt750lem  34638  unblimceq0  36500  knoppndvlem1  36505  knoppndvlem2  36506  knoppndvlem7  36511  knoppndvlem13  36517  knoppndvlem14  36518  knoppndvlem15  36519  knoppndvlem17  36521  knoppndvlem20  36524  irrdiff  37319  poimirlem22  37641  poimirlem31  37650  asindmre  37702  areacirclem4  37710  60gcd7e1  41998  3lexlogpow5ineq2  42048  aks4d1p1p2  42063  aks4d1p7  42076  aks4d1p8d2  42078  aks4d1p8d3  42079  aks4d1p8  42080  aks4d1p9  42081  aks6d1c5lem3  42130  sticksstones11  42149  aks6d1c6lem1  42163  aks6d1c6lem4  42166  aks6d1c7lem2  42174  explt1d  42316  3cubeslem1  42677  pellexlem2  42823  pellexlem6  42827  pell14qrgt0  42852  elpell1qr2  42865  pellfundex  42879  pellfundrp  42881  rmxypos  42940  relexp01min  43706  imo72b2  44165  radcnvrat  44307  reclt0d  45386  sqrlearg  45554  sumnnodd  45631  liminf10ex  45775  liminfltlimsupex  45782  dvnmul  45944  stoweidlem7  46008  stoweidlem36  46037  stoweidlem38  46039  stoweidlem42  46043  stoweidlem51  46052  stoweidlem59  46060  stirlinglem5  46079  stirlinglem7  46081  stirlinglem10  46084  stirlinglem11  46085  stirlinglem12  46086  stirlinglem15  46089  dirkeritg  46103  fourierdlem11  46119  fourierdlem30  46138  fourierdlem47  46154  fourierdlem79  46186  fourierdlem103  46210  fourierdlem104  46211  fouriersw  46232  etransclem4  46239  etransclem31  46266  etransclem32  46267  etransclem35  46270  etransclem41  46276  salexct2  46340  hoidmvlelem1  46596  tworepnotupword  46887  cjnpoly  46893  m1mod0mod1  47358  m1modmmod  47362  nfermltl2rev  47747  regt1loggt0  48541  rege1logbrege0  48563  nnlog2ge0lt1  48571  eenglngeehlnmlem2  48743  amgmwlem  49807