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 11210	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11174	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11730	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 689	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11163	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11214	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5163	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2098   ≠ wne 2932   class class class wbr 5138  (class class class)co 7401  ℝcr 11104  0cc0 11105  1c1 11106   · cmul 11110   < clt 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-resscn 11162  ax-1cn 11163  ax-icn 11164  ax-addcl 11165  ax-addrcl 11166  ax-mulcl 11167  ax-mulrcl 11168  ax-mulcom 11169  ax-addass 11170  ax-mulass 11171  ax-distr 11172  ax-i2m1 11173  ax-1ne0 11174  ax-1rid 11175  ax-rnegex 11176  ax-rrecex 11177  ax-cnre 11178  ax-pre-lttri 11179  ax-pre-lttrn 11180  ax-pre-ltadd 11181  ax-pre-mulgt0 11182

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-po 5578  df-so 5579  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-er 8698  df-en 8935  df-dom 8936  df-sdom 8937  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443

This theorem is referenced by:  0le1  11733  eqneg  11930  elimgt0  12048  ltp1  12050  ltm1  12052  recgt0  12056  mulgt1  12069  reclt1  12105  recgt1  12106  recgt1i  12107  recp1lt1  12108  recreclt  12109  recgt0ii  12116  inelr  12198  nnge1  12236  nngt0  12239  0nnnALT  12245  nnrecgt0  12251  2pos  12311  3pos  12313  4pos  12315  5pos  12317  6pos  12318  7pos  12319  8pos  12320  9pos  12321  neg1lt0  12325  halflt1  12426  nn0p1gt0  12497  elnnnn0c  12513  elnnz1  12584  nn0lt10b  12620  recnz  12633  1rp  12974  divlt1lt  13039  divle1le  13040  ledivge1le  13041  nnledivrp  13082  xmulrid  13254  0nelfz1  13516  fz10  13518  fzpreddisj  13546  elfznelfzob  13734  1mod  13864  expgt1  14062  ltexp2a  14127  expcan  14130  ltexp2  14131  leexp2  14132  leexp2a  14133  expnbnd  14191  expnlbnd  14192  expnlbnd2  14193  expmulnbnd  14194  discr1  14198  bcn1  14269  hashnn0n0nn  14347  s2fv0  14834  swrd2lsw  14899  2swrd2eqwrdeq  14900  sgn1  15035  resqrex  15193  mulcn2  15536  cvgrat  15825  bpoly4  15999  cos1bnd  16126  sin01gt0  16129  sincos1sgn  16132  ruclem8  16176  p1modz1  16200  nnoddm1d2  16325  sadcadd  16395  dvdsnprmd  16623  isprm7  16641  divdenle  16683  43prm  17053  plendxnocndx  17327  ipostr  18483  srgbinomlem4  20123  abvtrivd  20672  gzrngunit  21294  znidomb  21423  psgnodpmr  21450  thlleOLD  21559  leordtval2  23037  mopnex  24349  dscopn  24403  metnrmlem1a  24695  xrhmph  24793  evth  24806  xlebnum  24812  vitalilem5  25462  vitali  25463  ply1remlem  26019  plyremlem  26157  plyrem  26158  vieta1lem2  26164  reeff1olem  26299  sinhalfpilem  26314  rplogcl  26453  logtayllem  26508  cxplt  26543  cxple  26544  atanlogaddlem  26760  ressatans  26781  rlimcnp  26812  rlimcnp2  26813  cxp2limlem  26823  cxp2lim  26824  cxploglim2  26826  amgmlem  26837  emcllem2  26844  harmonicubnd  26857  fsumharmonic  26859  zetacvg  26862  ftalem1  26920  ftalem2  26921  chpchtsum  27067  chpub  27068  mersenne  27075  perfectlem2  27078  efexple  27129  chebbnd1  27320  dchrmusumlema  27341  dchrvmasumlem2  27346  dchrvmasumiflem1  27349  dchrisum0flblem2  27357  dchrisum0lema  27362  dchrisum0lem1  27364  dchrisum0lem2a  27365  mulog2sumlem1  27382  chpdifbndlem1  27401  chpdifbnd  27403  selberg3lem1  27405  pntrmax  27412  pntrsumo1  27413  pntpbnd1a  27433  pntpbnd2  27435  pntibndlem1  27437  pntlem3  27457  pnt  27462  ostth2lem1  27466  ostth2lem3  27483  ostth2lem4  27484  axcontlem2  28658  wwlksn0s  29550  clwwlkf1  29737  esumcst  33516  hasheuni  33538  ballotlemi1  33956  ballotlemic  33960  sgnnbi  33999  sgnpbi  34000  sgnmulsgp  34004  signsply0  34017  signswch  34027  hgt750lem  34118  unblimceq0  35839  knoppndvlem1  35844  knoppndvlem2  35845  knoppndvlem7  35850  knoppndvlem13  35856  knoppndvlem14  35857  knoppndvlem15  35858  knoppndvlem17  35860  knoppndvlem20  35863  irrdiff  36663  poimirlem22  36966  poimirlem31  36975  asindmre  37027  areacirclem4  37035  60gcd7e1  41329  3lexlogpow5ineq2  41379  aks4d1p1p2  41394  aks4d1p7  41407  aks4d1p8d2  41409  aks4d1p8d3  41410  aks4d1p8  41411  aks4d1p9  41412  sticksstones11  41431  2xp3dxp2ge1d  41481  3cubeslem1  41877  pellexlem2  42023  pellexlem6  42027  pell14qrgt0  42052  elpell1qr2  42065  pellfundex  42079  pellfundrp  42081  rmxypos  42141  relexp01min  42919  imo72b2  43379  radcnvrat  43528  reclt0d  44548  sqrlearg  44717  sumnnodd  44797  liminf10ex  44941  liminfltlimsupex  44948  dvnmul  45110  stoweidlem7  45174  stoweidlem36  45203  stoweidlem38  45205  stoweidlem42  45209  stoweidlem51  45218  stoweidlem59  45226  stirlinglem5  45245  stirlinglem7  45247  stirlinglem10  45250  stirlinglem11  45251  stirlinglem12  45252  stirlinglem15  45255  dirkeritg  45269  fourierdlem11  45285  fourierdlem30  45304  fourierdlem47  45320  fourierdlem79  45352  fourierdlem103  45376  fourierdlem104  45377  fouriersw  45398  etransclem4  45405  etransclem31  45432  etransclem32  45433  etransclem35  45436  etransclem41  45442  salexct2  45506  hoidmvlelem1  45762  tworepnotupword  46051  m1mod0mod1  46488  nfermltl2rev  46862  m1modmmod  47361  regt1loggt0  47376  rege1logbrege0  47398  nnlog2ge0lt1  47406  eenglngeehlnmlem2  47578  amgmwlem  48003