Theorem 0re 11117

Description: The number 0 is real. Remark: the first step could also be ax-icn 11068. See also 0reALT 11461. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 11-Oct-2022.)

Assertion

Ref	Expression
0re	⊢ 0 ∈ ℝ

Proof of Theorem 0re

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1cn 11067	. 2 ⊢ 1 ∈ ℂ
2		cnre 11112	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11080	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11092	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2816	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3130	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3122	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  (class class class)co 7349  ℂcc 11007  ℝcr 11008  0cc0 11009  1c1 11010  ici 11011   + caddc 11012   · cmul 11014

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 11067  ax-addrcl 11070  ax-rnegex 11080  ax-cnre 11082

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:  0red  11118  0xr  11162  axmulgt0  11190  ne0gt0  11221  00id  11291  mul02lem1  11292  mul02lem2  11293  mul02  11294  addrid  11296  ltaddneg  11332  addgt0  11606  addgegt0  11607  addgtge0  11608  addge0  11609  ltaddpos  11610  ltneg  11620  leneg  11623  lt0neg1  11626  lt0neg2  11627  le0neg1  11628  le0neg2  11629  addge01  11630  suble0  11634  mulge0  11638  msqge0  11641  0le1  11643  relin01  11644  gt0ne0i  11655  lt0ne0d  11685  elimge0  11963  ltm1  11966  recgt0  11970  prodgt0  11971  lemul1a  11978  ltmul12a  11980  lemul12a  11982  mulgt1OLD  11983  gt0div  11991  ge0div  11992  mulge0b  11995  lediv12a  12018  recgt1i  12022  recreclt  12024  ledivp1  12027  squeeze0  12028  recgt0ii  12031  ledivp1i  12050  ltdivp1i  12051  fimaxre2  12070  inelr  12118  crne0  12121  nnge1  12156  nngt0  12159  nnnle0  12161  nnne0  12162  nnrecgt0  12171  0le0  12229  halfge0  12340  nn0ssre  12388  nn0ge0  12409  nn0nlt0  12410  nn0le0eq0  12412  0mnnnnn0  12416  elnnnn0b  12428  elnnnn0c  12429  nn0sub  12434  elnnz  12481  0z  12482  elnn0z  12484  elnnz1  12501  recnz  12551  gtndiv  12553  fnn0ind  12575  10re  12610  rpge0  12907  rpneg  12927  0nrp  12930  0ltpnf  13024  mnflt0  13027  qsqueeze  13103  xneg0  13114  xaddrid  13143  xnn0xadd0  13149  xmulpnf1  13176  xlemul1a  13190  xadddi  13197  xrsupsslem  13209  xrinfmsslem  13210  elrege0  13357  0e0icopnf  13361  elicc01  13369  0elunit  13372  unitssre  13402  0nelfz1  13446  fzpreddisj  13476  fz0to4untppr  13533  fz0to5un2tp  13534  nn0p1elfzo  13605  ico01fl0  13723  rpsup  13770  modelico  13785  0mod  13806  1mod  13807  le2sq2  14042  expubnd  14085  sqlecan  14116  bernneq2  14137  expnbnd  14139  expnlbnd  14140  expmulnbnd  14142  discr1  14146  discr  14147  faclbnd  14197  faclbnd3  14199  faclbnd6  14206  bcval4  14214  bcval5  14225  bcpasc  14228  hasheq0  14270  hashneq0  14271  hashnn0n0nn  14298  hashgt12el  14329  hashgt12el2  14330  hashge2el2dif  14387  lsw0  14472  swrdccatin2  14635  pfxccatin12lem3  14638  reim0  15025  re0  15059  im0  15060  rei  15063  imi  15064  cj0  15065  sqeqd  15073  rennim  15146  cnpart  15147  sqrt0  15148  01sqrexlem4  15152  resqrex  15157  sqrtgt0  15165  sqrt00  15170  sqrtneglem  15173  sqrt9  15180  sqrt2gt1lt2  15181  leabs  15206  absor  15207  max0add  15217  eqsqrt2d  15276  sqrtpclii  15290  rlimconst  15451  rlimrege0  15486  lo1mul  15535  iserge0  15568  fsum00  15705  isumless  15752  arisum2  15768  georeclim  15779  geo2sum  15780  geoisumr  15785  0.999...  15788  cvgrat  15790  fprodge0  15900  bpoly4  15966  cos0  16059  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  cos2bnd  16097  sin01gt0  16099  cos01gt0  16100  sincos2sgn  16103  sin4lt0  16104  absef  16106  absefib  16107  efieq1re  16108  epos  16116  rpnnen2lem2  16124  rpnnen2lem3  16125  rpnnen2lem4  16126  rpnnen2lem9  16131  ruclem6  16144  dvdslelem  16220  divalglem1  16305  divalglem5  16308  divalglem6  16309  flodddiv4  16326  sadcadd  16369  gcdn0gt0  16429  nn0seqcvgd  16481  algcvgblem  16488  algcvga  16490  pythagtriplem12  16738  pythagtriplem13  16739  pythagtriplem14  16740  pythagtriplem16  16742  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  1arith  16839  ramz  16937  mulgnegnn  18963  subgmulg  19019  srgbinomlem4  20114  isabvd  20697  abvtrivd  20717  rge0srg  21345  xrs1mnd  21347  xrs10  21348  psgnodpmr  21497  re0g  21519  psrbaglesupp  21829  psdmvr  22054  mnfnei  23106  imasdsf1olem  24259  ssblps  24308  ssbl  24309  xmeter  24319  dscmet  24458  dscopn  24459  nmoi  24614  nmoeq0  24622  0nghm  24627  idnghm  24629  cnbl0  24659  xrsxmet  24696  metdseq0  24741  iicmp  24777  iiconn  24778  iihalf1  24823  iihalf1cnOLD  24825  elii1  24829  icopnfcnv  24838  icopnfhmeo  24839  iccpnfcnv  24840  xrhmeo  24842  xrhmph  24843  htpycc  24877  reparphti  24894  reparphtiOLD  24895  pcoval1  24911  pco0  24912  pcoval2  24914  pcocn  24915  pcohtpylem  24917  pcopt  24920  pcopt2  24921  pcoass  24922  pcorevlem  24924  reust  25279  recusp  25280  rrx0el  25296  minveclem4c  25323  minveclem2  25324  minveclem3b  25326  minveclem4  25330  minveclem7  25333  pjthlem1  25335  cniccbdd  25360  ovolunnul  25399  ovoliunnul  25406  ovolicc1  25415  ovolre  25424  iccvolcl  25466  ovolioo  25467  ioovolcl  25469  ioorcl  25476  vitalilem4  25510  vitalilem5  25511  vitali  25512  ismbf  25527  mbfmulc2lem  25546  mbfpos  25550  mbfposr  25551  i1f0  25586  i1f1  25589  itg1addlem2  25596  itg1addlem4  25598  itg1addlem5  25599  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  mbfi1flimlem  25621  xrge0f  25630  itg2ge0  25634  itg2const  25639  itg2mulc  25646  itg2splitlem  25647  itg2gt0  25659  itg2cnlem1  25660  ibl0  25686  iblrelem  25690  iblposlem  25691  iblpos  25692  iblre  25693  itgreval  25696  itgneg  25703  iblss  25704  i1fibl  25707  itgitg1  25708  itgle  25709  itgeqa  25713  itgless  25716  iblconst  25717  itgconst  25718  ibladdlem  25719  itgaddlem2  25723  iblabslem  25727  iblabsr  25729  iblmulc2  25730  itgmulc2lem2  25732  itgabs  25734  itgsplit  25735  bddmulibl  25738  dvferm1  25887  dvferm2  25889  dvferm  25890  dvlip  25896  c1lip1  25900  dveq0  25903  dv11cn  25904  dvne0  25914  ftc1lem4  25944  ply1divex  26040  dgrco  26179  plyrecj  26185  vieta1lem2  26217  aalioulem2  26239  aalioulem3  26240  pserulm  26329  psercnlem2  26332  psercnlem1  26333  psercn  26334  abelth  26349  reeff1olem  26354  reeff1o  26355  pilem2  26360  pilem3  26361  pipos  26366  sinhalfpilem  26370  sincosq1sgn  26405  sincosq2sgn  26406  coseq00topi  26409  coseq0negpitopi  26410  tangtx  26412  tanabsge  26413  sinq12ge0  26415  sinq34lt0t  26416  cosq14ge0  26418  sincos4thpi  26420  sincos6thpi  26423  pige3ALT  26427  sineq0  26431  cosordlem  26437  cosord  26438  cos0pilt1  26439  cos11  26440  sinord  26441  recosf1o  26442  resinf1o  26443  tanord1  26444  tanord  26445  tanregt0  26446  efif1olem4  26452  efifo  26454  relogrn  26468  log1  26492  logi  26494  logneg  26495  argregt0  26517  argrege0  26518  argimgt0  26519  logneg2  26522  logdivlti  26527  logdivlt  26528  ellogdm  26546  logdmn0  26547  logdmnrp  26548  logcnlem3  26551  dvloglem  26555  logdmopn  26556  logf1o2  26557  dvlog2lem  26559  efopnlem1  26563  logtayl  26567  recxpcl  26582  cxpge0  26590  cxple2  26604  cxple2a  26606  cxpsqrtlem  26609  cxpcn3  26656  cxpaddlelem  26659  cxpaddle  26660  loglesqrt  26669  logbrec  26690  ang180lem3  26719  ang180lem4  26720  asinneg  26794  asin1  26802  reasinsin  26804  acosbnd  26808  atan0  26816  atanrecl  26819  atanlogaddlem  26821  atanlogsublem  26823  atanlogsub  26824  atantan  26831  atanbnd  26834  atan1  26836  atans2  26839  ressatans  26842  log2cnv  26852  log2tlbnd  26853  log2ub  26857  log2le1  26858  rlimcnp  26873  rlimcnp2  26874  o1cxp  26883  jensen  26897  amgm  26899  emgt0  26915  harmonicbnd3  26916  harmoniclbnd  26917  harmonicbnd4  26919  zetacvg  26923  eldmgm  26930  lgamgulmlem2  26938  basellem3  26991  basellem8  26996  efnnfsumcl  27011  ppisval  27012  vmage0  27029  chpge0  27034  efchtdvds  27067  ppiltx  27085  ppiub  27113  chpeq0  27117  chteq0  27118  chtleppi  27119  chpchtsum  27128  chpub  27129  dchr1re  27172  bcmono  27186  efexple  27190  bposlem1  27193  bposlem4  27196  bposlem5  27197  bposlem7  27199  bposlem8  27200  bposlem9  27201  lgsval2lem  27216  lgsval4a  27228  lgsneg  27230  lgsdilem  27233  lgsdir2lem1  27234  2lgsoddprmlem3a  27319  2lgsoddprmlem3b  27320  2lgsoddprmlem3c  27321  2lgsoddprmlem3d  27322  rplogsumlem2  27394  rpvmasumlem  27396  dchrisum0flblem1  27417  dchrisum0flblem2  27418  dchrisum0fno1  27420  rplogsum  27436  logdivsum  27442  mulog2sumlem2  27444  selberg2lem  27459  logdivbnd  27465  pntrsumo1  27474  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  pntpbnd1  27495  pntpbnd2  27496  pntlem3  27518  pntleml  27520  ostth2  27546  trgcgrg  28460  ttgcontlem1  28830  axlowdimlem1  28887  axlowdimlem6  28892  axlowdimlem7  28893  axlowdimlem10  28896  axlowdim1  28904  axlowdim2  28905  axlowdim  28906  elntg2  28930  umgrislfupgrlem  29067  lfgrnloop  29070  lfuhgr1v0e  29199  usgrexmplef  29204  pthdlem2  29713  crctcshwlkn0lem7  29761  rusgrnumwwlks  29919  clwwlkn0  29972  konigsberg  30201  ex-po  30379  ex-sqrt  30398  ex-gcd  30401  nvz0  30612  0blo  30736  nmlno0lem  30737  nmblolbii  30743  siilem2  30796  minvecolem2  30819  minvecolem3  30820  minvecolem4c  30823  minvecolem4  30824  minvecolem5  30825  minvecolem7  30827  htthlem  30861  hiidge0  31042  normlem6  31059  normgt0  31071  norm-i  31073  normpyc  31090  bcsiALT  31123  pjhthlem1  31335  pjneli  31667  nmlnop0iALT  31939  unopbd  31959  nmbdoplbi  31968  nmcoplbi  31972  nmbdfnlbi  31993  nmbdfnlb  31994  nmcfnlbi  31996  cnlnadjlem7  32017  nmopcoi  32039  branmfn  32049  leopmul  32078  nmopleid  32083  pjbdlni  32093  pjnormssi  32112  stle0i  32183  cdj3lem1  32378  xaddeq0  32696  expgt0b  32761  pr01ssre  32769  sgnclre  32777  sgnnbi  32783  sgnpbi  32784  indf  32798  indfval  32799  dp20u  32818  dp20h  32819  dp2clq  32821  dp2lt10  32824  dp2lt  32825  dp0u  32841  dplti  32845  dpexpp1  32848  xdiv0  32869  chnub  32954  xrge0slmod  33285  evl1deg3  33513  fldext2chn  33695  cos9thpiminplylem1  33749  unitdivcld  33868  sqsscirc1  33875  xrge0iifcnv  33900  xrge0iifiso  33902  rezh  33936  esumcvgsum  34055  voliune  34196  volfiniune  34197  sibfinima  34307  sitmcl  34319  0rrv  34419  coinfliprv  34451  ballotlem2  34457  ballotlem4  34467  ballotlemi1  34471  ballotlemic  34475  plymulx0  34515  signsply0  34519  signswch  34529  signstf  34534  signstf0  34536  signstfveq0  34545  signlem0  34555  signshf  34556  itgexpif  34574  hgt750lemd  34616  hgt750lem  34619  hgt750lem2  34620  hgt750leme  34626  iisconn  35225  iillysconn  35226  cvmliftlem10  35267  fz0n  35704  bcneg1  35709  nn0prpwlem  36296  dnizeq0  36449  dnizphlfeqhlf  36450  knoppndvlem13  36498  cnndvlem1  36511  bj-pinftyccb  37195  bj-minftyccb  37199  bj-pinftynminfty  37201  taupilemrplb  37294  irrdiff  37300  sin2h  37590  tan2h  37592  ptrecube  37600  poimirlem16  37616  poimirlem17  37617  poimirlem20  37620  poimirlem22  37622  poimirlem23  37623  poimirlem29  37629  poimirlem31  37631  poimir  37633  heicant  37635  mblfinlem2  37638  ismblfin  37641  ovoliunnfl  37642  voliunnfl  37644  volsupnfl  37645  mbfposadd  37647  itg2addnclem  37651  itg2addnclem2  37652  ibladdnclem  37656  itgaddnclem2  37659  iblabsnclem  37663  iblmulc2nc  37665  itgmulc2nclem2  37667  itgabsnc  37669  ftc1cnnclem  37671  ftc1anclem5  37677  ftc1anclem8  37680  asindmre  37683  dvasin  37684  areacirclem4  37691  areacirc  37693  isbnd3  37764  ssbnd  37768  prdsbnd  37773  bfplem2  37803  bfp  37804  renegclALT  38942  0cnALT3  42226  sn-1ne2  42238  itrere  42291  oexpreposd  42295  tan3rdpi  42325  asin1half  42330  readvrec2  42334  sn-00idlem2  42372  sn-00idlem3  42373  sn-00id  42374  sn-0tie0  42424  sn-ltaddpos  42426  sn-ltaddneg  42427  relt0neg1  42429  sn-nnne0  42433  reelznn0nn  42434  sn-0lt1  42448  sn-inelr  42460  sn-itrere  42461  sn-retire  42462  pellexlem6  42807  elpell14qr2  42835  oddcomabszz  42917  zindbi  42919  jm2.24  42936  acongeq  42956  arearect  43188  areaquad  43189  reabsifneg  43605  reabsifnpos  43606  reabsifpos  43607  reabsifnneg  43608  imsqrtvalex  43619  relexp01min  43686  imo72b2lem2  44140  imo72b2lem1  44142  imo72b2  44145  dvconstbi  44307  binomcxplemnn0  44322  binomcxplemdvbinom  44326  binomcxplemcvg  44327  binomcxplemnotnn0  44329  sineq0ALT  44910  halffl  45278  ren0  45381  rexanuz2nf  45471  sqrlearg  45534  limsup10ex  45754  dvnmptdivc  45919  dvnmul  45924  itgsin0pilem1  45931  itgsinexplem1  45935  itgsinexp  45936  iblempty  45946  stoweidlem17  45998  stoweidlem36  46017  stoweidlem55  46036  wallispilem1  46046  wallispilem2  46047  wallispilem4  46049  stirlinglem4  46058  stirlinglem13  46067  stirlinglem14  46068  stirlinglem15  46069  stirlingr  46071  dirker2re  46073  dirkerdenne0  46074  dirkerre  46076  dirkertrigeqlem1  46079  dirkercncflem2  46085  dirkercncflem4  46087  fourierdlem11  46099  fourierdlem16  46104  fourierdlem21  46109  fourierdlem22  46110  fourierdlem41  46129  fourierdlem42  46130  fourierdlem48  46135  fourierdlem62  46149  fourierdlem66  46153  fourierdlem79  46166  fourierdlem83  46170  fourierdlem94  46181  fourierdlem102  46189  fourierdlem103  46190  fourierdlem104  46191  fourierdlem111  46198  fourierdlem112  46199  fourierdlem113  46200  fourierdlem114  46201  sqwvfoura  46209  sqwvfourb  46210  fourierswlem  46211  fouriersw  46212  etransclem23  46238  etransclem44  46259  etransclem46  46261  salexct3  46323  salgensscntex  46325  sge0rnn0  46349  sge00  46357  0ome  46510  ovn0lem  46546  ovnhoilem1  46582  smfmullem1  46772  smfmullem2  46773  smfmullem3  46774  smfmullem4  46775  squeezedltsq  46870  zm1nn  47286  sqrtnegnre  47291  m1mod0mod1  47338  fmtnoprmfac2lem1  47550  31prm  47581  mod42tp1mod8  47586  nfermltl2rev  47727  tgblthelfgott  47799  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb0  48015  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpgusgralem  48040  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem2lem3  48100  gpg5edgnedg  48114  altgsumbcALT  48337  expnegico01  48503  dignnld  48588  eenglngeehlnmlem1  48722  line2ylem  48736  line2y  48740  itsclc0yqsollem2  48748  icccldii  48903  i0oii  48904  sepfsepc  48912  ex-gt  49713