Theorem 0lt1 11663

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 11135	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11098	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11661	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 693	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11087	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11140	. 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 7360  ℝcr 11028  0cc0 11029  1c1 11030   · cmul 11034   < clt 11170

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 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

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 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371

This theorem is referenced by:  0le1  11664  eqneg  11866  elimgt0  11984  ltp1  11986  ltm1  11988  recgt0  11992  mulgt1OLD  12005  mulgt1  12008  reclt1  12042  recgt1  12043  recgt1i  12044  recp1lt1  12045  recreclt  12046  recgt0ii  12053  neg1lt0  12138  nnge1  12196  nngt0  12199  0nnnALT  12205  nnrecgt0  12211  2pos  12275  3pos  12277  4pos  12279  5pos  12281  6pos  12282  7pos  12283  8pos  12284  9pos  12285  halflt1  12385  nn0p1gt0  12457  elnnnn0c  12473  elnnz1  12544  nn0lt10b  12582  recnz  12595  1rp  12937  divlt1lt  13004  divle1le  13005  ledivge1le  13006  nnledivrp  13047  xmulrid  13222  0nelfz1  13488  fz10  13490  fzpreddisj  13518  elfznelfzob  13720  1mod  13853  expgt1  14053  ltexp2a  14119  expcan  14122  ltexp2  14123  leexp2  14124  leexp2a  14125  expnbnd  14185  expnlbnd  14186  expnlbnd2  14187  expmulnbnd  14188  discr1  14192  bcn1  14266  hashnn0n0nn  14344  s2fv0  14840  swrd2lsw  14905  2swrd2eqwrdeq  14906  sgn1  15045  resqrex  15203  mulcn2  15549  cvgrat  15839  bpoly4  16015  cos1bnd  16145  sin01gt0  16148  sincos1sgn  16151  ruclem8  16195  p1modz1  16219  nnoddm1d2  16346  sadcadd  16418  dvdsnprmd  16650  isprm7  16669  divdenle  16710  43prm  17083  plendxnocndx  17338  ipostr  18486  srgbinomlem4  20201  abvtrivd  20800  gzrngunit  21423  znidomb  21551  psgnodpmr  21580  leordtval2  23187  mopnex  24494  dscopn  24548  metnrmlem1a  24834  xrhmph  24924  evth  24936  xlebnum  24942  vitalilem5  25589  vitali  25590  ply1remlem  26140  plyremlem  26281  plyrem  26282  vieta1lem2  26288  reeff1olem  26424  sinhalfpilem  26440  rplogcl  26581  logtayllem  26636  cxplt  26671  cxple  26672  atanlogaddlem  26890  ressatans  26911  rlimcnp  26942  rlimcnp2  26943  cxp2limlem  26953  cxp2lim  26954  cxploglim2  26956  amgmlem  26967  emcllem2  26974  harmonicubnd  26987  fsumharmonic  26989  zetacvg  26992  ftalem1  27050  ftalem2  27051  chpchtsum  27196  chpub  27197  mersenne  27204  perfectlem2  27207  efexple  27258  chebbnd1  27449  dchrmusumlema  27470  dchrvmasumlem2  27475  dchrvmasumiflem1  27478  dchrisum0flblem2  27486  dchrisum0lema  27491  dchrisum0lem1  27493  dchrisum0lem2a  27494  mulog2sumlem1  27511  chpdifbndlem1  27530  chpdifbnd  27532  selberg3lem1  27534  pntrmax  27541  pntrsumo1  27542  pntpbnd1a  27562  pntpbnd2  27564  pntibndlem1  27566  pntlem3  27586  pnt  27591  ostth2lem1  27595  ostth2lem3  27612  ostth2lem4  27613  axcontlem2  29048  wwlksn0s  29944  clwwlkf1  30134  sgnnbi  32926  sgnpbi  32927  sgnmulsgp  32931  vietadeg1  33737  cos9thpiminplylem1  33942  cos9thpiminply  33948  esumcst  34223  hasheuni  34245  ballotlemi1  34663  ballotlemic  34667  signsply0  34711  signswch  34721  hgt750lem  34811  unblimceq0  36783  knoppndvlem1  36788  knoppndvlem2  36789  knoppndvlem7  36794  knoppndvlem13  36800  knoppndvlem14  36801  knoppndvlem15  36802  knoppndvlem17  36804  knoppndvlem20  36807  irrdiff  37656  poimirlem22  37977  poimirlem31  37986  asindmre  38038  areacirclem4  38046  60gcd7e1  42458  3lexlogpow5ineq2  42508  aks4d1p1p2  42523  aks4d1p7  42536  aks4d1p8d2  42538  aks4d1p8d3  42539  aks4d1p8  42540  aks4d1p9  42541  aks6d1c5lem3  42590  sticksstones11  42609  aks6d1c6lem1  42623  aks6d1c6lem4  42626  aks6d1c7lem2  42634  explt1d  42769  3cubeslem1  43130  pellexlem2  43276  pellexlem6  43280  pell14qrgt0  43305  elpell1qr2  43318  pellfundex  43332  pellfundrp  43334  rmxypos  43393  relexp01min  44158  imo72b2  44617  radcnvrat  44759  reclt0d  45834  sqrlearg  46001  sumnnodd  46078  liminf10ex  46220  liminfltlimsupex  46227  dvnmul  46389  stoweidlem7  46453  stoweidlem36  46482  stoweidlem38  46484  stoweidlem42  46488  stoweidlem51  46497  stoweidlem59  46505  stirlinglem5  46524  stirlinglem7  46526  stirlinglem10  46529  stirlinglem11  46530  stirlinglem12  46531  stirlinglem15  46534  dirkeritg  46548  fourierdlem11  46564  fourierdlem30  46583  fourierdlem47  46599  fourierdlem79  46631  fourierdlem103  46655  fourierdlem104  46656  fouriersw  46677  etransclem4  46684  etransclem31  46711  etransclem32  46712  etransclem35  46715  etransclem41  46721  salexct2  46785  hoidmvlelem1  47041  cjnpoly  47349  m1mod0mod1  47820  m1modmmod  47824  muldvdsfacgt  47846  muldvdsfacm1  47847  nfermltl2rev  48231  regt1loggt0  49024  rege1logbrege0  49046  nnlog2ge0lt1  49054  eenglngeehlnmlem2  49226  amgmwlem  50289