Theorem 0lt1 11731

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 11203	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11164	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11729	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 704	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11153	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11208	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5136	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2143   ≠ wne 2958   class class class wbr 5109  (class class class)co 7410  ℝcr 11094  0cc0 11095  1c1 11096   · cmul 11100   < clt 11238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-po 5569  df-so 5570  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  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 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439

This theorem is referenced by:  0le1  11732  eqneg  11930  elimgt0  12048  ltp1  12050  ltm1  12052  recgt0  12056  mulgt1  12071  reclt1  12105  recgt1  12106  recgt1i  12107  recp1lt1  12108  recreclt  12109  recgt0ii  12116  neg1lt0  12201  nnge1  12259  nngt0  12262  0nnnALT  12268  nnrecgt0  12274  2posOLD  12341  halflt1  12456  nn0p1gt0  12528  elnnnn0c  12544  elnnz1  12615  nn0lt10b  12653  recnz  12666  1rp  13015  divlt1lt  13082  divle1le  13083  ledivge1le  13084  nnledivrp  13125  xmulrid  13300  0nelfz1  13566  fz10  13568  fzpreddisj  13597  elfznelfzob  13799  1mod  13932  expgt1  14132  ltexp2a  14198  expcan  14201  ltexp2  14202  leexp2  14203  leexp2a  14204  expnbnd  14264  expnlbnd  14265  expnlbnd2  14266  expmulnbnd  14267  discr1  14271  bcn1  14345  hashnn0n0nn  14423  s2fv0  14920  swrd2lsw  14985  2swrd2eqwrdeq  14986  sgn1  15125  sgnnbi  15137  sgnpbi  15138  resqrex  15297  mulcn2  15643  cvgrat  15933  bpoly4  16108  cos1bnd  16238  sin01gt0  16241  sincos1sgn  16244  ruclem8  16288  p1modz1  16312  nnoddm1d2  16439  sadcadd  16511  dvdsnprmd  16743  isprm7  16762  divdenle  16803  43prm  17177  plendxnocndx  17432  ipostr  18580  srgbinomlem4  20306  abvtrivd  20935  gzrngunit  21583  znidomb  21711  psgnodpmr  21740  leordtval2  23369  mopnex  24676  dscopn  24730  metnrmlem1a  25016  xrhmph  25106  evth  25118  xlebnum  25124  vitalilem5  25771  vitali  25772  ply1remlem  26322  plyremlem  26465  plyrem  26466  vieta1lem2  26472  reeff1olem  26609  sinhalfpilem  26628  rplogcl  26769  logtayllem  26824  cxplt  26859  cxple  26860  atanlogaddlem  27078  ressatans  27099  rlimcnp  27130  rlimcnp2  27131  cxp2limlem  27140  cxp2lim  27141  cxploglim2  27143  amgmlem  27154  emcllem2  27161  harmonicubnd  27174  fsumharmonic  27176  zetacvg  27179  ftalem1  27237  ftalem2  27238  chpchtsum  27383  chpub  27384  mersenne  27391  perfectlem2  27394  efexple  27445  chebbnd1  27636  dchrmusumlema  27657  dchrvmasumlem2  27662  dchrvmasumiflem1  27665  dchrisum0flblem2  27673  dchrisum0lema  27678  dchrisum0lem1  27680  dchrisum0lem2a  27681  mulog2sumlem1  27698  chpdifbndlem1  27717  chpdifbnd  27719  selberg3lem1  27721  pntrmax  27728  pntrsumo1  27729  pntpbnd1a  27749  pntpbnd2  27751  pntibndlem1  27753  pntlem3  27773  pnt  27778  ostth2lem1  27782  ostth2lem3  27799  ostth2lem4  27800  axcontlem2  29315  wwlksn0s  30210  clwwlkf1  30400  sgnmulsgp  33176  vietadeg1  33968  cos9thpiminplylem1  34172  cos9thpiminply  34178  esumcst  34453  hasheuni  34475  ballotlemi1  34893  ballotlemic  34897  signsply0  34938  signswch  34948  hgt750lem  35038  unblimceq0  37096  knoppndvlem1  37101  knoppndvlem2  37102  knoppndvlem7  37107  knoppndvlem13  37113  knoppndvlem14  37114  knoppndvlem15  37115  knoppndvlem17  37117  knoppndvlem20  37120  irrdiff  37970  poimirlem22  38293  poimirlem31  38302  asindmre  38354  areacirclem4  38362  60gcd7e1  42772  3lexlogpow5ineq2  42822  aks4d1p1p2  42837  aks4d1p7  42850  aks4d1p8d2  42852  aks4d1p8d3  42853  aks4d1p8  42854  aks4d1p9  42855  aks6d1c5lem3  42904  sticksstones11  42923  aks6d1c6lem1  42937  aks6d1c6lem4  42940  aks6d1c7lem2  42948  explt1d  43084  3cubeslem1  43415  pellexlem2  43557  pellexlem6  43561  pell14qrgt0  43586  elpell1qr2  43599  pellfundex  43613  pellfundrp  43615  rmxypos  43674  relexp01min  44439  imo72b2  44898  radcnvrat  45024  reclt0d  46102  sqrlearg  46269  sumnnodd  46346  liminf10ex  46488  liminfltlimsupex  46495  dvnmul  46657  stoweidlem7  46721  stoweidlem36  46750  stoweidlem38  46752  stoweidlem42  46756  stoweidlem51  46765  stoweidlem59  46773  stirlinglem5  46792  stirlinglem7  46794  stirlinglem10  46797  stirlinglem11  46798  stirlinglem12  46799  stirlinglem15  46802  dirkeritg  46816  fourierdlem11  46832  fourierdlem30  46851  fourierdlem47  46867  fourierdlem79  46899  fourierdlem103  46923  fourierdlem104  46924  fouriersw  46945  etransclem4  46952  etransclem31  46979  etransclem32  46980  etransclem35  46983  etransclem41  46989  salexct2  47053  hoidmvlelem1  47309  cjnpoly  47626  m1mod0mod1  48097  m1modmmod  48101  muldvdsfacgt  48123  muldvdsfacm1  48124  nfermltl2rev  48508  regt1loggt0  49316  rege1logbrege0  49338  nnlog2ge0lt1  49346  eenglngeehlnmlem2  49518  amgmwlem  50622