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

Theorem 0red 10079
Description: 0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
0red (𝜑 → 0 ∈ ℝ)

Proof of Theorem 0red
StepHypRef Expression
1 0re 10078 . 2 0 ∈ ℝ
21a1i 11 1 (𝜑 → 0 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cr 9973  0cc0 9974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  gt0ne0  10531  add20  10578  subge0  10579  lesub0  10583  mulge0  10584  msqgt0  10586  msqge0  10587  addgt0d  10640  sublt0d  10691  prodgt0  10906  prodge0  10908  lt2msq1  10945  supmul1  11030  supmul  11033  0mnnnnn0  11363  nn0negleid  11383  rpgecl  11897  ge0p1rp  11900  ledivge1le  11939  mul2lt0rlt0  11970  mul2lt0rgt0  11971  mul2lt0bi  11974  max0sub  12065  reltxrnmnf  12210  infmrp1  12212  iccf1o  12354  xov1plusxeqvd  12356  elfz0fzfz0  12483  fz0fzelfz0  12484  elfzo0z  12549  fzofzim  12554  fzo1fzo0n0  12558  elfzodifsumelfzo  12573  ssfzoulel  12602  elfznelfzo  12613  muladdmodid  12750  modltm1p1mod  12762  addmodlteq  12785  expgt1  12938  ltexp2a  12952  expcan  12953  ltexp2  12954  leexp2  12955  leexp2a  12956  expnlbnd2  13035  discr  13041  fi1uzind  13317  ccatsymb  13400  ccat2s1fvw  13460  swrdnd  13478  swrdswrdlem  13505  swrdswrd  13506  swrdccatin2  13533  swrdccatin12lem3  13536  repswswrd  13577  swrd2lsw  13741  2swrd2eqwrdeq  13742  leabs  14083  max0add  14094  absgt0  14108  rlimrege0  14354  iseraltlem2  14457  fsumrecl  14509  o1fsum  14589  cvgcmp  14592  cvgcmpce  14594  geomulcvg  14651  mertenslem2  14661  fprodle  14771  rpnnen2lem4  14990  p1modz1  15034  moddvds  15038  oddge22np1  15120  bitsfzolem  15203  bitsinv1lem  15210  sadcaddlem  15226  lcmgcdlem  15366  dvdsnprmd  15450  isprm7  15467  qnumgt0  15505  modprm0  15557  qexpz  15652  prmreclem4  15670  4sqlem6  15694  prmgaplem7  15808  gzrngunit  19860  regsumfsum  19862  regsumsupp  20016  fvmptnn04ifd  20706  chfacffsupp  20709  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulgsum  20717  prdsmet  22222  metustexhalf  22408  nlmvscnlem2  22536  nlmvscnlem1  22537  nmo0  22586  evth  22805  lebnumlem1  22807  lebnumii  22812  htpycc  22826  pcohtpylem  22865  pcoass  22870  pcorevlem  22872  nmoleub2lem3  22961  ipcnlem2  23089  ipcnlem1  23090  rrxcph  23226  rrxmetlem  23236  rrxmet  23237  rrxdstprj1  23238  ehlbase  23240  minveclem3b  23245  minveclem6  23251  pjthlem1  23254  ovolicopnf  23338  ioorcl2  23386  volivth  23421  mbfposr  23464  i1fmulc  23515  itg1mulc  23516  itg1ge0a  23523  mbfi1flim  23535  itg2split  23561  itg2monolem1  23562  itg2monolem3  23564  itg2mono  23565  itg2cnlem2  23574  itgge0  23622  dvlip  23801  dvlipcn  23802  dveq0  23808  dv11cn  23809  dvlt0  23813  dvfsumge  23830  dgradd2  24069  plydivlem3  24095  mtest  24203  radcnvlem1  24212  radcnv0  24215  radcnvlt1  24217  radcnvle  24219  pserulm  24221  pserdvlem1  24226  pserdv  24228  abelthlem2  24231  abelthlem7  24237  pilem2  24251  coseq00topi  24299  tanabsge  24303  tanord1  24328  tanord  24329  rplogcl  24395  logdivle  24413  logcnlem3  24435  logcnlem4  24436  dvloglem  24439  logtayl  24451  abscxp2  24484  cxplt  24485  cxple  24486  cxple2a  24490  cxpcn3lem  24533  abscxpbnd  24539  chordthmlem5  24608  asinlem3  24643  atanre  24657  atanlogaddlem  24685  atanlogadd  24686  atanlogsublem  24687  atantan  24695  atans2  24703  efrlim  24741  cxp2limlem  24747  cxp2lim  24748  cxploglim2  24750  divsqrtsumlem  24751  jensenlem2  24759  harmonicubnd  24781  fsumharmonic  24783  dmlogdmgm  24795  lgamgulmlem1  24800  lgamgulmlem2  24801  ftalem1  24844  ftalem2  24845  ftalem5  24848  vmacl  24889  chtwordi  24927  ppiwordi  24933  chtrpcl  24946  fsumfldivdiaglem  24960  fsumvma2  24984  chpval2  24988  chpchtsum  24989  chpub  24990  logfacbnd3  24993  logexprlim  24995  mersenne  24997  lgsdilem  25094  lgsne0  25105  gausslemma2dlem1a  25135  lgseisen  25149  lgsquadlem1  25150  lgsquadlem2  25151  chebbnd1lem2  25204  chebbnd1lem3  25205  chebbnd1  25206  chtppilimlem1  25207  chtppilimlem2  25208  chtppilim  25209  chebbnd2  25211  chto1lb  25212  chpchtlim  25213  chpo1ub  25214  dchrisumlema  25222  dchrisumlem2  25224  dchrisumlem3  25225  dchrmusumlema  25227  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0re  25247  dchrisum0lema  25248  dchrisum0  25254  dirith2  25262  mulog2sumlem1  25268  vmalogdivsum2  25272  log2sumbnd  25278  selberg2lem  25284  chpdifbndlem1  25287  chpdifbndlem2  25288  chpdifbnd  25289  selberg3lem1  25291  pntrmax  25298  pntrsumo1  25299  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntlemg  25332  pntlemj  25337  pntlemk  25340  pntlem3  25343  pntleml  25345  pnt2  25347  pnt  25348  ostth2lem1  25352  padicabv  25364  padicabvcxp  25366  ostth2lem3  25369  ostth2lem4  25370  ostth3  25372  trgcgrg  25455  tgcgr4  25471  axsegconlem7  25848  axsegconlem10  25851  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem10  25898  crctcshwlkn0lem3  26760  crctcshwlkn0  26769  clwlkclwwlklem2a2  26959  clwlkclwwlklem2a  26964  wwlksubclwwlk  27023  frgrogt3nreg  27384  friendshipgt3  27385  minvecolem5  27865  minvecolem6  27866  htthlem  27902  pjhthlem1  28378  nndiffz1  29676  bcm1n  29682  2sqmod  29776  pnfneige0  30125  nexple  30199  indf1o  30214  measinb  30412  eulerpartlems  30550  eulerpartlemgc  30552  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemodife  30687  sgnneg  30730  sgnmul  30732  sgnsub  30734  signsply0  30756  signslema  30767  signsvtp  30788  signshf  30793  itgexpif  30812  breprexplemc  30838  circlemeth  30846  logdivsqrle  30856  cvmliftlem2  31394  dnibndlem9  32601  unbdqndv2lem2  32626  knoppndvlem1  32628  knoppndvlem2  32629  knoppndvlem7  32634  knoppndvlem11  32638  knoppndvlem14  32641  knoppndvlem15  32642  knoppndvlem17  32644  knoppndvlem19  32646  knoppndvlem20  32647  bj-pinftynminfty  33244  poimirlem10  33549  poimirlem11  33550  poimirlem24  33563  poimirlem29  33568  poimirlem31  33570  poimirlem32  33571  poimir  33572  mblfinlem2  33577  bddiblnc  33610  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  areacirclem1  33630  areacirclem4  33633  areacirc  33635  geomcau  33685  isbnd3b  33714  prdsbnd  33722  bfp  33753  rrnequiv  33764  irrapxlem1  37703  irrapxlem2  37704  irrapxlem3  37705  irrapxlem4  37706  pellexlem6  37715  pell14qrgt0  37740  pell1qrgaplem  37754  pellfundex  37767  pellfundrp  37769  monotoddzzfi  37824  jm2.24  37847  jm2.23  37880  jm2.26lem3  37885  jm3.1lem3  37903  k0004ss2  38767  imo72b2lem1  38788  dvgrat  38828  hashnzfz2  38837  binomcxplemnn0  38865  binomcxplemnotnn0  38872  neglt  39810  divlt0gt0d  39812  upbdrech2  39836  xralrple2  39883  xralrple3  39903  fiminre2  39907  reclt0d  39920  reclt0  39927  xrpnf  40029  fsumnncl  40121  fsumsupp0  40128  sumnnodd  40180  lptre2pt  40190  limsupubuz  40263  liminfresre  40329  liminf0  40343  dvmptconst  40447  dvdivbd  40456  dvcosax  40459  dvbdfbdioolem1  40461  dvbdfbdioolem2  40462  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvxpaek  40473  dvnxpaek  40475  volioc  40506  volico  40518  stoweidlem1  40536  stoweidlem7  40542  stoweidlem11  40546  stoweidlem25  40560  stoweidlem26  40561  stoweidlem34  40569  stoweidlem36  40571  stoweidlem41  40576  stoweidlem42  40577  stoweidlem44  40579  stoweidlem45  40580  wallispilem3  40602  wallispilem4  40603  wallispi  40605  stirlinglem3  40611  stirlinglem5  40613  stirlinglem6  40614  stirlinglem7  40615  stirlinglem10  40618  stirlinglem11  40619  stirlinglem12  40620  dirkeritg  40637  dirkercncflem2  40639  fourierdlem9  40651  fourierdlem11  40653  fourierdlem12  40654  fourierdlem14  40656  fourierdlem15  40657  fourierdlem19  40661  fourierdlem24  40666  fourierdlem28  40670  fourierdlem30  40672  fourierdlem40  40682  fourierdlem41  40683  fourierdlem43  40685  fourierdlem44  40686  fourierdlem47  40688  fourierdlem50  40691  fourierdlem51  40692  fourierdlem57  40698  fourierdlem60  40701  fourierdlem61  40702  fourierdlem66  40707  fourierdlem68  40709  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem78  40719  fourierdlem79  40720  fourierdlem83  40724  fourierdlem88  40729  fourierdlem92  40733  fourierdlem93  40734  fourierdlem97  40738  fourierdlem103  40744  fourierdlem104  40745  fourierdlem109  40750  fourierdlem111  40752  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  elaa2lem  40768  etransclem4  40773  etransclem18  40787  etransclem19  40788  etransclem23  40792  etransclem27  40796  etransclem31  40800  etransclem32  40801  etransclem35  40804  etransclem41  40810  etransclem46  40815  etransclem48  40817  rrxtopnfi  40824  qndenserrnbllem  40832  salgencntex  40879  sge0tsms  40915  sge0isum  40962  volicorecl  41081  hoiprodcl  41082  ovnlerp  41097  ovnsubaddlem1  41105  hoiprodcl3  41115  volicore  41116  hoidmvcl  41117  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoi  41138  hoiqssbllem2  41158  volicorege0  41172  vonhoire  41207  pimrecltpos  41240  pimrecltneg  41254  smfmbfcex  41289  nsssmfmbflem  41307  smfrec  41317  smfmullem3  41321  sharhght  41375  zm1nn  41641  eluzge0nn0  41647  elfz2z  41650  2ffzoeq  41663  iccpartigtl  41684  iccpartgt  41688  expnegico01  42633  m1modmmod  42641  difmodm1lt  42642  regt1loggt0  42655  refdivmptf  42661  elbigolo1  42676  rege1logbrege0  42677  fllog2  42687  dignn0flhalflem1  42734  amgmwlem  42876
  Copyright terms: Public domain W3C validator