Theorem 0lt1 11747

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 11219	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11180	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11745	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 705	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11169	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11224	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5138	1 ⊢ 0 < 1

This proof depends on syntax axioms:   ∈ wcel 2146   ≠ wne 2960   class class class wbr 5111  (class class class)co 7416  ℝcr 11110  0cc0 11111  1c1 11112   · cmul 11116   < clt 11254

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-resscn 11168  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-mulcom 11175  ax-addass 11176  ax-mulass 11177  ax-distr 11178  ax-i2m1 11179  ax-1ne0 11180  ax-1rid 11181  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184  ax-pre-lttri 11185  ax-pre-lttrn 11186  ax-pre-ltadd 11187  ax-pre-mulgt0 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11454  df-neg 11455

This theorem is used by:  0le1  11748  eqneg  11946  elimgt0  12064  ltp1  12066  ltm1  12068  recgt0  12072  mulgt1  12087  reclt1  12121  recgt1  12122  recgt1i  12123  recp1lt1  12124  recreclt  12125  recgt0ii  12132  neg1lt0  12217  nnge1  12275  nngt0  12278  0nnnALT  12284  nnrecgt0  12290  2posOLD  12357  halflt1  12472  nn0p1gt0  12544  elnnnn0c  12560  elnnz1  12631  nn0lt10b  12670  recnz  12683  1rp  13032  divlt1lt  13099  divle1le  13100  ledivge1le  13101  nnledivrp  13142  xmulrid  13317  0nelfz1  13583  fz10  13585  fzpreddisj  13614  elfznelfzob  13816  1mod  13950  expgt1  14150  ltexp2a  14216  expcan  14219  ltexp2  14220  leexp2  14221  leexp2a  14222  expnbnd  14282  expnlbnd  14283  expnlbnd2  14284  expmulnbnd  14285  discr1  14289  bcn1  14363  hashnn0n0nn  14441  s2fv0  14944  swrd2lsw  15009  2swrd2eqwrdeq  15010  sgn1  15149  sgnnbi  15161  sgnpbi  15162  resqrex  15321  mulcn2  15667  cvgrat  15956  bpoly4  16131  cos1bnd  16261  sin01gt0  16264  sincos1sgn  16267  ruclem8  16311  p1modz1  16335  nnoddm1d2  16462  sadcadd  16534  dvdsnprmd  16766  isprm7  16785  divdenle  16826  43prm  17200  plendxnocndx  17455  ipostr  18603  srgbinomlem4  20335  abvtrivd  20965  gzrngunit  21613  znidomb  21741  psgnodpmr  21770  leordtval2  23399  mopnex  24707  dscopn  24761  metnrmlem1a  25047  xrhmph  25137  evth  25149  xlebnum  25155  vitalilem5  25802  vitali  25803  ply1remlem  26353  plyremlem  26496  plyrem  26497  vieta1lem2  26503  reeff1olem  26640  sinhalfpilem  26659  rplogcl  26800  logtayllem  26855  cxplt  26890  cxple  26891  atanlogaddlem  27109  ressatans  27130  rlimcnp  27161  rlimcnp2  27162  cxp2limlem  27171  cxp2lim  27172  cxploglim2  27174  amgmlem  27185  emcllem2  27192  harmonicubnd  27205  fsumharmonic  27207  zetacvg  27210  ftalem1  27268  ftalem2  27269  chpchtsum  27414  chpub  27415  mersenne  27422  perfectlem2  27425  efexple  27476  chebbnd1  27667  dchrmusumlema  27688  dchrvmasumlem2  27693  dchrvmasumiflem1  27696  dchrisum0flblem2  27704  dchrisum0lema  27709  dchrisum0lem1  27711  dchrisum0lem2a  27712  mulog2sumlem1  27729  chpdifbndlem1  27748  chpdifbnd  27750  selberg3lem1  27752  pntrmax  27759  pntrsumo1  27760  pntpbnd1a  27780  pntpbnd2  27782  pntibndlem1  27784  pntlem3  27804  pnt  27809  ostth2lem1  27813  ostth2lem3  27830  ostth2lem4  27831  axcontlem2  29346  wwlksn0s  30253  clwwlkf1  30443  sgnmulsgp  33222  vietadeg1  34008  cos9thpiminplylem1  34212  cos9thpiminply  34218  esumcst  34493  hasheuni  34515  ballotlemi1  34934  ballotlemic  34938  signsply0  34979  signswch  34989  hgt750lem  35079  unblimceq0  37129  knoppndvlem1  37134  knoppndvlem2  37135  knoppndvlem7  37140  knoppndvlem13  37146  knoppndvlem14  37147  knoppndvlem15  37148  knoppndvlem17  37150  knoppndvlem20  37153  irrdiff  38003  poimirlem22  38326  poimirlem31  38335  asindmre  38387  areacirclem4  38395  60gcd7e1  42805  3lexlogpow5ineq2  42855  aks4d1p1p2  42870  aks4d1p7  42883  aks4d1p8d2  42885  aks4d1p8d3  42886  aks4d1p8  42887  aks4d1p9  42888  aks6d1c5lem3  42937  sticksstones11  42956  aks6d1c6lem1  42970  aks6d1c6lem4  42973  aks6d1c7lem2  42981  explt1d  43117  3cubeslem1  43448  pellexlem2  43590  pellexlem6  43594  pell14qrgt0  43619  elpell1qr2  43632  pellfundex  43646  pellfundrp  43648  rmxypos  43707  relexp01min  44472  imo72b2  44931  radcnvrat  45057  reclt0d  46135  sqrlearg  46302  sumnnodd  46379  liminf10ex  46521  liminfltlimsupex  46528  dvnmul  46690  stoweidlem7  46754  stoweidlem36  46783  stoweidlem38  46785  stoweidlem42  46789  stoweidlem51  46798  stoweidlem59  46806  stirlinglem5  46825  stirlinglem7  46827  stirlinglem10  46830  stirlinglem11  46831  stirlinglem12  46832  stirlinglem15  46835  dirkeritg  46849  fourierdlem11  46865  fourierdlem30  46884  fourierdlem47  46900  fourierdlem79  46932  fourierdlem103  46956  fourierdlem104  46957  fouriersw  46978  etransclem4  46985  etransclem31  47012  etransclem32  47013  etransclem35  47016  etransclem41  47022  salexct2  47086  hoidmvlelem1  47342  cjnpoly  47659  m1mod0mod1  48130  m1modmmod  48134  muldvdsfacgt  48156  muldvdsfacm1  48157  nfermltl2rev  48541  regt1loggt0  49349  rege1logbrege0  49371  nnlog2ge0lt1  49379  eenglngeehlnmlem2  49551  amgmwlem  50683