Theorem 0red 11314

Description: The number 0 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
0red	⊢ (𝜑 → 0 ∈ ℝ)

Proof of Theorem 0red

Step	Hyp	Ref	Expression
1		0re 11313	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℝ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11202  0cc0 11203

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-ext 2732  ax-1cn 11261  ax-addrcl 11264  ax-rnegex 11274  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-rex 3087

This theorem is used by:  gt0ne0  11784  add20  11831  subge0  11832  lesub0  11836  mulge0  11837  msqgt0  11839  msqge0  11840  gt0ne0d  11883  addgt0d  11894  sublt0d  11945  prodgt0  12167  mulgt1  12181  lt2msq1  12204  fiminre2  12268  supmul1  12289  supmul  12292  nnne0  12375  0mnnnnn0  12641  nn0negleid  12661  0nn0m1nnn0  12756  neglt  13143  rpgecl  13153  ge0p1rp  13156  ledivge1le  13196  mul2lt0rlt0  13227  mul2lt0rgt0  13228  mul2lt0bi  13231  prodge0rd  13232  max0sub  13329  reltxrnmnf  13476  infmrp1  13478  lincmb01cmp  13629  iccf1o  13630  xov1plusxeqvd  13632  elfz0fzfz0  13770  fz0fzelfz0  13771  elfzo0z  13839  fzofzim  13847  fzo1fzo0n0  13853  elfzodifsumelfzo  13869  ssfzoulel  13898  elfznelfzo  13911  muladdmodid  14056  modltm1p1mod  14069  addmodlteq  14092  expgt1  14246  ltexp2a  14312  expcan  14315  ltexp2  14316  leexp2  14317  leexp2a  14318  zzlesq  14353  expnlbnd2  14381  discr  14387  fi1uzind  14655  ccatsymb  14731  ccat2s1fvw  14790  swrdnd  14808  swrdnnn0nd  14810  swrdswrdlem  14857  swrdswrd  14858  repswswrd  14939  swrd2lsw  15110  2swrd2eqwrdeq  15111  sgnneg  15258  sgnsub  15264  sgnmul  15265  leabs  15471  max0add  15482  absgt0  15497  rlimrege0  15751  iseraltlem2  15855  fsumrecl  15905  o1fsum  15985  cvgcmp  15988  cvgcmpce  15990  geomulcvg  16050  mertenslem2  16059  fprodle  16168  rpnnen2lem4  16390  p1modz1  16434  moddvds  16438  oddge22np1  16524  bitsfzolem  16609  bitsinv1lem  16616  sadcaddlem  16632  nn0rppwr  16740  nn0expgcd  16743  lcmgcdlem  16786  dvdsnprmd  16870  2mulprm  16873  isprm7  16889  qnumgt0  16931  posqsqznn  16941  modprm0  16988  qexpz  17084  prmreclem4  17102  4sqlem6  17126  prmgaplem7  17240  gzrngunit  21744  regsumfsum  21746  regsumsupp  21933  fvmptnn04ifd  23176  chfacffsupp  23179  chfacfscmul0  23181  chfacfscmulgsum  23183  chfacfpmmul0  23185  chfacfpmmulgsum  23187  prdsmet  24694  metustexhalf  24880  nlmvscnlem2  25009  nlmvscnlem1  25010  nmo0  25059  blcvx  25122  iihalf1cn  25258  evth  25285  lebnumlem1  25287  lebnumii  25292  htpycc  25306  pcohtpylem  25345  pcoass  25350  pcorevlem  25352  nmoleub2lem3  25441  ipcnlem2  25570  ipcnlem1  25571  rrxcph  25718  rrxmetlem  25733  rrxmet  25734  rrxdstprj1  25735  minveclem3b  25754  minveclem6  25760  pjthlem1  25763  ovolicopnf  25850  ioorcl2  25898  volivth  25933  mbfposr  25978  i1fmulc  26029  itg1mulc  26030  itg1ge0a  26037  mbfi1flim  26049  itg2split  26075  itg2monolem1  26076  itg2monolem3  26078  itg2mono  26079  itg2cnlem2  26088  itgge0  26136  bddiblnc  26167  dvlip  26318  dvlipcn  26319  dveq0  26325  dv11cn  26326  dvlt0  26330  dvfsumge  26347  dgradd2  26592  plydivlem3  26621  mtest  26736  radcnvlem1  26745  radcnv0  26748  radcnvlt1  26750  radcnvle  26752  pserulm  26754  pserdvlem1  26759  pserdv  26761  abelthlem2  26764  abelthlem7  26770  pilem2  26784  pilem3  26785  coseq00topi  26836  tanabsge  26840  cosq34lt1  26860  tanord1  26870  tanord  26871  rplogcl  26937  logdivle  26955  logcnlem3  26977  logcnlem4  26978  dvloglem  26981  logtayl  26993  abscxp2  27026  cxplt  27027  cxple  27028  cxple2a  27032  cxpcn3lem  27080  abscxpbnd  27086  rtprmirr  27093  chordthmlem4  27168  chordthmlem5  27169  asinlem3  27204  atanre  27218  atanlogaddlem  27246  atanlogadd  27247  atanlogsublem  27248  atantan  27256  atans2  27264  efrlim  27302  cxp2limlem  27308  cxp2lim  27309  cxploglim2  27311  divsqrtsumlem  27312  jensenlem2  27320  harmonicubnd  27342  fsumharmonic  27344  dmlogdmgm  27356  lgamgulmlem1  27361  lgamgulmlem2  27362  ftalem1  27405  ftalem2  27406  ftalem5  27409  vmacl  27450  chtwordi  27488  ppiwordi  27494  chtrpcl  27507  fsumfldivdiaglem  27521  fsumvma2  27546  chpval2  27550  chpchtsum  27551  chpub  27552  logfacbnd3  27555  logexprlim  27557  mersenne  27559  lgsdilem  27656  lgsne0  27667  gausslemma2dlem1a  27697  lgseisen  27711  lgsquadlem1  27712  lgsquadlem2  27713  2sqmod  27768  2sqnn0  27770  chebbnd1lem2  27802  chebbnd1lem3  27803  chebbnd1  27804  chtppilimlem1  27805  chtppilimlem2  27806  chtppilim  27807  chebbnd2  27809  chto1lb  27810  chpchtlim  27811  chpo1ub  27812  dchrisumlema  27820  dchrisumlem2  27822  dchrisumlem3  27823  dchrmusumlema  27825  dchrvmasumlem2  27830  dchrvmasumiflem1  27833  dchrisum0flblem1  27840  dchrisum0flblem2  27841  dchrisum0re  27845  dchrisum0lema  27846  dchrisum0  27852  dirith2  27860  mulog2sumlem1  27866  vmalogdivsum2  27870  log2sumbnd  27876  selberg2lem  27882  chpdifbndlem1  27885  chpdifbnd  27887  selberg3lem1  27889  pntrmax  27896  pntrsumo1  27897  pntrlog2bndlem4  27912  pntrlog2bndlem5  27913  pntpbnd1a  27917  pntpbnd1  27918  pntpbnd2  27919  pntlemg  27930  pntlemj  27935  pntlemk  27938  pntlem3  27941  pnt2  27945  pnt  27946  ostth2lem1  27950  padicabv  27962  padicabvcxp  27964  ostth2lem3  27967  ostth2lem4  27968  ostth3  27970  trgcgrg  28983  tgcgr4  28999  axsegconlem7  29506  axsegconlem10  29509  axcontlem2  29548  axcontlem4  29550  axcontlem7  29553  axcontlem10  29556  crctcshwlkn0lem3  30406  crctcshwlkn0  30415  clwlkclwwlklem2a2  30589  clwlkclwwlklem2a  30594  wwlksubclwwlk  30654  frgrogt3nreg  31003  friendshipgt3  31004  minvecolem5  31488  minvecolem6  31489  htthlem  31524  pjhthlem1  31998  sgnval2  33373  nndiffz1  33424  bcm1n  33433  fzo0opth  33441  expgt0b  33454  nexple  33470  oexpled  33473  indf1o  33477  wrdt2ind  33562  cycpmrn  33750  cyc3conja  33764  ccfldextdgrr  34350  constrsslem  34419  constrresqrtcl  34455  constrsqrtcl  34457  cos9thpiminplylem1  34460  pnfneige0  34629  measinb  34900  eulerpartlems  35038  eulerpartlemgc  35040  ballotlemfc0  35171  ballotlemfcc  35172  ballotlemodife  35176  signsply0  35226  signslema  35237  signsvtp  35258  itgexpif  35281  breprexplemc  35307  circlemeth  35315  logdivsqrle  35325  cvmliftlem2  36137  dnibndlem9  37444  unbdqndv2lem2  37468  knoppndvlem1  37470  knoppndvlem2  37471  knoppndvlem7  37476  knoppndvlem11  37480  knoppndvlem14  37483  knoppndvlem15  37484  knoppndvlem17  37486  knoppndvlem19  37488  knoppndvlem20  37489  bj-pinftynminfty  38241  poimirlem10  38641  poimirlem11  38642  poimirlem24  38655  poimirlem29  38660  poimirlem31  38662  poimirlem32  38663  poimir  38664  mblfinlem2  38669  ftc1anclem7  38710  ftc1anclem8  38711  ftc1anc  38712  areacirclem1  38719  areacirclem4  38722  areacirc  38724  geomcau  38786  isbnd3b  38812  prdsbnd  38820  bfp  38851  rrnequiv  38862  resdvopclptsd  43171  lcmineqlem2  43173  lcmineqlem3  43174  lcmineqlem10  43181  lcmineqlem12  43183  lcmineqlem23  43194  3lexlogpow5ineq1  43197  3lexlogpow5ineq2  43198  3lexlogpow5ineq4  43199  3lexlogpow5ineq3  43200  3lexlogpow2ineq2  43202  3lexlogpow5ineq5  43203  aks4d1lem1  43205  dvrelog2  43207  dvrelog3  43208  dvrelog2b  43209  0nonelalab  43210  dvrelogpow2b  43211  aks4d1p1p3  43212  aks4d1p1p2  43213  aks4d1p1p4  43214  aks4d1p1p6  43216  aks4d1p1p7  43217  aks4d1p1p5  43218  aks4d1p1  43219  aks4d1p2  43220  aks4d1p3  43221  aks4d1p5  43223  aks4d1p6  43224  aks4d1p7d1  43225  aks4d1p7  43226  aks4d1p8d2  43228  aks4d1p8d3  43229  aks4d1p8  43230  aks4d1p9  43231  posbezout  43243  primrootspoweq0  43249  aks6d1c1  43259  hashscontpow1  43264  aks6d1c2lem4  43270  aks6d1c5lem2  43281  deg1gprod  43283  2np3bcnp1  43287  2ap1caineq  43288  sticksstones7  43295  sticksstones10  43298  sticksstones12a  43300  sticksstones12  43301  sticksstones22  43311  aks6d1c6lem3  43315  bcled  43321  bcle2d  43322  aks6d1c7lem1  43323  aks6d1c7lem2  43324  aks6d1c7  43327  aks5lem6  43335  unitscyglem5  43342  aks5lem8  43344  sn-1ne2  43423  oexpreposd  43472  redvmptabs  43504  readvrec  43506  re1m1e0m0  43541  re0m0e0  43546  remul01  43551  sn-remul0ord  43552  remulneg2d  43559  rediveq0d  43593  sn-rediv0d  43597  sn-addlt0d  43615  sn-addgt0d  43616  renegmulnnass  43622  zmulcomlem  43624  mulgt0con1dlem  43626  sn-mulgt1d  43636  mulltgt0d  43639  mullt0b2d  43641  sn-mullt0d  43642  sn-msqgt0d  43643  fimgmcyc  43691  dffltz  43763  3cubeslem1  43787  irrapxlem1  43922  irrapxlem2  43923  irrapxlem3  43924  irrapxlem4  43925  pellexlem6  43934  pell14qrgt0  43959  pell1qrgaplem  43973  pellfundex  43986  pellfundrp  43988  monotoddzzfi  44042  jm2.24  44063  jm2.23  44096  jm2.26lem3  44101  jm3.1lem3  44119  sqrtcvallem1  44724  reabsifneg  44725  reabsifpos  44727  sqrtcval  44734  k0004ss2  45245  imo72b2lem1  45262  dvgrat  45389  hashnzfz2  45398  binomcxplemnn0  45426  binomcxplemnotnn0  45433  divlt0gt0d  46395  upbdrech2  46417  xralrple2  46459  xralrple3  46478  reclt0d  46491  reclt0  46495  xrpnf  46588  fsumnncl  46677  fsumsupp0  46683  sumnnodd  46735  lptre2pt  46743  limsupubuz  46816  liminfresre  46882  liminf0  46896  dvmptconst  47018  dvdivbd  47026  dvcosax  47029  dvbdfbdioolem1  47031  dvbdfbdioolem2  47032  ioodvbdlimc1lem1  47034  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  dvxpaek  47043  dvnxpaek  47045  volioc  47075  volico  47086  stoweidlem1  47104  stoweidlem7  47110  stoweidlem11  47114  stoweidlem25  47128  stoweidlem26  47129  stoweidlem34  47137  stoweidlem36  47139  stoweidlem41  47144  stoweidlem42  47145  stoweidlem44  47147  stoweidlem45  47148  wallispilem3  47170  wallispilem4  47171  wallispi  47173  stirlinglem3  47179  stirlinglem5  47181  stirlinglem6  47182  stirlinglem7  47183  stirlinglem10  47186  stirlinglem11  47187  stirlinglem12  47188  dirkeritg  47205  dirkercncflem2  47207  fourierdlem9  47219  fourierdlem11  47221  fourierdlem12  47222  fourierdlem14  47224  fourierdlem15  47225  fourierdlem19  47229  fourierdlem24  47234  fourierdlem28  47238  fourierdlem30  47240  fourierdlem40  47250  fourierdlem41  47251  fourierdlem43  47253  fourierdlem44  47254  fourierdlem47  47256  fourierdlem50  47259  fourierdlem51  47260  fourierdlem57  47266  fourierdlem60  47269  fourierdlem61  47270  fourierdlem66  47275  fourierdlem68  47277  fourierdlem73  47282  fourierdlem74  47283  fourierdlem75  47284  fourierdlem78  47287  fourierdlem79  47288  fourierdlem83  47292  fourierdlem88  47297  fourierdlem92  47301  fourierdlem93  47302  fourierdlem97  47306  fourierdlem103  47312  fourierdlem104  47313  fourierdlem109  47318  fourierdlem111  47320  sqwvfoura  47331  sqwvfourb  47332  fourierswlem  47333  fouriersw  47334  elaa2lem  47336  etransclem4  47341  etransclem18  47355  etransclem19  47356  etransclem23  47360  etransclem27  47364  etransclem31  47368  etransclem32  47369  etransclem35  47372  etransclem41  47378  etransclem46  47383  etransclem48  47385  rrxtopnfi  47390  qndenserrnbllem  47397  salgencntex  47446  sge0tsms  47483  sge0isum  47530  volicorecl  47649  hoiprodcl  47650  ovnlerp  47665  ovnsubaddlem1  47673  hoiprodcl3  47683  volicore  47684  hoidmvcl  47685  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem3  47700  ovnhoi  47706  hoiqssbllem2  47726  volicorege0  47740  vonhoire  47775  pimrecltpos  47811  pimrecltneg  47827  smfmbfcex  47863  nsssmfmbflem  47881  smfrec  47892  smfmullem3  47896  smfdivdmmbl  47941  sharhght  47968  et-sqrtnegnre  47976  ormkglobd  47980  chnsubseqwl  47982  zm1nn  48465  eluzge0nn0  48475  elfz2z  48478  2ffzoeq  48491  m1modmmod  48527  modm1p1ne  48539  muldvdsfacm1  48550  iccpartigtl  48598  iccpartgt  48602  nprmdvdsfacm1lem4  48801  requad01  48812  requad1  48813  requad2  48814  stgrusgra  49150  gpgedgvtx1  49253  expnegico01  49723  regt1loggt0  49741  refdivmptf  49747  elbigolo1  49762  rege1logbrege0  49763  fllog2  49773  dignn0flhalflem1  49820  eenglngeehlnmlem2  49944  line2  49957  line2xlem  49958  line2x  49959  line2y  49960  itsclc0yqsol  49969  2itscp  49986  inlinecirc02plem  49991  veronesefvcl  51140  veronesev1lem  51141  veronesev2lem  51142  veronesev3lem  51143  veronesev4lem  51144  veronesev5lem  51145  veronesev6lem  51146  amgmwlem  51155