Theorem 0lt1 11838

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 11308	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11269	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11836	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 705	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11258	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11313	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5129	1 ⊢ 0 < 1

This proof depends on syntax axioms:   ∈ wcel 2144   ≠ wne 2955   class class class wbr 5102  (class class class)co 7420  ℝcr 11199  0cc0 11200  1c1 11201   · cmul 11205   < clt 11343

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276  ax-pre-mulgt0 11277

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-sub 11543  df-neg 11544

This theorem is used by:  0le1  11839  eqneg  12037  elimgt0  12155  ltp1  12157  ltm1  12159  recgt0  12163  mulgt1  12178  reclt1  12212  recgt1  12213  recgt1i  12214  recp1lt1  12215  recreclt  12216  recgt0ii  12223  neg1lt0  12308  nnge1  12366  nngt0  12369  0nnnALT  12375  nnrecgt0  12381  2posOLD  12448  halflt1  12563  nn0p1gt0  12635  elnnnn0c  12651  elnnz1  12722  nn0lt10b  12761  recnz  12774  1rp  13124  divlt1lt  13191  divle1le  13192  ledivge1le  13193  nnledivrp  13234  xmulrid  13409  0nelfz1  13676  fz10  13678  fzpreddisj  13707  elfznelfzob  13909  1mod  14043  expgt1  14243  ltexp2a  14309  expcan  14312  ltexp2  14313  leexp2  14314  leexp2a  14315  expnbnd  14376  expnlbnd  14377  expnlbnd2  14378  expmulnbnd  14379  discr1  14383  bcn1  14457  hashnn0n0nn  14535  s2fv0  15038  swrd2lsw  15105  2swrd2eqwrdeq  15106  sgn1  15245  sgnnbi  15257  sgnpbi  15258  resqrex  15417  mulcn2  15763  cvgrat  16052  bpoly4  16225  cos1bnd  16355  sin01gt0  16358  sincos1sgn  16361  ruclem8  16405  p1modz1  16429  nnoddm1d2  16556  sadcadd  16628  dvdsnprmd  16865  isprm7  16884  divdenle  16925  43prm  17300  plendxnocndx  17555  ipostr  18703  srgbinomlem4  20455  abvtrivd  21089  gzrngunit  21739  znidomb  21867  psgnodpmr  21896  leordtval2  23530  mopnex  24838  dscopn  24892  metnrmlem1a  25178  xrhmph  25268  evth  25280  xlebnum  25286  vitalilem5  25933  vitali  25934  ply1remlem  26483  plyremlem  26625  plyrem  26626  vieta1lem2  26634  reeff1olem  26773  sinhalfpilem  26792  rplogcl  26932  logtayllem  26987  cxplt  27022  cxple  27023  atanlogaddlem  27241  ressatans  27262  rlimcnp  27293  rlimcnp2  27294  cxp2limlem  27303  cxp2lim  27304  cxploglim2  27306  amgmlem  27317  emcllem2  27324  harmonicubnd  27337  fsumharmonic  27339  zetacvg  27342  ftalem1  27400  ftalem2  27401  chpchtsum  27546  chpub  27547  mersenne  27554  perfectlem2  27557  efexple  27608  chebbnd1  27799  dchrmusumlema  27820  dchrvmasumlem2  27825  dchrvmasumiflem1  27828  dchrisum0flblem2  27836  dchrisum0lema  27841  dchrisum0lem1  27843  dchrisum0lem2a  27844  mulog2sumlem1  27861  chpdifbndlem1  27880  chpdifbnd  27882  selberg3lem1  27884  pntrmax  27891  pntrsumo1  27892  pntpbnd1a  27912  pntpbnd2  27914  pntibndlem1  27916  pntlem3  27936  pnt  27941  ostth2lem1  27945  ostth2lem3  27962  ostth2lem4  27963  axcontlem2  29543  wwlksn0s  30450  clwwlkf1  30640  sgnmulsgp  33423  vietadeg1  34210  cos9thpiminplylem1  34414  cos9thpiminply  34420  esumcst  34695  hasheuni  34717  ballotlemi1  35135  ballotlemic  35139  signsply0  35180  signswch  35190  hgt750lem  35280  unblimceq0  37373  knoppndvlem1  37378  knoppndvlem2  37379  knoppndvlem7  37384  knoppndvlem13  37390  knoppndvlem14  37391  knoppndvlem15  37392  knoppndvlem17  37394  knoppndvlem20  37397  irrdiff  38248  poimirlem22  38561  poimirlem31  38570  asindmre  38622  areacirclem4  38630  60gcd7e1  43056  3lexlogpow5ineq2  43106  aks4d1p1p2  43121  aks4d1p7  43134  aks4d1p8d2  43136  aks4d1p8d3  43137  aks4d1p8  43138  aks4d1p9  43139  aks6d1c5lem3  43188  sticksstones11  43207  aks6d1c6lem1  43221  aks6d1c6lem4  43224  aks6d1c7lem2  43232  explt1d  43381  3cubeslem1  43695  pellexlem2  43837  pellexlem6  43841  pell14qrgt0  43866  elpell1qr2  43879  pellfundex  43893  pellfundrp  43895  rmxypos  43954  relexp01min  44713  imo72b2  45172  radcnvrat  45298  reclt0d  46398  sqrlearg  46565  sumnnodd  46642  liminf10ex  46784  liminfltlimsupex  46791  dvnmul  46953  stoweidlem7  47017  stoweidlem36  47046  stoweidlem38  47048  stoweidlem42  47052  stoweidlem51  47061  stoweidlem59  47069  stirlinglem5  47088  stirlinglem7  47090  stirlinglem10  47093  stirlinglem11  47094  stirlinglem12  47095  stirlinglem15  47098  dirkeritg  47112  fourierdlem11  47128  fourierdlem30  47147  fourierdlem47  47163  fourierdlem79  47195  fourierdlem103  47219  fourierdlem104  47220  fouriersw  47241  etransclem4  47248  etransclem31  47275  etransclem32  47276  etransclem35  47279  etransclem41  47285  salexct2  47349  hoidmvlelem1  47605  cjnpoly  47939  m1mod0mod1  48430  m1modmmod  48434  muldvdsfacgt  48456  muldvdsfacm1  48457  nfermltl2rev  48841  regt1loggt0  49648  rege1logbrege0  49670  nnlog2ge0lt1  49678  eenglngeehlnmlem2  49850  amgmwlem  50987