Theorem 0lt1 11243

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 10722	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 10687	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11241	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 692	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 10676	. . 3 ⊢ 1 ∈ ℂ
6	5	mulid1i 10726	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5056	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2114   ≠ wne 2935   class class class wbr 5031  (class class class)co 7173  ℝcr 10617  0cc0 10618  1c1 10619   · cmul 10623   < clt 10756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7482  ax-resscn 10675  ax-1cn 10676  ax-icn 10677  ax-addcl 10678  ax-addrcl 10679  ax-mulcl 10680  ax-mulrcl 10681  ax-mulcom 10682  ax-addass 10683  ax-mulass 10684  ax-distr 10685  ax-i2m1 10686  ax-1ne0 10687  ax-1rid 10688  ax-rnegex 10689  ax-rrecex 10690  ax-cnre 10691  ax-pre-lttri 10692  ax-pre-lttrn 10693  ax-pre-ltadd 10694  ax-pre-mulgt0 10695

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3401  df-sbc 3682  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5430  df-po 5443  df-so 5444  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7130  df-ov 7176  df-oprab 7177  df-mpo 7178  df-er 8323  df-en 8559  df-dom 8560  df-sdom 8561  df-pnf 10758  df-mnf 10759  df-xr 10760  df-ltxr 10761  df-le 10762  df-sub 10953  df-neg 10954

This theorem is referenced by:  0le1  11244  eqneg  11441  elimgt0  11559  ltp1  11561  ltm1  11563  recgt0  11567  mulgt1  11580  reclt1  11616  recgt1  11617  recgt1i  11618  recp1lt1  11619  recreclt  11620  recgt0ii  11627  inelr  11709  nnge1  11747  nngt0  11750  0nnnALT  11756  nnrecgt0  11762  2pos  11822  3pos  11824  4pos  11826  5pos  11828  6pos  11829  7pos  11830  8pos  11831  9pos  11832  neg1lt0  11836  halflt1  11937  nn0p1gt0  12008  elnnnn0c  12024  elnnz1  12092  nn0lt10b  12128  recnz  12141  1rp  12479  divlt1lt  12544  divle1le  12545  ledivge1le  12546  nnledivrp  12587  xmulid1  12758  0nelfz1  13020  fz10  13022  fzpreddisj  13050  elfznelfzob  13237  1mod  13365  expgt1  13562  ltexp2a  13625  expcan  13628  ltexp2  13629  leexp2  13630  leexp2a  13631  expnbnd  13688  expnlbnd  13689  expnlbnd2  13690  expmulnbnd  13691  discr1  13695  bcn1  13768  hashnn0n0nn  13847  s2fv0  14341  swrd2lsw  14406  2swrd2eqwrdeq  14407  sgn1  14544  resqrex  14703  mulcn2  15046  cvgrat  15334  bpoly4  15508  cos1bnd  15635  sin01gt0  15638  sincos1sgn  15641  ruclem8  15685  p1modz1  15709  nnoddm1d2  15834  sadcadd  15904  dvdsnprmd  16134  isprm7  16152  divdenle  16192  43prm  16561  ipostr  17882  srgbinomlem4  19415  abvtrivd  19733  gzrngunit  20286  znidomb  20383  psgnodpmr  20409  thlle  20516  leordtval2  21966  mopnex  23275  dscopn  23329  metnrmlem1a  23613  xrhmph  23702  evth  23714  xlebnum  23720  vitalilem5  24367  vitali  24368  ply1remlem  24918  plyremlem  25055  plyrem  25056  vieta1lem2  25062  reeff1olem  25196  sinhalfpilem  25211  rplogcl  25350  logtayllem  25405  cxplt  25440  cxple  25441  atanlogaddlem  25654  ressatans  25675  rlimcnp  25706  rlimcnp2  25707  cxp2limlem  25716  cxp2lim  25717  cxploglim2  25719  amgmlem  25730  emcllem2  25737  harmonicubnd  25750  fsumharmonic  25752  zetacvg  25755  ftalem1  25813  ftalem2  25814  chpchtsum  25958  chpub  25959  mersenne  25966  perfectlem2  25969  efexple  26020  chebbnd1  26211  dchrmusumlema  26232  dchrvmasumlem2  26237  dchrvmasumiflem1  26240  dchrisum0flblem2  26248  dchrisum0lema  26253  dchrisum0lem1  26255  dchrisum0lem2a  26256  mulog2sumlem1  26273  chpdifbndlem1  26292  chpdifbnd  26294  selberg3lem1  26296  pntrmax  26303  pntrsumo1  26304  pntpbnd1a  26324  pntpbnd2  26326  pntibndlem1  26328  pntlem3  26348  pnt  26353  ostth2lem1  26357  ostth2lem3  26374  ostth2lem4  26375  axcontlem2  26914  wwlksn0s  27802  clwwlkf1  27989  esumcst  31604  hasheuni  31626  ballotlemi1  32042  ballotlemic  32046  sgnnbi  32085  sgnpbi  32086  sgnmulsgp  32090  signsply0  32103  signswch  32113  hgt750lem  32204  unblimceq0  34333  knoppndvlem1  34338  knoppndvlem2  34339  knoppndvlem7  34344  knoppndvlem13  34350  knoppndvlem14  34351  knoppndvlem15  34352  knoppndvlem17  34354  knoppndvlem20  34357  irrdiff  35140  poimirlem22  35445  poimirlem31  35454  asindmre  35506  areacirclem4  35514  60gcd7e1  39656  3lexlogpow5ineq2  39706  aks4d1p1p2  39720  2xp3dxp2ge1d  39776  3cubeslem1  40101  pellexlem2  40247  pellexlem6  40251  pell14qrgt0  40276  elpell1qr2  40289  pellfundex  40303  pellfundrp  40305  rmxypos  40364  relexp01min  40890  imo72b2  41353  radcnvrat  41493  reclt0d  42487  sqrlearg  42654  sumnnodd  42736  liminf10ex  42880  liminfltlimsupex  42887  dvnmul  43049  stoweidlem7  43113  stoweidlem36  43142  stoweidlem38  43144  stoweidlem42  43148  stoweidlem51  43157  stoweidlem59  43165  stirlinglem5  43184  stirlinglem7  43186  stirlinglem10  43189  stirlinglem11  43190  stirlinglem12  43191  stirlinglem15  43194  dirkeritg  43208  fourierdlem11  43224  fourierdlem30  43243  fourierdlem47  43259  fourierdlem79  43291  fourierdlem103  43315  fourierdlem104  43316  fouriersw  43337  etransclem4  43344  etransclem31  43371  etransclem32  43372  etransclem35  43375  etransclem41  43381  salexct2  43443  hoidmvlelem1  43698  m1mod0mod1  44385  nfermltl2rev  44759  m1modmmod  45431  regt1loggt0  45446  rege1logbrege0  45468  nnlog2ge0lt1  45476  eenglngeehlnmlem2  45648  amgmwlem  45989