Theorem 0lt1 11843

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 11313	. . 3 ⊢ 1 ∈ ℝ
2		ax-1ne0 11274	. . 3 ⊢ 1 ≠ 0
3		msqgt0 11841	. . 3 ⊢ ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
4	1, 2, 3	mp2an 705	. 2 ⊢ 0 < (1 · 1)
5		ax-1cn 11263	. . 3 ⊢ 1 ∈ ℂ
6	5	mulridi 11318	. 2 ⊢ (1 · 1) = 1
7	4, 6	breqtri 5129	1 ⊢ 0 < 1

This proof depends on syntax axioms:   ∈ wcel 2144   ≠ wne 2955   class class class wbr 5102  (class class class)co 7422  ℝcr 11204  0cc0 11205  1c1 11206   · cmul 11210   < clt 11348

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7753  ax-resscn 11262  ax-1cn 11263  ax-icn 11264  ax-addcl 11265  ax-addrcl 11266  ax-mulcl 11267  ax-mulrcl 11268  ax-mulcom 11269  ax-addass 11270  ax-mulass 11271  ax-distr 11272  ax-i2m1 11273  ax-1ne0 11274  ax-1rid 11275  ax-rnegex 11276  ax-rrecex 11277  ax-cnre 11278  ax-pre-lttri 11279  ax-pre-lttrn 11280  ax-pre-ltadd 11281  ax-pre-mulgt0 11282

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6496  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7379  df-ov 7425  df-oprab 7426  df-mpo 7427  df-er 8722  df-en 8979  df-dom 8980  df-sdom 8981  df-pnf 11350  df-mnf 11351  df-xr 11352  df-ltxr 11353  df-le 11354  df-sub 11548  df-neg 11549

