Theorem 0lt1 11732

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 11210	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11175	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11730	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 690	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11164	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11214	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5172	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2106   ≠ wne 2940   class class class wbr 5147  (class class class)co 7405  ℝcr 11105  0cc0 11106  1c1 11107   · cmul 11111   < clt 11244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-so 5588  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443

This theorem is referenced by:  0le1  11733  eqneg  11930  elimgt0  12048  ltp1  12050  ltm1  12052  recgt0  12056  mulgt1  12069  reclt1  12105  recgt1  12106  recgt1i  12107  recp1lt1  12108  recreclt  12109  recgt0ii  12116  inelr  12198  nnge1  12236  nngt0  12239  0nnnALT  12245  nnrecgt0  12251  2pos  12311  3pos  12313  4pos  12315  5pos  12317  6pos  12318  7pos  12319  8pos  12320  9pos  12321  neg1lt0  12325  halflt1  12426  nn0p1gt0  12497  elnnnn0c  12513  elnnz1  12584  nn0lt10b  12620  recnz  12633  1rp  12974  divlt1lt  13039  divle1le  13040  ledivge1le  13041  nnledivrp  13082  xmulrid  13254  0nelfz1  13516  fz10  13518  fzpreddisj  13546  elfznelfzob  13734  1mod  13864  expgt1  14062  ltexp2a  14127  expcan  14130  ltexp2  14131  leexp2  14132  leexp2a  14133  expnbnd  14191  expnlbnd  14192  expnlbnd2  14193  expmulnbnd  14194  discr1  14198  bcn1  14269  hashnn0n0nn  14347  s2fv0  14834  swrd2lsw  14899  2swrd2eqwrdeq  14900  sgn1  15035  resqrex  15193  mulcn2  15536  cvgrat  15825  bpoly4  15999  cos1bnd  16126  sin01gt0  16129  sincos1sgn  16132  ruclem8  16176  p1modz1  16200  nnoddm1d2  16325  sadcadd  16395  dvdsnprmd  16623  isprm7  16641  divdenle  16681  43prm  17051  plendxnocndx  17325  ipostr  18478  srgbinomlem4  20045  abvtrivd  20440  gzrngunit  21003  znidomb  21108  psgnodpmr  21134  thlleOLD  21243  leordtval2  22707  mopnex  24019  dscopn  24073  metnrmlem1a  24365  xrhmph  24454  evth  24466  xlebnum  24472  vitalilem5  25120  vitali  25121  ply1remlem  25671  plyremlem  25808  plyrem  25809  vieta1lem2  25815  reeff1olem  25949  sinhalfpilem  25964  rplogcl  26103  logtayllem  26158  cxplt  26193  cxple  26194  atanlogaddlem  26407  ressatans  26428  rlimcnp  26459  rlimcnp2  26460  cxp2limlem  26469  cxp2lim  26470  cxploglim2  26472  amgmlem  26483  emcllem2  26490  harmonicubnd  26503  fsumharmonic  26505  zetacvg  26508  ftalem1  26566  ftalem2  26567  chpchtsum  26711  chpub  26712  mersenne  26719  perfectlem2  26722  efexple  26773  chebbnd1  26964  dchrmusumlema  26985  dchrvmasumlem2  26990  dchrvmasumiflem1  26993  dchrisum0flblem2  27001  dchrisum0lema  27006  dchrisum0lem1  27008  dchrisum0lem2a  27009  mulog2sumlem1  27026  chpdifbndlem1  27045  chpdifbnd  27047  selberg3lem1  27049  pntrmax  27056  pntrsumo1  27057  pntpbnd1a  27077  pntpbnd2  27079  pntibndlem1  27081  pntlem3  27101  pnt  27106  ostth2lem1  27110  ostth2lem3  27127  ostth2lem4  27128  axcontlem2  28212  wwlksn0s  29104  clwwlkf1  29291  esumcst  33049  hasheuni  33071  ballotlemi1  33489  ballotlemic  33493  sgnnbi  33532  sgnpbi  33533  sgnmulsgp  33537  signsply0  33550  signswch  33560  hgt750lem  33651  unblimceq0  35371  knoppndvlem1  35376  knoppndvlem2  35377  knoppndvlem7  35382  knoppndvlem13  35388  knoppndvlem14  35389  knoppndvlem15  35390  knoppndvlem17  35392  knoppndvlem20  35395  irrdiff  36195  poimirlem22  36498  poimirlem31  36507  asindmre  36559  areacirclem4  36567  60gcd7e1  40858  3lexlogpow5ineq2  40908  aks4d1p1p2  40923  aks4d1p7  40936  aks4d1p8d2  40938  aks4d1p8d3  40939  aks4d1p8  40940  aks4d1p9  40941  sticksstones11  40960  2xp3dxp2ge1d  41010  3cubeslem1  41407  pellexlem2  41553  pellexlem6  41557  pell14qrgt0  41582  elpell1qr2  41595  pellfundex  41609  pellfundrp  41611  rmxypos  41671  relexp01min  42449  imo72b2  42909  radcnvrat  43058  reclt0d  44083  sqrlearg  44252  sumnnodd  44332  liminf10ex  44476  liminfltlimsupex  44483  dvnmul  44645  stoweidlem7  44709  stoweidlem36  44738  stoweidlem38  44740  stoweidlem42  44744  stoweidlem51  44753  stoweidlem59  44761  stirlinglem5  44780  stirlinglem7  44782  stirlinglem10  44785  stirlinglem11  44786  stirlinglem12  44787  stirlinglem15  44790  dirkeritg  44804  fourierdlem11  44820  fourierdlem30  44839  fourierdlem47  44855  fourierdlem79  44887  fourierdlem103  44911  fourierdlem104  44912  fouriersw  44933  etransclem4  44940  etransclem31  44967  etransclem32  44968  etransclem35  44971  etransclem41  44977  salexct2  45041  hoidmvlelem1  45297  tworepnotupword  45586  m1mod0mod1  46023  nfermltl2rev  46397  m1modmmod  47160  regt1loggt0  47175  rege1logbrege0  47197  nnlog2ge0lt1  47205  eenglngeehlnmlem2  47377  amgmwlem  47802