Theorem 0lt1 11650

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 11123	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11086	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11648	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 692	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11075	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11127	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5120	1 ⊢ 0 < 1

Syntax hints:   ∈ wcel 2113   ≠ wne 2929   class class class wbr 5095  (class class class)co 7355  ℝcr 11016  0cc0 11017  1c1 11018   · cmul 11022   < clt 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093  ax-pre-mulgt0 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-sub 11357  df-neg 11358

This theorem is referenced by:  0le1  11651  eqneg  11852  elimgt0  11970  ltp1  11972  ltm1  11974  recgt0  11978  mulgt1OLD  11991  mulgt1  11994  reclt1  12028  recgt1  12029  recgt1i  12030  recp1lt1  12031  recreclt  12032  recgt0ii  12039  neg1lt0  12124  nnge1  12164  nngt0  12167  0nnnALT  12173  nnrecgt0  12179  2pos  12239  3pos  12241  4pos  12243  5pos  12245  6pos  12246  7pos  12247  8pos  12248  9pos  12249  halflt1  12349  nn0p1gt0  12421  elnnnn0c  12437  elnnz1  12508  nn0lt10b  12545  recnz  12558  1rp  12900  divlt1lt  12967  divle1le  12968  ledivge1le  12969  nnledivrp  13010  xmulrid  13185  0nelfz1  13450  fz10  13452  fzpreddisj  13480  elfznelfzob  13681  1mod  13814  expgt1  14014  ltexp2a  14080  expcan  14083  ltexp2  14084  leexp2  14085  leexp2a  14086  expnbnd  14146  expnlbnd  14147  expnlbnd2  14148  expmulnbnd  14149  discr1  14153  bcn1  14227  hashnn0n0nn  14305  s2fv0  14801  swrd2lsw  14866  2swrd2eqwrdeq  14867  sgn1  15006  resqrex  15164  mulcn2  15510  cvgrat  15797  bpoly4  15973  cos1bnd  16103  sin01gt0  16106  sincos1sgn  16109  ruclem8  16153  p1modz1  16177  nnoddm1d2  16304  sadcadd  16376  dvdsnprmd  16608  isprm7  16626  divdenle  16667  43prm  17040  plendxnocndx  17295  ipostr  18443  srgbinomlem4  20155  abvtrivd  20756  gzrngunit  21379  znidomb  21507  psgnodpmr  21536  leordtval2  23147  mopnex  24454  dscopn  24508  metnrmlem1a  24794  xrhmph  24892  evth  24905  xlebnum  24911  vitalilem5  25560  vitali  25561  ply1remlem  26117  plyremlem  26259  plyrem  26260  vieta1lem2  26266  reeff1olem  26403  sinhalfpilem  26419  rplogcl  26560  logtayllem  26615  cxplt  26650  cxple  26651  atanlogaddlem  26870  ressatans  26891  rlimcnp  26922  rlimcnp2  26923  cxp2limlem  26933  cxp2lim  26934  cxploglim2  26936  amgmlem  26947  emcllem2  26954  harmonicubnd  26967  fsumharmonic  26969  zetacvg  26972  ftalem1  27030  ftalem2  27031  chpchtsum  27177  chpub  27178  mersenne  27185  perfectlem2  27188  efexple  27239  chebbnd1  27430  dchrmusumlema  27451  dchrvmasumlem2  27456  dchrvmasumiflem1  27459  dchrisum0flblem2  27467  dchrisum0lema  27472  dchrisum0lem1  27474  dchrisum0lem2a  27475  mulog2sumlem1  27492  chpdifbndlem1  27511  chpdifbnd  27513  selberg3lem1  27515  pntrmax  27522  pntrsumo1  27523  pntpbnd1a  27543  pntpbnd2  27545  pntibndlem1  27547  pntlem3  27567  pnt  27572  ostth2lem1  27576  ostth2lem3  27593  ostth2lem4  27594  axcontlem2  28964  wwlksn0s  29860  clwwlkf1  30050  sgnnbi  32847  sgnpbi  32848  sgnmulsgp  32852  vietadeg1  33662  cos9thpiminplylem1  33867  cos9thpiminply  33873  esumcst  34148  hasheuni  34170  ballotlemi1  34588  ballotlemic  34592  signsply0  34636  signswch  34646  hgt750lem  34736  unblimceq0  36623  knoppndvlem1  36628  knoppndvlem2  36629  knoppndvlem7  36634  knoppndvlem13  36640  knoppndvlem14  36641  knoppndvlem15  36642  knoppndvlem17  36644  knoppndvlem20  36647  irrdiff  37443  poimirlem22  37755  poimirlem31  37764  asindmre  37816  areacirclem4  37824  60gcd7e1  42171  3lexlogpow5ineq2  42221  aks4d1p1p2  42236  aks4d1p7  42249  aks4d1p8d2  42251  aks4d1p8d3  42252  aks4d1p8  42253  aks4d1p9  42254  aks6d1c5lem3  42303  sticksstones11  42322  aks6d1c6lem1  42336  aks6d1c6lem4  42339  aks6d1c7lem2  42347  explt1d  42493  3cubeslem1  42841  pellexlem2  42987  pellexlem6  42991  pell14qrgt0  43016  elpell1qr2  43029  pellfundex  43043  pellfundrp  43045  rmxypos  43104  relexp01min  43870  imo72b2  44329  radcnvrat  44471  reclt0d  45547  sqrlearg  45715  sumnnodd  45792  liminf10ex  45934  liminfltlimsupex  45941  dvnmul  46103  stoweidlem7  46167  stoweidlem36  46196  stoweidlem38  46198  stoweidlem42  46202  stoweidlem51  46211  stoweidlem59  46219  stirlinglem5  46238  stirlinglem7  46240  stirlinglem10  46243  stirlinglem11  46244  stirlinglem12  46245  stirlinglem15  46248  dirkeritg  46262  fourierdlem11  46278  fourierdlem30  46297  fourierdlem47  46313  fourierdlem79  46345  fourierdlem103  46369  fourierdlem104  46370  fouriersw  46391  etransclem4  46398  etransclem31  46425  etransclem32  46426  etransclem35  46429  etransclem41  46435  salexct2  46499  hoidmvlelem1  46755  cjnpoly  47051  m1mod0mod1  47516  m1modmmod  47520  nfermltl2rev  47905  regt1loggt0  48698  rege1logbrege0  48720  nnlog2ge0lt1  48728  eenglngeehlnmlem2  48900  amgmwlem  49963