This theorem is used by:  0le1  11844  eqneg  12042  elimgt0  12160  ltp1  12162  ltm1  12164  recgt0  12168  mulgt1  12183  reclt1  12217  recgt1  12218  recgt1i  12219  recp1lt1  12220  recreclt  12221  recgt0ii  12228  neg1lt0  12313  nnge1  12371  nngt0  12374  0nnnALT  12380  nnrecgt0  12386  2posOLD  12453  halflt1  12568  nn0p1gt0  12640  elnnnn0c  12656  elnnz1  12727  nn0lt10b  12766  recnz  12779  1rp  13129  divlt1lt  13196  divle1le  13197  ledivge1le  13198  nnledivrp  13239  xmulrid  13414  0nelfz1  13681  fz10  13683  fzpreddisj  13712  elfznelfzob  13914  1mod  14048  expgt1  14248  ltexp2a  14314  expcan  14317  ltexp2  14318  leexp2  14319  leexp2a  14320  expnbnd  14381  expnlbnd  14382  expnlbnd2  14383  expmulnbnd  14384  discr1  14388  bcn1  14462  hashnn0n0nn  14540  s2fv0  15044  swrd2lsw  15112  2swrd2eqwrdeq  15113  sgn1  15252  sgnnbi  15264  sgnpbi  15265  resqrex  15424  mulcn2  15770  cvgrat  16059  bpoly4  16232  cos1bnd  16362  sin01gt0  16365  sincos1sgn  16368  ruclem8  16412  p1modz1  16436  nnoddm1d2  16563  sadcadd  16635  dvdsnprmd  16872  isprm7  16891  divdenle  16932  43prm  17307  plendxnocndx  17562  ipostr  18710  srgbinomlem4  20462  abvtrivd  21096  gzrngunit  21746  znidomb  21874  psgnodpmr  21903  leordtval2  23537  mopnex  24845  dscopn  24899  metnrmlem1a  25185  xrhmph  25275  evth  25287  xlebnum  25293  vitalilem5  25940  vitali  25941  ply1remlem  26490  plyremlem  26632  plyrem  26633  vieta1lem2  26641  reeff1olem  26780  sinhalfpilem  26799  rplogcl  26939  logtayllem  26994  cxplt  27029  cxple  27030  atanlogaddlem  27248  ressatans  27269  rlimcnp  27300  rlimcnp2  27301  cxp2limlem  27310  cxp2lim  27311  cxploglim2  27313  amgmlem  27324  emcllem2  27331  harmonicubnd  27344  fsumharmonic  27346  zetacvg  27349  ftalem1  27407  ftalem2  27408  chpchtsum  27553  chpub  27554  mersenne  27561  perfectlem2  27564  efexple  27615  chebbnd1  27806  dchrmusumlema  27827  dchrvmasumlem2  27832  dchrvmasumiflem1  27835  dchrisum0flblem2  27843  dchrisum0lema  27848  dchrisum0lem1  27850  dchrisum0lem2a  27851  mulog2sumlem1  27868  chpdifbndlem1  27887  chpdifbnd  27889  selberg3lem1  27891  pntrmax  27898  pntrsumo1  27899  pntpbnd1a  27919  pntpbnd2  27921  pntibndlem1  27923  pntlem3  27943  pnt  27948  ostth2lem1  27952  ostth2lem3  27969  ostth2lem4  27970  axcontlem2  29550  wwlksn0s  30457  clwwlkf1  30647  sgnmulsgp  33471  vietadeg1  34258  cos9thpiminplylem1  34462  cos9thpiminply  34468  esumcst  34743  hasheuni  34765  ballotlemi1  35183  ballotlemic  35187  signsply0  35228  signswch  35238  hgt750lem  35328  unblimceq0  37467  knoppndvlem1  37472  knoppndvlem2  37473  knoppndvlem7  37478  knoppndvlem13  37484  knoppndvlem14  37485  knoppndvlem15  37486  knoppndvlem17  37488  knoppndvlem20  37491  irrdiff  38354  poimirlem22  38667  poimirlem31  38676  asindmre  38728  areacirclem4  38736  60gcd7e1  43162  3lexlogpow5ineq2  43212  aks4d1p1p2  43227  aks4d1p7  43240  aks4d1p8d2  43242  aks4d1p8d3  43243  aks4d1p8  43244  aks4d1p9  43245  aks6d1c5lem3  43294  sticksstones11  43313  aks6d1c6lem1  43327  aks6d1c6lem4  43330  aks6d1c7lem2  43338  explt1d  43487  3cubeslem1  43801  pellexlem2  43944  pellexlem6  43948  pell14qrgt0  43973  elpell1qr2  43986  pellfundex  44000  pellfundrp  44002  rmxypos  44061  relexp01min  44820  imo72b2  45279  radcnvrat  45405  reclt0d  46505  sqrlearg  46672  sumnnodd  46749  liminf10ex  46891  liminfltlimsupex  46898  dvnmul  47060  stoweidlem7  47124  stoweidlem36  47153  stoweidlem38  47155  stoweidlem42  47159  stoweidlem51  47168  stoweidlem59  47176  stirlinglem5  47195  stirlinglem7  47197  stirlinglem10  47200  stirlinglem11  47201  stirlinglem12  47202  stirlinglem15  47205  dirkeritg  47219  fourierdlem11  47235  fourierdlem30  47254  fourierdlem47  47270  fourierdlem79  47302  fourierdlem103  47326  fourierdlem104  47327  fouriersw  47348  etransclem4  47355  etransclem31  47382  etransclem32  47383  etransclem35  47386  etransclem41  47392  salexct2  47456  hoidmvlelem1  47712  cjnpoly  48046  m1mod0mod1  48537  m1modmmod  48541  muldvdsfacgt  48563  muldvdsfacm1  48564  nfermltl2rev  48948  regt1loggt0  49755  rege1logbrege0  49777  nnlog2ge0lt1  49785  eenglngeehlnmlem2  49958  amgmwlem  51169