Theorem 0lt1 11767

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 11243	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11206	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11765	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 692	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11195	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11247	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5148	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2107   ≠ wne 2931   class class class wbr 5123  (class class class)co 7413  ℝcr 11136  0cc0 11137  1c1 11138   · cmul 11142   < clt 11277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-resscn 11194  ax-1cn 11195  ax-icn 11196  ax-addcl 11197  ax-addrcl 11198  ax-mulcl 11199  ax-mulrcl 11200  ax-mulcom 11201  ax-addass 11202  ax-mulass 11203  ax-distr 11204  ax-i2m1 11205  ax-1ne0 11206  ax-1rid 11207  ax-rnegex 11208  ax-rrecex 11209  ax-cnre 11210  ax-pre-lttri 11211  ax-pre-lttrn 11212  ax-pre-ltadd 11213  ax-pre-mulgt0 11214

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-po 5572  df-so 5573  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283  df-sub 11476  df-neg 11477

This theorem is referenced by:  0le1  11768  eqneg  11969  elimgt0  12087  ltp1  12089  ltm1  12091  recgt0  12095  mulgt1OLD  12108  mulgt1  12111  reclt1  12145  recgt1  12146  recgt1i  12147  recp1lt1  12148  recreclt  12149  recgt0ii  12156  inelr  12238  nnge1  12276  nngt0  12279  0nnnALT  12285  nnrecgt0  12291  2pos  12351  3pos  12353  4pos  12355  5pos  12357  6pos  12358  7pos  12359  8pos  12360  9pos  12361  neg1lt0  12365  halflt1  12466  nn0p1gt0  12538  elnnnn0c  12554  elnnz1  12626  nn0lt10b  12663  recnz  12676  1rp  13020  divlt1lt  13086  divle1le  13087  ledivge1le  13088  nnledivrp  13129  xmulrid  13303  0nelfz1  13565  fz10  13567  fzpreddisj  13595  elfznelfzob  13794  1mod  13925  expgt1  14123  ltexp2a  14188  expcan  14191  ltexp2  14192  leexp2  14193  leexp2a  14194  expnbnd  14253  expnlbnd  14254  expnlbnd2  14255  expmulnbnd  14256  discr1  14260  bcn1  14334  hashnn0n0nn  14412  s2fv0  14908  swrd2lsw  14973  2swrd2eqwrdeq  14974  sgn1  15113  resqrex  15271  mulcn2  15614  cvgrat  15901  bpoly4  16077  cos1bnd  16205  sin01gt0  16208  sincos1sgn  16211  ruclem8  16255  p1modz1  16279  nnoddm1d2  16405  sadcadd  16477  dvdsnprmd  16709  isprm7  16727  divdenle  16768  43prm  17141  plendxnocndx  17400  ipostr  18543  srgbinomlem4  20194  abvtrivd  20801  gzrngunit  21413  znidomb  21534  psgnodpmr  21562  thlleOLD  21671  leordtval2  23166  mopnex  24476  dscopn  24530  metnrmlem1a  24816  xrhmph  24914  evth  24927  xlebnum  24933  vitalilem5  25583  vitali  25584  ply1remlem  26140  plyremlem  26282  plyrem  26283  vieta1lem2  26289  reeff1olem  26426  sinhalfpilem  26441  rplogcl  26582  logtayllem  26637  cxplt  26672  cxple  26673  atanlogaddlem  26892  ressatans  26913  rlimcnp  26944  rlimcnp2  26945  cxp2limlem  26955  cxp2lim  26956  cxploglim2  26958  amgmlem  26969  emcllem2  26976  harmonicubnd  26989  fsumharmonic  26991  zetacvg  26994  ftalem1  27052  ftalem2  27053  chpchtsum  27199  chpub  27200  mersenne  27207  perfectlem2  27210  efexple  27261  chebbnd1  27452  dchrmusumlema  27473  dchrvmasumlem2  27478  dchrvmasumiflem1  27481  dchrisum0flblem2  27489  dchrisum0lema  27494  dchrisum0lem1  27496  dchrisum0lem2a  27497  mulog2sumlem1  27514  chpdifbndlem1  27533  chpdifbnd  27535  selberg3lem1  27537  pntrmax  27544  pntrsumo1  27545  pntpbnd1a  27565  pntpbnd2  27567  pntibndlem1  27569  pntlem3  27589  pnt  27594  ostth2lem1  27598  ostth2lem3  27615  ostth2lem4  27616  axcontlem2  28910  wwlksn0s  29809  clwwlkf1  29996  esumcst  34023  hasheuni  34045  ballotlemi1  34464  ballotlemic  34468  sgnnbi  34507  sgnpbi  34508  sgnmulsgp  34512  signsply0  34525  signswch  34535  hgt750lem  34625  unblimceq0  36467  knoppndvlem1  36472  knoppndvlem2  36473  knoppndvlem7  36478  knoppndvlem13  36484  knoppndvlem14  36485  knoppndvlem15  36486  knoppndvlem17  36488  knoppndvlem20  36491  irrdiff  37286  poimirlem22  37608  poimirlem31  37617  asindmre  37669  areacirclem4  37677  60gcd7e1  41965  3lexlogpow5ineq2  42015  aks4d1p1p2  42030  aks4d1p7  42043  aks4d1p8d2  42045  aks4d1p8d3  42046  aks4d1p8  42047  aks4d1p9  42048  aks6d1c5lem3  42097  sticksstones11  42116  aks6d1c6lem1  42130  aks6d1c6lem4  42133  aks6d1c7lem2  42141  2xp3dxp2ge1d  42201  explt1d  42321  3cubeslem1  42658  pellexlem2  42804  pellexlem6  42808  pell14qrgt0  42833  elpell1qr2  42846  pellfundex  42860  pellfundrp  42862  rmxypos  42922  relexp01min  43688  imo72b2  44147  radcnvrat  44290  reclt0d  45355  sqrlearg  45523  sumnnodd  45602  liminf10ex  45746  liminfltlimsupex  45753  dvnmul  45915  stoweidlem7  45979  stoweidlem36  46008  stoweidlem38  46010  stoweidlem42  46014  stoweidlem51  46023  stoweidlem59  46031  stirlinglem5  46050  stirlinglem7  46052  stirlinglem10  46055  stirlinglem11  46056  stirlinglem12  46057  stirlinglem15  46060  dirkeritg  46074  fourierdlem11  46090  fourierdlem30  46109  fourierdlem47  46125  fourierdlem79  46157  fourierdlem103  46181  fourierdlem104  46182  fouriersw  46203  etransclem4  46210  etransclem31  46237  etransclem32  46238  etransclem35  46241  etransclem41  46247  salexct2  46311  hoidmvlelem1  46567  tworepnotupword  46858  m1mod0mod1  47314  nfermltl2rev  47688  m1modmmod  48400  regt1loggt0  48415  rege1logbrege0  48437  nnlog2ge0lt1  48445  eenglngeehlnmlem2  48617  amgmwlem  49329