MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0lt1 Structured version   Visualization version   GIF version

Theorem 0lt1 10804
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
StepHypRef Expression
1 1re 10293 . . 3 1 ∈ ℝ
2 ax-1ne0 10258 . . 3 1 ≠ 0
3 msqgt0 10802 . . 3 ((1 ∈ ℝ ∧ 1 ≠ 0) → 0 < (1 · 1))
41, 2, 3mp2an 683 . 2 0 < (1 · 1)
5 ax-1cn 10247 . . 3 1 ∈ ℂ
65mulid1i 10298 . 2 (1 · 1) = 1
74, 6breqtri 4834 1 0 < 1
Colors of variables: wff setvar class
Syntax hints:  wcel 2155  wne 2937   class class class wbr 4809  (class class class)co 6842  cr 10188  0cc0 10189  1c1 10190   · cmul 10194   < clt 10328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-po 5198  df-so 5199  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523
This theorem is referenced by:  0le1  10805  eqneg  10999  elimgt0  11113  ltp1  11115  ltm1  11117  recgt0  11121  mulgt1  11136  reclt1  11172  recgt1  11173  recgt1i  11174  recp1lt1  11175  recreclt  11176  recgt0ii  11183  inelr  11264  nnge1  11303  nngt0  11306  0nnn  11309  nnrecgt0  11315  2pos  11382  3pos  11384  4pos  11386  5pos  11388  6pos  11389  7pos  11390  8pos  11391  9pos  11392  neg1lt0  11396  halflt1  11496  nn0p1gt0  11569  elnnnn0c  11585  elnnz1  11650  nn0lt10b  11686  recnz  11699  1rp  12032  divlt1lt  12097  divle1le  12098  ledivge1le  12099  nnledivrp  12140  xmulid1  12311  0nelfz1  12567  fz10  12569  fzpreddisj  12597  elfznelfzob  12782  1mod  12910  expgt1  13105  ltexp2a  13119  expcan  13120  ltexp2  13121  leexp2  13122  leexp2a  13123  expnbnd  13200  expnlbnd  13201  expnlbnd2  13202  expmulnbnd  13203  discr1  13207  bcn1  13304  hashnn0n0nn  13382  brfi1indALT  13483  s2fv0  13916  swrd2lsw  13981  2swrd2eqwrdeq  13982  2swrd2eqwrdeqOLD  13983  sgn1  14117  resqrex  14276  mulcn2  14611  cvgrat  14898  bpoly4  15072  cos1bnd  15199  sin01gt0  15202  sincos1sgn  15205  ruclem8  15248  p1modz1  15272  nnoddm1d2  15384  sadcadd  15461  dvdsnprmd  15683  isprm7  15699  divdenle  15736  43prm  16102  ipostr  17419  srgbinomlem4  18810  abvtrivd  19109  gzrngunit  20085  znidomb  20182  psgnodpmr  20208  thlle  20317  leordtval2  21296  mopnex  22603  dscopn  22657  metnrmlem1a  22940  xrhmph  23025  evth  23037  xlebnum  23043  vitalilem5  23670  vitali  23671  ply1remlem  24213  plyremlem  24350  plyrem  24351  vieta1lem2  24357  reeff1olem  24491  sinhalfpilem  24507  rplogcl  24641  logtayllem  24696  cxplt  24731  cxple  24732  atanlogaddlem  24931  ressatans  24952  rlimcnp  24983  rlimcnp2  24984  cxp2limlem  24993  cxp2lim  24994  cxploglim2  24996  amgmlem  25007  emcllem2  25014  harmonicubnd  25027  fsumharmonic  25029  zetacvg  25032  ftalem1  25090  ftalem2  25091  chpchtsum  25235  chpub  25236  mersenne  25243  perfectlem2  25246  efexple  25297  chebbnd1  25452  dchrmusumlema  25473  dchrvmasumlem2  25478  dchrvmasumiflem1  25481  dchrisum0flblem2  25489  dchrisum0lema  25494  dchrisum0lem1  25496  dchrisum0lem2a  25497  mulog2sumlem1  25514  chpdifbndlem1  25533  chpdifbnd  25535  selberg3lem1  25537  pntrmax  25544  pntrsumo1  25545  pntpbnd1a  25565  pntpbnd2  25567  pntibndlem1  25569  pntlem3  25589  pnt  25594  ostth2lem1  25598  ostth2lem3  25615  ostth2lem4  25616  axcontlem2  26136  wwlksn0s  27052  clwwlkf1OLD  27292  clwwlkf1  27297  esumcst  30572  hasheuni  30594  ballotlemi1  31012  ballotlemic  31016  sgnnbi  31055  sgnpbi  31056  sgnmulsgp  31060  signsply0  31077  signswch  31087  hgt750lem  31180  unblimceq0  32937  knoppndvlem1  32942  knoppndvlem2  32943  knoppndvlem7  32948  knoppndvlem13  32954  knoppndvlem14  32955  knoppndvlem15  32956  knoppndvlem17  32958  knoppndvlem20  32961  poimirlem22  33855  poimirlem31  33864  asindmre  33918  areacirclem4  33926  pellexlem2  38072  pellexlem6  38076  pell14qrgt0  38101  elpell1qr2  38114  pellfundex  38128  pellfundrp  38130  rmxypos  38191  relexp01min  38680  imo72b2  39149  radcnvrat  39187  reclt0d  40245  sqrlearg  40418  sumnnodd  40500  liminf10ex  40644  liminfltlimsupex  40651  dvnmul  40796  stoweidlem7  40861  stoweidlem36  40890  stoweidlem38  40892  stoweidlem42  40896  stoweidlem51  40905  stoweidlem59  40913  stirlinglem5  40932  stirlinglem7  40934  stirlinglem10  40937  stirlinglem11  40938  stirlinglem12  40939  stirlinglem15  40942  dirkeritg  40956  fourierdlem11  40972  fourierdlem30  40991  fourierdlem47  41007  fourierdlem79  41039  fourierdlem103  41063  fourierdlem104  41064  fouriersw  41085  etransclem4  41092  etransclem31  41119  etransclem32  41120  etransclem35  41123  etransclem41  41129  salexct2  41194  hoidmvlelem1  41449  m1mod0mod1  42073  m1modmmod  42985  regt1loggt0  42999  rege1logbrege0  43021  nnlog2ge0lt1  43029  amgmwlem  43220
  Copyright terms: Public domain W3C validator