Theorem 0lt1 11764

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 11240	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11203	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11762	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 692	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11192	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11244	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5149	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2109   ≠ wne 2933   class class class wbr 5124  (class class class)co 7410  ℝcr 11133  0cc0 11134  1c1 11135   · cmul 11139   < clt 11274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-reu 3365  df-rab 3421  df-v 3466  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 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-po 5566  df-so 5567  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 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474

This theorem is referenced by:  0le1  11765  eqneg  11966  elimgt0  12084  ltp1  12086  ltm1  12088  recgt0  12092  mulgt1OLD  12105  mulgt1  12108  reclt1  12142  recgt1  12143  recgt1i  12144  recp1lt1  12145  recreclt  12146  recgt0ii  12153  inelr  12235  nnge1  12273  nngt0  12276  0nnnALT  12282  nnrecgt0  12288  2pos  12348  3pos  12350  4pos  12352  5pos  12354  6pos  12355  7pos  12356  8pos  12357  9pos  12358  neg1lt0  12362  halflt1  12463  nn0p1gt0  12535  elnnnn0c  12551  elnnz1  12623  nn0lt10b  12660  recnz  12673  1rp  13017  divlt1lt  13083  divle1le  13084  ledivge1le  13085  nnledivrp  13126  xmulrid  13300  0nelfz1  13565  fz10  13567  fzpreddisj  13595  elfznelfzob  13794  1mod  13925  expgt1  14123  ltexp2a  14189  expcan  14192  ltexp2  14193  leexp2  14194  leexp2a  14195  expnbnd  14255  expnlbnd  14256  expnlbnd2  14257  expmulnbnd  14258  discr1  14262  bcn1  14336  hashnn0n0nn  14414  s2fv0  14911  swrd2lsw  14976  2swrd2eqwrdeq  14977  sgn1  15116  resqrex  15274  mulcn2  15617  cvgrat  15904  bpoly4  16080  cos1bnd  16210  sin01gt0  16213  sincos1sgn  16216  ruclem8  16260  p1modz1  16284  nnoddm1d2  16410  sadcadd  16482  dvdsnprmd  16714  isprm7  16732  divdenle  16773  43prm  17146  plendxnocndx  17403  ipostr  18544  srgbinomlem4  20194  abvtrivd  20797  gzrngunit  21406  znidomb  21527  psgnodpmr  21555  leordtval2  23155  mopnex  24463  dscopn  24517  metnrmlem1a  24803  xrhmph  24901  evth  24914  xlebnum  24920  vitalilem5  25570  vitali  25571  ply1remlem  26127  plyremlem  26269  plyrem  26270  vieta1lem2  26276  reeff1olem  26413  sinhalfpilem  26429  rplogcl  26570  logtayllem  26625  cxplt  26660  cxple  26661  atanlogaddlem  26880  ressatans  26901  rlimcnp  26932  rlimcnp2  26933  cxp2limlem  26943  cxp2lim  26944  cxploglim2  26946  amgmlem  26957  emcllem2  26964  harmonicubnd  26977  fsumharmonic  26979  zetacvg  26982  ftalem1  27040  ftalem2  27041  chpchtsum  27187  chpub  27188  mersenne  27195  perfectlem2  27198  efexple  27249  chebbnd1  27440  dchrmusumlema  27461  dchrvmasumlem2  27466  dchrvmasumiflem1  27469  dchrisum0flblem2  27477  dchrisum0lema  27482  dchrisum0lem1  27484  dchrisum0lem2a  27485  mulog2sumlem1  27502  chpdifbndlem1  27521  chpdifbnd  27523  selberg3lem1  27525  pntrmax  27532  pntrsumo1  27533  pntpbnd1a  27553  pntpbnd2  27555  pntibndlem1  27557  pntlem3  27577  pnt  27582  ostth2lem1  27586  ostth2lem3  27603  ostth2lem4  27604  axcontlem2  28949  wwlksn0s  29848  clwwlkf1  30035  sgnnbi  32822  sgnpbi  32823  sgnmulsgp  32827  cos9thpiminplylem1  33821  cos9thpiminply  33827  esumcst  34099  hasheuni  34121  ballotlemi1  34540  ballotlemic  34544  signsply0  34588  signswch  34598  hgt750lem  34688  unblimceq0  36530  knoppndvlem1  36535  knoppndvlem2  36536  knoppndvlem7  36541  knoppndvlem13  36547  knoppndvlem14  36548  knoppndvlem15  36549  knoppndvlem17  36551  knoppndvlem20  36554  irrdiff  37349  poimirlem22  37671  poimirlem31  37680  asindmre  37732  areacirclem4  37740  60gcd7e1  42023  3lexlogpow5ineq2  42073  aks4d1p1p2  42088  aks4d1p7  42101  aks4d1p8d2  42103  aks4d1p8d3  42104  aks4d1p8  42105  aks4d1p9  42106  aks6d1c5lem3  42155  sticksstones11  42174  aks6d1c6lem1  42188  aks6d1c6lem4  42191  aks6d1c7lem2  42199  explt1d  42341  3cubeslem1  42682  pellexlem2  42828  pellexlem6  42832  pell14qrgt0  42857  elpell1qr2  42870  pellfundex  42884  pellfundrp  42886  rmxypos  42946  relexp01min  43712  imo72b2  44171  radcnvrat  44313  reclt0d  45394  sqrlearg  45562  sumnnodd  45639  liminf10ex  45783  liminfltlimsupex  45790  dvnmul  45952  stoweidlem7  46016  stoweidlem36  46045  stoweidlem38  46047  stoweidlem42  46051  stoweidlem51  46060  stoweidlem59  46068  stirlinglem5  46087  stirlinglem7  46089  stirlinglem10  46092  stirlinglem11  46093  stirlinglem12  46094  stirlinglem15  46097  dirkeritg  46111  fourierdlem11  46127  fourierdlem30  46146  fourierdlem47  46162  fourierdlem79  46194  fourierdlem103  46218  fourierdlem104  46219  fouriersw  46240  etransclem4  46247  etransclem31  46274  etransclem32  46275  etransclem35  46278  etransclem41  46284  salexct2  46348  hoidmvlelem1  46604  tworepnotupword  46895  m1mod0mod1  47363  nfermltl2rev  47737  m1modmmod  48481  regt1loggt0  48496  rege1logbrege0  48518  nnlog2ge0lt1  48526  eenglngeehlnmlem2  48698  amgmwlem  49646