Theorem 0red 11177

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 11176	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  0cc0 11068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-rex 3054

This theorem is referenced by:  gt0ne0  11643  add20  11690  subge0  11691  lesub0  11695  mulge0  11696  msqgt0  11698  msqge0  11699  gt0ne0d  11742  addgt0d  11753  sublt0d  11804  prodgt0  12029  mulgt1  12044  lt2msq1  12067  fiminre2  12131  supmul1  12152  supmul  12155  nnne0  12220  0mnnnnn0  12474  nn0negleid  12494  neglt  12971  rpgecl  12981  ge0p1rp  12984  ledivge1le  13024  mul2lt0rlt0  13055  mul2lt0rgt0  13056  mul2lt0bi  13059  prodge0rd  13060  max0sub  13156  reltxrnmnf  13303  infmrp1  13305  lincmb01cmp  13456  iccf1o  13457  xov1plusxeqvd  13459  elfz0fzfz0  13594  fz0fzelfz0  13595  elfzo0z  13662  fzofzim  13670  fzo1fzo0n0  13676  elfzodifsumelfzo  13692  ssfzoulel  13721  elfznelfzo  13733  muladdmodid  13875  modltm1p1mod  13888  addmodlteq  13911  expgt1  14065  ltexp2a  14131  expcan  14134  ltexp2  14135  leexp2  14136  leexp2a  14137  zzlesq  14171  expnlbnd2  14199  discr  14205  fi1uzind  14472  ccatsymb  14547  ccat2s1fvw  14603  swrdnd  14619  swrdnnn0nd  14621  swrdswrdlem  14669  swrdswrd  14670  repswswrd  14749  swrd2lsw  14918  2swrd2eqwrdeq  14919  leabs  15265  max0add  15276  absgt0  15291  rlimrege0  15545  iseraltlem2  15649  fsumrecl  15700  o1fsum  15779  cvgcmp  15782  cvgcmpce  15784  geomulcvg  15842  mertenslem2  15851  fprodle  15962  rpnnen2lem4  16185  p1modz1  16229  moddvds  16233  oddge22np1  16319  bitsfzolem  16404  bitsinv1lem  16411  sadcaddlem  16427  nn0rppwr  16531  nn0expgcd  16534  lcmgcdlem  16576  dvdsnprmd  16660  2mulprm  16663  isprm7  16678  qnumgt0  16720  modprm0  16776  qexpz  16872  prmreclem4  16890  4sqlem6  16914  prmgaplem7  17028  gzrngunit  21350  regsumfsum  21352  regsumsupp  21531  fvmptnn04ifd  22740  chfacffsupp  22743  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulgsum  22751  prdsmet  24258  metustexhalf  24444  nlmvscnlem2  24573  nlmvscnlem1  24574  nmo0  24623  blcvx  24686  iihalf1cn  24826  evth  24858  lebnumlem1  24860  lebnumii  24865  htpycc  24879  pcohtpylem  24919  pcoass  24924  pcorevlem  24926  nmoleub2lem3  25015  ipcnlem2  25144  ipcnlem1  25145  rrxcph  25292  rrxmetlem  25307  rrxmet  25308  rrxdstprj1  25309  ehlbase  25315  minveclem3b  25328  minveclem6  25334  pjthlem1  25337  ovolicopnf  25425  ioorcl2  25473  volivth  25508  mbfposr  25553  i1fmulc  25604  itg1mulc  25605  itg1ge0a  25612  mbfi1flim  25624  itg2split  25650  itg2monolem1  25651  itg2monolem3  25653  itg2mono  25654  itg2cnlem2  25663  itgge0  25712  bddiblnc  25743  dvlip  25898  dvlipcn  25899  dveq0  25905  dv11cn  25906  dvlt0  25910  dvfsumge  25928  dgradd2  26174  plydivlem3  26203  mtest  26313  radcnvlem1  26322  radcnv0  26325  radcnvlt1  26327  radcnvle  26329  pserulm  26331  pserdvlem1  26337  pserdv  26339  abelthlem2  26342  abelthlem7  26348  pilem2  26362  pilem3  26363  coseq00topi  26411  tanabsge  26415  cosq34lt1  26436  tanord1  26446  tanord  26447  rplogcl  26513  logdivle  26531  logcnlem3  26553  logcnlem4  26554  dvloglem  26557  logtayl  26569  abscxp2  26602  cxplt  26603  cxple  26604  cxple2a  26608  cxpcn3lem  26657  abscxpbnd  26663  rtprmirr  26670  chordthmlem4  26745  chordthmlem5  26746  asinlem3  26781  atanre  26795  atanlogaddlem  26823  atanlogadd  26824  atanlogsublem  26825  atantan  26833  atans2  26841  efrlim  26879  efrlimOLD  26880  cxp2limlem  26886  cxp2lim  26887  cxploglim2  26889  divsqrtsumlem  26890  jensenlem2  26898  harmonicubnd  26920  fsumharmonic  26922  dmlogdmgm  26934  lgamgulmlem1  26939  lgamgulmlem2  26940  ftalem1  26983  ftalem2  26984  ftalem5  26987  vmacl  27028  chtwordi  27066  ppiwordi  27072  chtrpcl  27085  fsumfldivdiaglem  27099  fsumvma2  27125  chpval2  27129  chpchtsum  27130  chpub  27131  logfacbnd3  27134  logexprlim  27136  mersenne  27138  lgsdilem  27235  lgsne0  27246  gausslemma2dlem1a  27276  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  2sqmod  27347  2sqnn0  27349  chebbnd1lem2  27381  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  chtppilimlem2  27385  chtppilim  27386  chebbnd2  27388  chto1lb  27389  chpchtlim  27390  chpo1ub  27391  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  dchrmusumlema  27404  dchrvmasumlem2  27409  dchrvmasumiflem1  27412  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0re  27424  dchrisum0lema  27425  dchrisum0  27431  dirith2  27439  mulog2sumlem1  27445  vmalogdivsum2  27449  log2sumbnd  27455  selberg2lem  27461  chpdifbndlem1  27464  chpdifbnd  27466  selberg3lem1  27468  pntrmax  27475  pntrsumo1  27476  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntlemg  27509  pntlemj  27514  pntlemk  27517  pntlem3  27520  pnt2  27524  pnt  27525  ostth2lem1  27529  padicabv  27541  padicabvcxp  27543  ostth2lem3  27546  ostth2lem4  27547  ostth3  27549  trgcgrg  28442  tgcgr4  28458  axsegconlem7  28850  axsegconlem10  28853  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem10  28900  crctcshwlkn0lem3  29742  crctcshwlkn0  29751  clwlkclwwlklem2a2  29922  clwlkclwwlklem2a  29927  wwlksubclwwlk  29987  frgrogt3nreg  30326  friendshipgt3  30327  minvecolem5  30810  minvecolem6  30811  htthlem  30846  pjhthlem1  31320  sgnval2  32658  nndiffz1  32709  bcm1n  32718  fzo0opth  32728  expgt0b  32741  sgnneg  32758  sgnmul  32760  sgnsub  32762  nexple  32769  oexpled  32772  indf1o  32787  wrdt2ind  32875  cycpmrn  33100  cyc3conja  33114  ccfldextdgrr  33667  constrsslem  33731  constrresqrtcl  33767  constrsqrtcl  33769  cos9thpiminplylem1  33772  pnfneige0  33941  measinb  34211  eulerpartlems  34351  eulerpartlemgc  34353  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemodife  34489  signsply0  34542  signslema  34553  signsvtp  34574  itgexpif  34597  breprexplemc  34623  circlemeth  34631  logdivsqrle  34641  0nn0m1nnn0  35100  cvmliftlem2  35273  dnibndlem9  36474  unbdqndv2lem2  36498  knoppndvlem1  36500  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem11  36510  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem17  36516  knoppndvlem19  36518  knoppndvlem20  36519  bj-pinftynminfty  37215  poimirlem10  37624  poimirlem11  37625  poimirlem24  37638  poimirlem29  37643  poimirlem31  37645  poimirlem32  37646  poimir  37647  mblfinlem2  37652  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  areacirclem1  37702  areacirclem4  37705  areacirc  37707  geomcau  37753  isbnd3b  37779  prdsbnd  37787  bfp  37818  rrnequiv  37829  resdvopclptsd  42016  lcmineqlem2  42018  lcmineqlem3  42019  lcmineqlem10  42026  lcmineqlem12  42028  lcmineqlem23  42039  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  dvrelog2  42052  dvrelog3  42053  dvrelog2b  42054  0nonelalab  42055  dvrelogpow2b  42056  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8d2  42073  aks4d1p8d3  42074  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  primrootspoweq0  42094  aks6d1c1  42104  hashscontpow1  42109  aks6d1c2lem4  42115  aks6d1c5lem2  42126  deg1gprod  42128  2np3bcnp1  42132  2ap1caineq  42133  sticksstones7  42140  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem3  42160  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7lem2  42169  aks6d1c7  42172  aks5lem6  42180  unitscyglem5  42187  aks5lem8  42189  sn-1ne2  42253  oexpreposd  42310  posqsqznn  42324  redvmptabs  42348  readvrec  42350  re1m1e0m0  42385  re0m0e0  42390  remul01  42395  sn-remul0ord  42396  remulneg2d  42403  sn-addlt0d  42446  sn-addgt0d  42447  renegmulnnass  42453  zmulcomlem  42455  mulgt0con1dlem  42457  sn-mulgt1d  42467  mulltgt0d  42470  mullt0b2d  42472  sn-mullt0d  42473  sn-msqgt0d  42474  fimgmcyc  42522  dffltz  42622  3cubeslem1  42672  irrapxlem1  42810  irrapxlem2  42811  irrapxlem3  42812  irrapxlem4  42813  pellexlem6  42822  pell14qrgt0  42847  pell1qrgaplem  42861  pellfundex  42874  pellfundrp  42876  monotoddzzfi  42931  jm2.24  42952  jm2.23  42985  jm2.26lem3  42990  jm3.1lem3  43008  sqrtcvallem1  43620  reabsifneg  43621  reabsifpos  43623  sqrtcval  43630  k0004ss2  44141  imo72b2lem1  44158  dvgrat  44301  hashnzfz2  44310  binomcxplemnn0  44338  binomcxplemnotnn0  44345  divlt0gt0d  45284  upbdrech2  45306  xralrple2  45350  xralrple3  45370  reclt0d  45383  reclt0  45387  xrpnf  45481  fsumnncl  45570  fsumsupp0  45576  sumnnodd  45628  lptre2pt  45638  limsupubuz  45711  liminfresre  45777  liminf0  45791  dvmptconst  45913  dvdivbd  45921  dvcosax  45924  dvbdfbdioolem1  45926  dvbdfbdioolem2  45927  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvxpaek  45938  dvnxpaek  45940  volioc  45970  volico  45981  stoweidlem1  45999  stoweidlem7  46005  stoweidlem11  46009  stoweidlem25  46023  stoweidlem26  46024  stoweidlem34  46032  stoweidlem36  46034  stoweidlem41  46039  stoweidlem42  46040  stoweidlem44  46042  stoweidlem45  46043  wallispilem3  46065  wallispilem4  46066  wallispi  46068  stirlinglem3  46074  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  dirkeritg  46100  dirkercncflem2  46102  fourierdlem9  46114  fourierdlem11  46116  fourierdlem12  46117  fourierdlem14  46119  fourierdlem15  46120  fourierdlem19  46124  fourierdlem24  46129  fourierdlem28  46133  fourierdlem30  46135  fourierdlem40  46145  fourierdlem41  46146  fourierdlem43  46148  fourierdlem44  46149  fourierdlem47  46151  fourierdlem50  46154  fourierdlem51  46155  fourierdlem57  46161  fourierdlem60  46164  fourierdlem61  46165  fourierdlem66  46170  fourierdlem68  46172  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem78  46182  fourierdlem79  46183  fourierdlem83  46187  fourierdlem88  46192  fourierdlem92  46196  fourierdlem93  46197  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem109  46213  fourierdlem111  46215  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  elaa2lem  46231  etransclem4  46236  etransclem18  46250  etransclem19  46251  etransclem23  46255  etransclem27  46259  etransclem31  46263  etransclem32  46264  etransclem35  46267  etransclem41  46273  etransclem46  46278  etransclem48  46280  rrxtopnfi  46285  qndenserrnbllem  46292  salgencntex  46341  sge0tsms  46378  sge0isum  46425  volicorecl  46544  hoiprodcl  46545  ovnlerp  46560  ovnsubaddlem1  46568  hoiprodcl3  46578  volicore  46579  hoidmvcl  46580  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoi  46601  hoiqssbllem2  46621  volicorege0  46635  vonhoire  46670  pimrecltpos  46706  pimrecltneg  46722  smfmbfcex  46758  nsssmfmbflem  46776  smfrec  46787  smfmullem3  46791  smfdivdmmbl  46836  sharhght  46863  et-sqrtnegnre  46871  ormkglobd  46873  natglobalincr  46875  upwordnul  46878  zm1nn  47303  eluzge0nn0  47313  elfz2z  47316  2ffzoeq  47328  m1modmmod  47359  modm1p1ne  47371  iccpartigtl  47424  iccpartgt  47428  requad01  47622  requad1  47623  requad2  47624  stgrusgra  47958  gpgedgvtx1  48053  expnegico01  48507  regt1loggt0  48525  refdivmptf  48531  elbigolo1  48546  rege1logbrege0  48547  fllog2  48557  dignn0flhalflem1  48604  eenglngeehlnmlem2  48727  line2  48741  line2xlem  48742  line2x  48743  line2y  48744  itsclc0yqsol  48753  2itscp  48770  inlinecirc02plem  48775  amgmwlem  49791