Theorem 0lt1 11783

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 11259	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11222	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11781	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 692	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11211	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11263	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5173	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2106   ≠ wne 2938   class class class wbr 5148  (class class class)co 7431  ℝcr 11152  0cc0 11153  1c1 11154   · cmul 11158   < clt 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-po 5597  df-so 5598  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493

This theorem is referenced by:  0le1  11784  eqneg  11985  elimgt0  12103  ltp1  12105  ltm1  12107  recgt0  12111  mulgt1OLD  12124  mulgt1  12127  reclt1  12161  recgt1  12162  recgt1i  12163  recp1lt1  12164  recreclt  12165  recgt0ii  12172  inelr  12254  nnge1  12292  nngt0  12295  0nnnALT  12301  nnrecgt0  12307  2pos  12367  3pos  12369  4pos  12371  5pos  12373  6pos  12374  7pos  12375  8pos  12376  9pos  12377  neg1lt0  12381  halflt1  12482  nn0p1gt0  12553  elnnnn0c  12569  elnnz1  12641  nn0lt10b  12678  recnz  12691  1rp  13036  divlt1lt  13102  divle1le  13103  ledivge1le  13104  nnledivrp  13145  xmulrid  13318  0nelfz1  13580  fz10  13582  fzpreddisj  13610  elfznelfzob  13809  1mod  13940  expgt1  14138  ltexp2a  14203  expcan  14206  ltexp2  14207  leexp2  14208  leexp2a  14209  expnbnd  14268  expnlbnd  14269  expnlbnd2  14270  expmulnbnd  14271  discr1  14275  bcn1  14349  hashnn0n0nn  14427  s2fv0  14923  swrd2lsw  14988  2swrd2eqwrdeq  14989  sgn1  15128  resqrex  15286  mulcn2  15629  cvgrat  15916  bpoly4  16092  cos1bnd  16220  sin01gt0  16223  sincos1sgn  16226  ruclem8  16270  p1modz1  16294  nnoddm1d2  16420  sadcadd  16492  dvdsnprmd  16724  isprm7  16742  divdenle  16783  43prm  17156  plendxnocndx  17430  ipostr  18587  srgbinomlem4  20247  abvtrivd  20850  gzrngunit  21469  znidomb  21598  psgnodpmr  21626  thlleOLD  21735  leordtval2  23236  mopnex  24548  dscopn  24602  metnrmlem1a  24894  xrhmph  24992  evth  25005  xlebnum  25011  vitalilem5  25661  vitali  25662  ply1remlem  26219  plyremlem  26361  plyrem  26362  vieta1lem2  26368  reeff1olem  26505  sinhalfpilem  26520  rplogcl  26661  logtayllem  26716  cxplt  26751  cxple  26752  atanlogaddlem  26971  ressatans  26992  rlimcnp  27023  rlimcnp2  27024  cxp2limlem  27034  cxp2lim  27035  cxploglim2  27037  amgmlem  27048  emcllem2  27055  harmonicubnd  27068  fsumharmonic  27070  zetacvg  27073  ftalem1  27131  ftalem2  27132  chpchtsum  27278  chpub  27279  mersenne  27286  perfectlem2  27289  efexple  27340  chebbnd1  27531  dchrmusumlema  27552  dchrvmasumlem2  27557  dchrvmasumiflem1  27560  dchrisum0flblem2  27568  dchrisum0lema  27573  dchrisum0lem1  27575  dchrisum0lem2a  27576  mulog2sumlem1  27593  chpdifbndlem1  27612  chpdifbnd  27614  selberg3lem1  27616  pntrmax  27623  pntrsumo1  27624  pntpbnd1a  27644  pntpbnd2  27646  pntibndlem1  27648  pntlem3  27668  pnt  27673  ostth2lem1  27677  ostth2lem3  27694  ostth2lem4  27695  axcontlem2  28995  wwlksn0s  29891  clwwlkf1  30078  esumcst  34044  hasheuni  34066  ballotlemi1  34484  ballotlemic  34488  sgnnbi  34527  sgnpbi  34528  sgnmulsgp  34532  signsply0  34545  signswch  34555  hgt750lem  34645  unblimceq0  36490  knoppndvlem1  36495  knoppndvlem2  36496  knoppndvlem7  36501  knoppndvlem13  36507  knoppndvlem14  36508  knoppndvlem15  36509  knoppndvlem17  36511  knoppndvlem20  36514  irrdiff  37309  poimirlem22  37629  poimirlem31  37638  asindmre  37690  areacirclem4  37698  60gcd7e1  41987  3lexlogpow5ineq2  42037  aks4d1p1p2  42052  aks4d1p7  42065  aks4d1p8d2  42067  aks4d1p8d3  42068  aks4d1p8  42069  aks4d1p9  42070  aks6d1c5lem3  42119  sticksstones11  42138  aks6d1c6lem1  42152  aks6d1c6lem4  42155  aks6d1c7lem2  42163  2xp3dxp2ge1d  42223  explt1d  42337  3cubeslem1  42672  pellexlem2  42818  pellexlem6  42822  pell14qrgt0  42847  elpell1qr2  42860  pellfundex  42874  pellfundrp  42876  rmxypos  42936  relexp01min  43703  imo72b2  44162  radcnvrat  44310  reclt0d  45337  sqrlearg  45506  sumnnodd  45586  liminf10ex  45730  liminfltlimsupex  45737  dvnmul  45899  stoweidlem7  45963  stoweidlem36  45992  stoweidlem38  45994  stoweidlem42  45998  stoweidlem51  46007  stoweidlem59  46015  stirlinglem5  46034  stirlinglem7  46036  stirlinglem10  46039  stirlinglem11  46040  stirlinglem12  46041  stirlinglem15  46044  dirkeritg  46058  fourierdlem11  46074  fourierdlem30  46093  fourierdlem47  46109  fourierdlem79  46141  fourierdlem103  46165  fourierdlem104  46166  fouriersw  46187  etransclem4  46194  etransclem31  46221  etransclem32  46222  etransclem35  46225  etransclem41  46231  salexct2  46295  hoidmvlelem1  46551  tworepnotupword  46840  m1mod0mod1  47294  nfermltl2rev  47668  m1modmmod  48371  regt1loggt0  48386  rege1logbrege0  48408  nnlog2ge0lt1  48416  eenglngeehlnmlem2  48588  amgmwlem  49033