Theorem 0lt1 11427

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 10906	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 10871	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11425	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 688	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 10860	. . 3 ⊢ 1 ∈ ℂ
6	5	mulid1i 10910	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5095	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2108   ≠ wne 2942   class class class wbr 5070  (class class class)co 7255  ℝcr 10801  0cc0 10802  1c1 10803   · cmul 10807   < clt 10940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138

This theorem is referenced by:  0le1  11428  eqneg  11625  elimgt0  11743  ltp1  11745  ltm1  11747  recgt0  11751  mulgt1  11764  reclt1  11800  recgt1  11801  recgt1i  11802  recp1lt1  11803  recreclt  11804  recgt0ii  11811  inelr  11893  nnge1  11931  nngt0  11934  0nnnALT  11940  nnrecgt0  11946  2pos  12006  3pos  12008  4pos  12010  5pos  12012  6pos  12013  7pos  12014  8pos  12015  9pos  12016  neg1lt0  12020  halflt1  12121  nn0p1gt0  12192  elnnnn0c  12208  elnnz1  12276  nn0lt10b  12312  recnz  12325  1rp  12663  divlt1lt  12728  divle1le  12729  ledivge1le  12730  nnledivrp  12771  xmulid1  12942  0nelfz1  13204  fz10  13206  fzpreddisj  13234  elfznelfzob  13421  1mod  13551  expgt1  13749  ltexp2a  13812  expcan  13815  ltexp2  13816  leexp2  13817  leexp2a  13818  expnbnd  13875  expnlbnd  13876  expnlbnd2  13877  expmulnbnd  13878  discr1  13882  bcn1  13955  hashnn0n0nn  14034  s2fv0  14528  swrd2lsw  14593  2swrd2eqwrdeq  14594  sgn1  14731  resqrex  14890  mulcn2  15233  cvgrat  15523  bpoly4  15697  cos1bnd  15824  sin01gt0  15827  sincos1sgn  15830  ruclem8  15874  p1modz1  15898  nnoddm1d2  16023  sadcadd  16093  dvdsnprmd  16323  isprm7  16341  divdenle  16381  43prm  16751  ipostr  18162  srgbinomlem4  19694  abvtrivd  20015  gzrngunit  20576  znidomb  20681  psgnodpmr  20707  thlle  20814  leordtval2  22271  mopnex  23581  dscopn  23635  metnrmlem1a  23927  xrhmph  24016  evth  24028  xlebnum  24034  vitalilem5  24681  vitali  24682  ply1remlem  25232  plyremlem  25369  plyrem  25370  vieta1lem2  25376  reeff1olem  25510  sinhalfpilem  25525  rplogcl  25664  logtayllem  25719  cxplt  25754  cxple  25755  atanlogaddlem  25968  ressatans  25989  rlimcnp  26020  rlimcnp2  26021  cxp2limlem  26030  cxp2lim  26031  cxploglim2  26033  amgmlem  26044  emcllem2  26051  harmonicubnd  26064  fsumharmonic  26066  zetacvg  26069  ftalem1  26127  ftalem2  26128  chpchtsum  26272  chpub  26273  mersenne  26280  perfectlem2  26283  efexple  26334  chebbnd1  26525  dchrmusumlema  26546  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrisum0flblem2  26562  dchrisum0lema  26567  dchrisum0lem1  26569  dchrisum0lem2a  26570  mulog2sumlem1  26587  chpdifbndlem1  26606  chpdifbnd  26608  selberg3lem1  26610  pntrmax  26617  pntrsumo1  26618  pntpbnd1a  26638  pntpbnd2  26640  pntibndlem1  26642  pntlem3  26662  pnt  26667  ostth2lem1  26671  ostth2lem3  26688  ostth2lem4  26689  axcontlem2  27236  wwlksn0s  28127  clwwlkf1  28314  esumcst  31931  hasheuni  31953  ballotlemi1  32369  ballotlemic  32373  sgnnbi  32412  sgnpbi  32413  sgnmulsgp  32417  signsply0  32430  signswch  32440  hgt750lem  32531  unblimceq0  34614  knoppndvlem1  34619  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem13  34631  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem17  34635  knoppndvlem20  34638  irrdiff  35424  poimirlem22  35726  poimirlem31  35735  asindmre  35787  areacirclem4  35795  60gcd7e1  39941  3lexlogpow5ineq2  39991  aks4d1p1p2  40006  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8d3  40022  aks4d1p8  40023  aks4d1p9  40024  sticksstones11  40040  2xp3dxp2ge1d  40090  3cubeslem1  40422  pellexlem2  40568  pellexlem6  40572  pell14qrgt0  40597  elpell1qr2  40610  pellfundex  40624  pellfundrp  40626  rmxypos  40685  relexp01min  41210  imo72b2  41672  radcnvrat  41821  reclt0d  42816  sqrlearg  42981  sumnnodd  43061  liminf10ex  43205  liminfltlimsupex  43212  dvnmul  43374  stoweidlem7  43438  stoweidlem36  43467  stoweidlem38  43469  stoweidlem42  43473  stoweidlem51  43482  stoweidlem59  43490  stirlinglem5  43509  stirlinglem7  43511  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  stirlinglem15  43519  dirkeritg  43533  fourierdlem11  43549  fourierdlem30  43568  fourierdlem47  43584  fourierdlem79  43616  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  etransclem4  43669  etransclem31  43696  etransclem32  43697  etransclem35  43700  etransclem41  43706  salexct2  43768  hoidmvlelem1  44023  m1mod0mod1  44709  nfermltl2rev  45083  m1modmmod  45755  regt1loggt0  45770  rege1logbrege0  45792  nnlog2ge0lt1  45800  eenglngeehlnmlem2  45972  amgmwlem  46392