Theorem 0lt1 11732

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 11204	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11165	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11730	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 704	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11154	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11209	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5137	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2149   ≠ wne 2964   class class class wbr 5110  (class class class)co 7408  ℝcr 11095  0cc0 11096  1c1 11097   · cmul 11101   < clt 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-1cn 11154  ax-icn 11155  ax-addcl 11156  ax-addrcl 11157  ax-mulcl 11158  ax-mulrcl 11159  ax-mulcom 11160  ax-addass 11161  ax-mulass 11162  ax-distr 11163  ax-i2m1 11164  ax-1ne0 11165  ax-1rid 11166  ax-rnegex 11167  ax-rrecex 11168  ax-cnre 11169  ax-pre-lttri 11170  ax-pre-lttrn 11171  ax-pre-ltadd 11172  ax-pre-mulgt0 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245  df-sub 11439  df-neg 11440

This theorem is referenced by:  0le1  11733  eqneg  11931  elimgt0  12049  ltp1  12051  ltm1  12053  recgt0  12057  mulgt1  12072  reclt1  12106  recgt1  12107  recgt1i  12108  recp1lt1  12109  recreclt  12110  recgt0ii  12117  neg1lt0  12202  nnge1  12260  nngt0  12263  0nnnALT  12269  nnrecgt0  12275  2posOLD  12342  halflt1  12457  nn0p1gt0  12529  elnnnn0c  12545  elnnz1  12616  nn0lt10b  12654  recnz  12667  1rp  13016  divlt1lt  13083  divle1le  13084  ledivge1le  13085  nnledivrp  13126  xmulrid  13301  0nelfz1  13567  fz10  13569  fzpreddisj  13597  elfznelfzob  13799  1mod  13932  expgt1  14132  ltexp2a  14198  expcan  14201  ltexp2  14202  leexp2  14203  leexp2a  14204  expnbnd  14264  expnlbnd  14265  expnlbnd2  14266  expmulnbnd  14267  discr1  14271  bcn1  14345  hashnn0n0nn  14423  s2fv0  14920  swrd2lsw  14985  2swrd2eqwrdeq  14986  sgn1  15125  sgnnbi  15137  sgnpbi  15138  resqrex  15297  mulcn2  15643  cvgrat  15933  bpoly4  16109  cos1bnd  16239  sin01gt0  16242  sincos1sgn  16245  ruclem8  16289  p1modz1  16313  nnoddm1d2  16440  sadcadd  16512  dvdsnprmd  16744  isprm7  16763  divdenle  16804  43prm  17178  plendxnocndx  17433  ipostr  18581  srgbinomlem4  20307  abvtrivd  20909  gzrngunit  21548  znidomb  21676  psgnodpmr  21705  leordtval2  23334  mopnex  24641  dscopn  24695  metnrmlem1a  24981  xrhmph  25071  evth  25083  xlebnum  25089  vitalilem5  25736  vitali  25737  ply1remlem  26287  plyremlem  26430  plyrem  26431  vieta1lem2  26437  reeff1olem  26571  sinhalfpilem  26590  rplogcl  26731  logtayllem  26786  cxplt  26821  cxple  26822  atanlogaddlem  27040  ressatans  27061  rlimcnp  27092  rlimcnp2  27093  cxp2limlem  27102  cxp2lim  27103  cxploglim2  27105  amgmlem  27116  emcllem2  27123  harmonicubnd  27136  fsumharmonic  27138  zetacvg  27141  ftalem1  27199  ftalem2  27200  chpchtsum  27345  chpub  27346  mersenne  27353  perfectlem2  27356  efexple  27407  chebbnd1  27598  dchrmusumlema  27619  dchrvmasumlem2  27624  dchrvmasumiflem1  27627  dchrisum0flblem2  27635  dchrisum0lema  27640  dchrisum0lem1  27642  dchrisum0lem2a  27643  mulog2sumlem1  27660  chpdifbndlem1  27679  chpdifbnd  27681  selberg3lem1  27683  pntrmax  27690  pntrsumo1  27691  pntpbnd1a  27711  pntpbnd2  27713  pntibndlem1  27715  pntlem3  27735  pnt  27740  ostth2lem1  27744  ostth2lem3  27761  ostth2lem4  27762  axcontlem2  29252  wwlksn0s  30147  clwwlkf1  30337  sgnmulsgp  33113  vietadeg1  33909  cos9thpiminplylem1  34113  cos9thpiminply  34119  esumcst  34394  hasheuni  34416  ballotlemi1  34834  ballotlemic  34838  signsply0  34879  signswch  34889  hgt750lem  34979  unblimceq0  36981  knoppndvlem1  36986  knoppndvlem2  36987  knoppndvlem7  36992  knoppndvlem13  36998  knoppndvlem14  36999  knoppndvlem15  37000  knoppndvlem17  37002  knoppndvlem20  37005  irrdiff  37853  poimirlem22  38176  poimirlem31  38185  asindmre  38237  areacirclem4  38245  60gcd7e1  42657  3lexlogpow5ineq2  42707  aks4d1p1p2  42722  aks4d1p7  42735  aks4d1p8d2  42737  aks4d1p8d3  42738  aks4d1p8  42739  aks4d1p9  42740  aks6d1c5lem3  42789  sticksstones11  42808  aks6d1c6lem1  42822  aks6d1c6lem4  42825  aks6d1c7lem2  42833  explt1d  42969  3cubeslem1  43302  pellexlem2  43444  pellexlem6  43448  pell14qrgt0  43473  elpell1qr2  43486  pellfundex  43500  pellfundrp  43502  rmxypos  43561  relexp01min  44326  imo72b2  44785  radcnvrat  44911  reclt0d  45989  sqrlearg  46156  sumnnodd  46233  liminf10ex  46375  liminfltlimsupex  46382  dvnmul  46544  stoweidlem7  46608  stoweidlem36  46637  stoweidlem38  46639  stoweidlem42  46643  stoweidlem51  46652  stoweidlem59  46660  stirlinglem5  46679  stirlinglem7  46681  stirlinglem10  46684  stirlinglem11  46685  stirlinglem12  46686  stirlinglem15  46689  dirkeritg  46703  fourierdlem11  46719  fourierdlem30  46738  fourierdlem47  46754  fourierdlem79  46786  fourierdlem103  46810  fourierdlem104  46811  fouriersw  46832  etransclem4  46839  etransclem31  46866  etransclem32  46867  etransclem35  46870  etransclem41  46876  salexct2  46940  hoidmvlelem1  47196  cjnpoly  47510  m1mod0mod1  47981  m1modmmod  47985  muldvdsfacgt  48007  muldvdsfacm1  48008  nfermltl2rev  48392  regt1loggt0  49196  rege1logbrege0  49218  nnlog2ge0lt1  49226  eenglngeehlnmlem2  49398  amgmwlem  50471