Theorem 0lt1 11661

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 11133	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11096	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11659	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 693	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11085	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11138	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5111	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2114   ≠ wne 2933   class class class wbr 5086  (class class class)co 7358  ℝcr 11026  0cc0 11027  1c1 11028   · cmul 11032   < clt 11168

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680  ax-resscn 11084  ax-1cn 11085  ax-icn 11086  ax-addcl 11087  ax-addrcl 11088  ax-mulcl 11089  ax-mulrcl 11090  ax-mulcom 11091  ax-addass 11092  ax-mulass 11093  ax-distr 11094  ax-i2m1 11095  ax-1ne0 11096  ax-1rid 11097  ax-rnegex 11098  ax-rrecex 11099  ax-cnre 11100  ax-pre-lttri 11101  ax-pre-lttrn 11102  ax-pre-ltadd 11103  ax-pre-mulgt0 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369

This theorem is referenced by:  0le1  11662  eqneg  11864  elimgt0  11982  ltp1  11984  ltm1  11986  recgt0  11990  mulgt1OLD  12003  mulgt1  12006  reclt1  12040  recgt1  12041  recgt1i  12042  recp1lt1  12043  recreclt  12044  recgt0ii  12051  neg1lt0  12136  nnge1  12194  nngt0  12197  0nnnALT  12203  nnrecgt0  12209  2pos  12273  3pos  12275  4pos  12277  5pos  12279  6pos  12280  7pos  12281  8pos  12282  9pos  12283  halflt1  12383  nn0p1gt0  12455  elnnnn0c  12471  elnnz1  12542  nn0lt10b  12580  recnz  12593  1rp  12935  divlt1lt  13002  divle1le  13003  ledivge1le  13004  nnledivrp  13045  xmulrid  13220  0nelfz1  13486  fz10  13488  fzpreddisj  13516  elfznelfzob  13718  1mod  13851  expgt1  14051  ltexp2a  14117  expcan  14120  ltexp2  14121  leexp2  14122  leexp2a  14123  expnbnd  14183  expnlbnd  14184  expnlbnd2  14185  expmulnbnd  14186  discr1  14190  bcn1  14264  hashnn0n0nn  14342  s2fv0  14838  swrd2lsw  14903  2swrd2eqwrdeq  14904  sgn1  15043  resqrex  15201  mulcn2  15547  cvgrat  15837  bpoly4  16013  cos1bnd  16143  sin01gt0  16146  sincos1sgn  16149  ruclem8  16193  p1modz1  16217  nnoddm1d2  16344  sadcadd  16416  dvdsnprmd  16648  isprm7  16667  divdenle  16708  43prm  17081  plendxnocndx  17336  ipostr  18484  srgbinomlem4  20199  abvtrivd  20798  gzrngunit  21421  znidomb  21549  psgnodpmr  21578  leordtval2  23185  mopnex  24492  dscopn  24546  metnrmlem1a  24832  xrhmph  24922  evth  24934  xlebnum  24940  vitalilem5  25587  vitali  25588  ply1remlem  26138  plyremlem  26279  plyrem  26280  vieta1lem2  26286  reeff1olem  26422  sinhalfpilem  26438  rplogcl  26579  logtayllem  26634  cxplt  26669  cxple  26670  atanlogaddlem  26888  ressatans  26909  rlimcnp  26940  rlimcnp2  26941  cxp2limlem  26951  cxp2lim  26952  cxploglim2  26954  amgmlem  26965  emcllem2  26972  harmonicubnd  26985  fsumharmonic  26987  zetacvg  26990  ftalem1  27048  ftalem2  27049  chpchtsum  27194  chpub  27195  mersenne  27202  perfectlem2  27205  efexple  27256  chebbnd1  27447  dchrmusumlema  27468  dchrvmasumlem2  27473  dchrvmasumiflem1  27476  dchrisum0flblem2  27484  dchrisum0lema  27489  dchrisum0lem1  27491  dchrisum0lem2a  27492  mulog2sumlem1  27509  chpdifbndlem1  27528  chpdifbnd  27530  selberg3lem1  27532  pntrmax  27539  pntrsumo1  27540  pntpbnd1a  27560  pntpbnd2  27562  pntibndlem1  27564  pntlem3  27584  pnt  27589  ostth2lem1  27593  ostth2lem3  27610  ostth2lem4  27611  axcontlem2  29046  wwlksn0s  29942  clwwlkf1  30132  sgnnbi  32924  sgnpbi  32925  sgnmulsgp  32929  vietadeg1  33735  cos9thpiminplylem1  33940  cos9thpiminply  33946  esumcst  34221  hasheuni  34243  ballotlemi1  34661  ballotlemic  34665  signsply0  34709  signswch  34719  hgt750lem  34809  unblimceq0  36773  knoppndvlem1  36778  knoppndvlem2  36779  knoppndvlem7  36784  knoppndvlem13  36790  knoppndvlem14  36791  knoppndvlem15  36792  knoppndvlem17  36794  knoppndvlem20  36797  irrdiff  37646  poimirlem22  37967  poimirlem31  37976  asindmre  38028  areacirclem4  38036  60gcd7e1  42448  3lexlogpow5ineq2  42498  aks4d1p1p2  42513  aks4d1p7  42526  aks4d1p8d2  42528  aks4d1p8d3  42529  aks4d1p8  42530  aks4d1p9  42531  aks6d1c5lem3  42580  sticksstones11  42599  aks6d1c6lem1  42613  aks6d1c6lem4  42616  aks6d1c7lem2  42624  explt1d  42759  3cubeslem1  43120  pellexlem2  43266  pellexlem6  43270  pell14qrgt0  43295  elpell1qr2  43308  pellfundex  43322  pellfundrp  43324  rmxypos  43383  relexp01min  44148  imo72b2  44607  radcnvrat  44749  reclt0d  45824  sqrlearg  45991  sumnnodd  46068  liminf10ex  46210  liminfltlimsupex  46217  dvnmul  46379  stoweidlem7  46443  stoweidlem36  46472  stoweidlem38  46474  stoweidlem42  46478  stoweidlem51  46487  stoweidlem59  46495  stirlinglem5  46514  stirlinglem7  46516  stirlinglem10  46519  stirlinglem11  46520  stirlinglem12  46521  stirlinglem15  46524  dirkeritg  46538  fourierdlem11  46554  fourierdlem30  46573  fourierdlem47  46589  fourierdlem79  46621  fourierdlem103  46645  fourierdlem104  46646  fouriersw  46667  etransclem4  46674  etransclem31  46701  etransclem32  46702  etransclem35  46705  etransclem41  46711  salexct2  46775  hoidmvlelem1  47031  cjnpoly  47339  m1mod0mod1  47810  m1modmmod  47814  muldvdsfacgt  47836  muldvdsfacm1  47837  nfermltl2rev  48221  regt1loggt0  49014  rege1logbrege0  49036  nnlog2ge0lt1  49044  eenglngeehlnmlem2  49216  amgmwlem  50279