MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0red Structured version   Unicode version

Theorem 0red 9508
Description:  0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
0red  |-  ( ph  ->  0  e.  RR )

Proof of Theorem 0red
StepHypRef Expression
1 0re 9507 . 2  |-  0  e.  RR
21a1i 11 1  |-  ( ph  ->  0  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1826   RRcr 9402   0cc0 9403
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-i2m1 9471  ax-1ne0 9472  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199
This theorem is referenced by:  gt0ne0  9935  add20  9982  subge0  9983  lesub0  9987  mulge0  9988  msqgt0  9990  msqge0  9991  addgt0d  10044  prodgt0  10304  prodge0  10306  lt2msq1  10344  supmul1  10424  supmul  10427  0mnnnnn0  10745  rpgecl  11165  ge0p1rp  11168  max0sub  11316  iccf1o  11585  xov1plusxeqvd  11587  elfz1b  11670  elfz0fzfz0  11701  fz0fzelfz0  11702  fzo1fzo0n0  11759  elfzo0z  11760  fzofzim  11764  elfzodifsumelfzo  11781  ssfzoulel  11805  elfznelfzo  11814  muladdmodid  11937  modltm1p1mod  11942  expgt1  12107  ltexp2a  12120  expcan  12121  ltexp2  12122  leexp2  12123  leexp2a  12124  expnlbnd2  12199  discr  12205  brfi1uzind  12436  ccatsymb  12509  ccat2s1fvw  12551  swrdnd  12568  swrdswrdlem  12595  swrdswrd  12596  swrdccatin2  12623  swrdccatin12lem3  12626  repswswrd  12667  swrd2lsw  12801  2swrd2eqwrdeq  12802  leabs  13134  max0add  13145  absgt0  13159  rlimrege0  13404  iseraltlem2  13507  fsumrecl  13558  o1fsum  13629  cvgcmp  13632  cvgcmpce  13634  geomulcvg  13687  mertenslem2  13696  rpnnen2lem4  13953  moddvds  13995  bitsfzolem  14086  bitsinv1lem  14093  sadcaddlem  14109  qnumgt0  14285  modprm0  14332  qexpz  14422  prmreclem4  14439  4sqlem6  14463  gzrngunit  18596  regsumsupp  18749  fvmptnn04ifd  19439  chfacffsupp  19442  chfacfscmul0  19444  chfacfscmulgsum  19446  chfacfpmmul0  19448  chfacfpmmulgsum  19450  prdsmet  20958  metustexhalf  21152  nlmvscnlem2  21279  nlmvscnlem1  21280  nmo0  21327  evth  21544  lebnumlem1  21546  lebnumii  21551  htpycc  21565  pcohtpylem  21604  pcoass  21609  pcorevlem  21611  nmoleub2lem3  21683  ipcnlem2  21769  ipcnlem1  21770  rrxcph  21909  rrxmetlem  21919  rrxmet  21920  rrxdstprj1  21921  ehlbase  21923  minveclem3b  21928  minveclem6  21934  pjthlem1  21937  ovolicopnf  22020  ioorcl2  22066  volivth  22101  mbfposr  22144  i1fmulc  22195  itg1mulc  22196  itg1ge0a  22203  mbfi1flim  22215  itg2split  22241  itg2monolem1  22242  itg2monolem3  22244  itg2mono  22245  itg2cnlem2  22254  itgge0  22302  dvlip  22479  dvlipcn  22480  dveq0  22486  dv11cn  22487  dvlt0  22491  dvfsumge  22508  dgradd2  22750  plydivlem3  22776  mtest  22884  radcnvlem1  22893  radcnv0  22896  radcnvlt1  22898  radcnvle  22900  pserulm  22902  pserdvlem1  22907  pserdv  22909  abelthlem2  22912  abelthlem7  22918  pilem2  22932  coseq00topi  22980  tanabsge  22984  tanord1  23009  tanord  23010  rplogcl  23076  logdivle  23094  logcnlem3  23112  logcnlem4  23113  dvloglem  23116  logtayl  23128  abscxp2  23161  cxplt  23162  cxple  23163  cxple2a  23167  cxpcn3lem  23208  abscxpbnd  23214  chordthmlem5  23283  asinlem3  23318  atanre  23332  atanlogaddlem  23360  atanlogadd  23361  atanlogsublem  23362  atantan  23370  atans2  23378  efrlim  23416  cxp2limlem  23422  cxp2lim  23423  cxploglim2  23425  divsqrtsumlem  23426  jensenlem2  23434  harmonicubnd  23456  fsumharmonic  23458  ftalem1  23463  ftalem2  23464  ftalem5  23467  vmacl  23509  chtwordi  23547  ppiwordi  23553  chtrpcl  23566  fsumfldivdiaglem  23582  fsumvma2  23606  chpval2  23610  chpchtsum  23611  chpub  23612  logfacbnd3  23615  logexprlim  23617  mersenne  23619  lgslem4  23691  lgsdilem  23714  lgsne0  23725  lgseisen  23745  lgsquadlem1  23746  lgsquadlem2  23747  chebbnd1lem2  23772  chebbnd1lem3  23773  chebbnd1  23774  chtppilimlem1  23775  chtppilimlem2  23776  chtppilim  23777  chebbnd2  23779  chto1lb  23780  chpchtlim  23781  chpo1ub  23782  dchrisumlema  23790  dchrisumlem2  23792  dchrisumlem3  23793  dchrmusumlema  23795  dchrvmasumlem2  23800  dchrvmasumiflem1  23803  dchrisum0flblem1  23810  dchrisum0flblem2  23811  dchrisum0re  23815  dchrisum0lema  23816  dchrisum0  23822  dirith2  23830  mulog2sumlem1  23836  vmalogdivsum2  23840  log2sumbnd  23846  selberg2lem  23852  chpdifbndlem1  23855  chpdifbndlem2  23856  chpdifbnd  23857  selberg3lem1  23859  pntrmax  23866  pntrsumo1  23867  pntrlog2bndlem4  23882  pntrlog2bndlem5  23883  pntpbnd1a  23887  pntpbnd1  23888  pntpbnd2  23889  pntlemg  23900  pntlemj  23905  pntlemk  23908  pntlem3  23911  pntleml  23913  pnt2  23915  pnt  23916  ostth2lem1  23920  padicabv  23932  padicabvcxp  23934  ostth2lem3  23937  ostth2lem4  23938  ostth3  23940  trgcgrg  24026  axsegconlem7  24347  axsegconlem10  24350  axcontlem2  24389  axcontlem4  24391  axcontlem7  24394  axcontlem10  24397  nvnencycllem  24764  clwwlkn0  24895  clwlkisclwwlklem2a2  24901  clwlkisclwwlklem2a  24906  wwlksubclwwlk  24925  frgraogt3nreg  25241  friendshipgt3  25242  minvecolem5  25914  minvecolem6  25915  htthlem  25951  pjhthlem1  26426  mul2lt0rlt0  27715  mul2lt0rgt0  27716  mul2lt0bi  27719  nndiffz1  27749  bcm1n  27753  2sqmod  27789  regsumfsum  27926  pnfneige0  28087  nexple  28158  indf1o  28172  measinb  28348  eulerpartlems  28482  eulerpartlemgc  28484  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemodife  28619  sgnneg  28662  sgnmul  28664  sgnsub  28666  signsply0  28691  signslema  28702  signsvtp  28723  signshf  28728  dmlogdmgm  28755  lgamgulmlem1  28760  lgamgulmlem2  28761  cvmliftlem2  28920  bddiblnc  30251  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  areacirclem1  30273  areacirclem4  30276  areacirc  30278  geomcau  30418  isbnd3b  30447  prdsbnd  30455  bfp  30486  rrnequiv  30497  irrapxlem1  30923  irrapxlem2  30924  irrapxlem3  30925  irrapxlem4  30926  pellexlem6  30935  pell14qrgt0  30960  pell1qrgaplem  30974  pellfundex  30987  pellfundrp  30989  monotoddzzfi  31043  jm2.24  31066  jm2.23  31104  jm2.26lem3  31109  jm3.1lem3  31127  isprm7  31360  dvgrat  31361  lcmgcdlem  31380  hashnzfz2  31394  binomcxplemnn0  31422  binomcxplemnotnn0  31429  neglt  31634  divlt0gt0d  31636  sublt0d  31661  upbdrech2  31674  fsumnncl  31738  fprodle  31770  sumnnodd  31802  lptre2pt  31812  dvmptconst  31876  dvdivbd  31886  dvcosax  31889  dvbdfbdioolem1  31891  dvbdfbdioolem2  31892  ioodvbdlimc1lem1  31894  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvxpaek  31903  dvnxpaek  31905  volioc  31937  stoweidlem1  31949  stoweidlem7  31955  stoweidlem11  31959  stoweidlem25  31973  stoweidlem26  31974  stoweidlem34  31982  stoweidlem36  31984  stoweidlem41  31989  stoweidlem42  31990  stoweidlem44  31992  stoweidlem45  31993  wallispilem3  32015  wallispilem4  32016  wallispi  32018  stirlinglem3  32024  stirlinglem5  32026  stirlinglem6  32027  stirlinglem7  32028  stirlinglem10  32031  stirlinglem11  32032  stirlinglem12  32033  dirkeritg  32050  dirkercncflem2  32052  fourierdlem9  32064  fourierdlem11  32066  fourierdlem12  32067  fourierdlem14  32069  fourierdlem15  32070  fourierdlem19  32074  fourierdlem24  32079  fourierdlem28  32083  fourierdlem30  32085  fourierdlem40  32095  fourierdlem41  32096  fourierdlem43  32098  fourierdlem44  32099  fourierdlem47  32102  fourierdlem50  32105  fourierdlem51  32106  fourierdlem57  32112  fourierdlem60  32115  fourierdlem61  32116  fourierdlem66  32121  fourierdlem68  32123  fourierdlem73  32128  fourierdlem74  32129  fourierdlem75  32130  fourierdlem78  32133  fourierdlem79  32134  fourierdlem83  32138  fourierdlem88  32143  fourierdlem92  32147  fourierdlem93  32148  fourierdlem97  32152  fourierdlem103  32158  fourierdlem104  32159  fourierdlem109  32164  fourierdlem111  32166  sqwvfoura  32177  sqwvfourb  32178  fourierswlem  32179  fouriersw  32180  elaa2lem  32182  etransclem4  32187  etransclem18  32201  etransclem19  32202  etransclem23  32206  etransclem27  32210  etransclem31  32214  etransclem32  32215  etransclem35  32218  etransclem41  32224  etransclem46  32229  etransclem48  32231  sharhght  32248  zm1nn  32646  eluzge0nn0  32650  elfz2z  32652  2ffzoeq  32661  expnegico01  33323  m1modmmod  33334  difmodm1lt  33335  regt1loggt0  33357  refdivmptf  33363  elbigolo1  33378  rege1logbrege0  33379  fllog2  33389  dignn0flhalflem1  33436  bj-pinftynminfty  34977  imo72b2lem1  38517
  Copyright terms: Public domain W3C validator