Theorem 0lt1 9292

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 8833	. . 3 |- 1 e. RR
2		ax-1ne0 8802	. . 3 |- 1 =/= 0
3		msqgt0 9290	. . 3 |- ( ( 1 e. RR /\ 1 =/= 0 ) -> 0 < ( 1 x. 1 ) )
4	1, 2, 3	mp2an 653	. 2 |- 0 < ( 1 x. 1 )
5		ax-1cn 8791	. . 3 |- 1 e. CC
6	5	mulid1i 8835	. 2 |- ( 1 x. 1 ) = 1
7	4, 6	breqtri 4047	1 |- 0 < 1

Syntax hints:   e. wcel 1685   =/= wne 2447   class class class wbr 4024  (class class class)co 5820   RRcr 8732   0cc0 8733   1c1 8734   x. cmul 8738   < clt 8863

This theorem is referenced by:  0le1  9293  eqneg  9476  elimgt0  9588  ltp1  9590  ltm1  9592  recgt0  9596  mulgt1  9611  reclt1  9647  recgt1  9648  recgt1i  9649  recp1lt1  9650  recreclt  9651  recgt0ii  9658  inelr  9732  nnge1  9768  nngt0  9771  0nnn  9773  nnrecgt0  9779  2pos  9824  3pos  9826  4pos  9828  5pos  9829  6pos  9830  7pos  9831  8pos  9832  9pos  9833  10pos  9834  halflt1  9929  elnnnn0c  10005  elnnz1  10045  recnz  10083  1rp  10354  xmulid1  10595  fz10  10810  1mod  10992  expgt1  11136  ltexp2a  11149  expcan  11150  ltexp2  11151  leexp2  11152  leexp2a  11153  expnbnd  11226  expnlbnd  11227  expnlbnd2  11228  expmulnbnd  11229  discr1  11233  bcn1  11321  s2fv0  11531  resqrex  11732  mulcn2  12065  cvgrat  12335  cos1bnd  12463  sin01gt0  12466  sincos1sgn  12469  ruclem8  12511  nthruz  12526  sadcadd  12645  divdenle  12816  43prm  13119  ipostr  14252  abvtrivd  15601  gzrngunit  16433  znidomb  16511  thlle  16593  leordtval2  16938  mopnex  18061  dscopn  18092  metnrmlem1a  18358  xrhmph  18441  evth  18453  xlebnum  18459  vitalilem4  18962  vitalilem5  18963  vitali  18964  ply1remlem  19544  plyremlem  19680  plyrem  19681  vieta1lem2  19687  reeff1olem  19818  sinhalfpilem  19830  rplogcl  19954  logtayllem  20002  cxplt  20037  cxple  20038  atanre  20177  atanlogaddlem  20205  ressatans  20226  rlimcnp  20256  rlimcnp2  20257  cxp2limlem  20266  cxp2lim  20267  cxploglim2  20269  amgmlem  20280  emcllem2  20286  harmonicubnd  20299  fsumharmonic  20301  ftalem1  20306  ftalem2  20307  chpchtsum  20454  chpub  20455  mersenne  20462  perfectlem2  20465  efexple  20516  lgsdir2lem3  20560  chebbnd1  20617  dchrmusumlema  20638  dchrvmasumlem2  20643  dchrvmasumiflem1  20646  dchrisum0flblem2  20654  dchrisum0lema  20659  dchrisum0lem1  20661  dchrisum0lem2a  20662  mulog2sumlem1  20679  chpdifbndlem1  20698  chpdifbnd  20700  selberg3lem1  20702  pntrmax  20709  pntrsumo1  20710  pntpbnd1a  20730  pntpbnd2  20732  pntibndlem1  20734  pntlem3  20754  pnt  20759  ostth2lem1  20763  ostth2lem3  20780  ostth2lem4  20781  ballotlemi1  23057  ballotlemic  23061  ballotlem1c  23062  zetacvg  23096  fz0n  23503  axcontlem2  24003  bpoly4  24204  areacirclem5  24339  pellexlem2  26326  pellexlem6  26330  pell14qrgt0  26355  elpell1qr2  26368  pellfundex  26382  pellfundrp  26384  rmxypos  26445  stoweidlem7  27167  stoweidlem34  27194  stoweidlem36  27196  stoweidlem38  27198  stoweidlem42  27202  stoweidlem44  27204  stoweidlem51  27211  stoweidlem59  27219  stirlinglem5  27238  stirlinglem6  27239  stirlinglem7  27240  stirlinglem10  27243  stirlinglem11  27244  stirlinglem12  27245  stirlinglem15  27248  sgn1  27521

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pow 4187  ax-pr 4213  ax-un 4511  ax-resscn 8790  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-mulcom 8797  ax-addass 8798  ax-mulass 8799  ax-distr 8800  ax-i2m1 8801  ax-1ne0 8802  ax-1rid 8803  ax-rnegex 8804  ax-rrecex 8805  ax-cnre 8806  ax-pre-lttri 8807  ax-pre-lttrn 8808  ax-pre-ltadd 8809  ax-pre-mulgt0 8810

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-nel 2450  df-ral 2549  df-rex 2550  df-reu 2551  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-pw 3628  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-po 4313  df-so 4314  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229  df-ov 5823  df-oprab 5824  df-mpt2 5825  df-iota 6253  df-riota 6300  df-er 6656  df-en 6860  df-dom 6861  df-sdom 6862  df-pnf 8865  df-mnf 8866  df-xr 8867  df-ltxr 8868  df-le 8869  df-sub 9035  df-neg 9036