Theorem 0lt1 9264

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 8805	. . 3 |- 1 e. RR
2		ax-1ne0 8774	. . 3 |- 1 =/= 0
3		msqgt0 9262	. . 3 |- ( ( 1 e. RR /\ 1 =/= 0 ) -> 0 < ( 1 x. 1 ) )
4	1, 2, 3	mp2an 656	. 2 |- 0 < ( 1 x. 1 )
5		ax-1cn 8763	. . 3 |- 1 e. CC
6	5	mulid1i 8807	. 2 |- ( 1 x. 1 ) = 1
7	4, 6	breqtri 4020	1 |- 0 < 1

Syntax hints:   e. wcel 1621   =/= wne 2421   class class class wbr 3997  (class class class)co 5792   RRcr 8704   0cc0 8705   1c1 8706   x. cmul 8710   < clt 8835

This theorem is referenced by:  0le1  9265  eqneg  9448  elimgt0  9560  ltp1  9562  ltm1  9564  recgt0  9568  mulgt1  9583  reclt1  9619  recgt1  9620  recgt1i  9621  recp1lt1  9622  recreclt  9623  recgt0ii  9630  inelr  9704  nnge1  9740  nngt0  9743  0nnn  9745  nnrecgt0  9751  2pos  9796  3pos  9798  4pos  9800  5pos  9801  6pos  9802  7pos  9803  8pos  9804  9pos  9805  10pos  9806  halflt1  9901  elnnnn0c  9977  elnnz1  10017  recnz  10055  1rp  10326  xmulid1  10566  fz10  10781  1mod  10963  expgt1  11107  ltexp2a  11120  expcan  11121  ltexp2  11122  leexp2  11123  leexp2a  11124  expnbnd  11197  expnlbnd  11198  expnlbnd2  11199  expmulnbnd  11200  discr1  11204  bcn1  11292  s2fv0  11501  resqrex  11702  mulcn2  12035  cvgrat  12302  cos1bnd  12430  sin01gt0  12433  sincos1sgn  12436  ruclem8  12478  nthruz  12493  sadcadd  12612  divdenle  12783  43prm  13086  ipostr  14219  abvtrivd  15568  gzrngunit  16400  znidomb  16478  thlle  16560  leordtval2  16905  mopnex  18028  dscopn  18059  metnrmlem1a  18325  xrhmph  18408  evth  18420  xlebnum  18426  vitalilem4  18929  vitalilem5  18930  vitali  18931  ply1remlem  19511  plyremlem  19647  plyrem  19648  vieta1lem2  19654  reeff1olem  19785  sinhalfpilem  19797  rplogcl  19921  logtayllem  19969  cxplt  20004  cxple  20005  atanre  20144  atanlogaddlem  20172  ressatans  20193  rlimcnp  20223  rlimcnp2  20224  cxp2limlem  20233  cxp2lim  20234  cxploglim2  20236  amgmlem  20247  emcllem2  20253  harmonicubnd  20266  fsumharmonic  20268  ftalem1  20273  ftalem2  20274  chpchtsum  20421  chpub  20422  mersenne  20429  perfectlem2  20432  efexple  20483  lgsdir2lem3  20527  chebbnd1  20584  dchrmusumlema  20605  dchrvmasumlem2  20610  dchrvmasumiflem1  20613  dchrisum0flblem2  20621  dchrisum0lema  20626  dchrisum0lem1  20628  dchrisum0lem2a  20629  mulog2sumlem1  20646  chpdifbndlem1  20665  chpdifbnd  20667  selberg3lem1  20669  pntrmax  20676  pntrsumo1  20677  pntpbnd1a  20697  pntpbnd2  20699  pntibndlem1  20701  pntlem3  20721  pnt  20726  ostth2lem1  20730  ostth2lem3  20747  ostth2lem4  20748  ballotlemi1  23023  ballotlemic  23027  ballotlem1c  23028  zetacvg  23062  fz0n  23469  axcontlem2  23969  bpoly4  24170  pellexlem2  26283  pellexlem6  26287  pell14qrgt0  26312  elpell1qr2  26325  pellfundex  26339  pellfundrp  26341  rmxypos  26402  stoweidlem7  27125  stoweidlem34  27152  stoweidlem36  27154  stoweidlem38  27156  stoweidlem42  27160  stoweidlem44  27162  stoweidlem51  27169  stoweidlem59  27177  stirlinglem5  27196  stirlinglem6  27197  stirlinglem7  27198  stirlinglem10  27201  stirlinglem11  27202  stirlinglem12  27203  stirlinglem15  27206  sgn1  27382

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484  ax-resscn 8762  ax-1cn 8763  ax-icn 8764  ax-addcl 8765  ax-addrcl 8766  ax-mulcl 8767  ax-mulrcl 8768  ax-mulcom 8769  ax-addass 8770  ax-mulass 8771  ax-distr 8772  ax-i2m1 8773  ax-1ne0 8774  ax-1rid 8775  ax-rnegex 8776  ax-rrecex 8777  ax-cnre 8778  ax-pre-lttri 8779  ax-pre-lttrn 8780  ax-pre-ltadd 8781  ax-pre-mulgt0 8782

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-nel 2424  df-ral 2523  df-rex 2524  df-reu 2525  df-rab 2527  df-v 2765  df-sbc 2967  df-csb 3057  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-mpt 4053  df-id 4281  df-po 4286  df-so 4287  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fn 4684  df-f 4685  df-f1 4686  df-fo 4687  df-f1o 4688  df-fv 4689  df-ov 5795  df-oprab 5796  df-mpt2 5797  df-iota 6225  df-riota 6272  df-er 6628  df-en 6832  df-dom 6833  df-sdom 6834  df-pnf 8837  df-mnf 8838  df-xr 8839  df-ltxr 8840  df-le 8841  df-sub 9007  df-neg 9008