Theorem 0re 11132

Description: The number 0 is real. Remark: the first step could also be ax-icn 11083. See also 0reALT 11476. (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 11082	. 2 ⊢ 1 ∈ ℂ
2		cnre 11127	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11095	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11107	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2822	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3135	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3127	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3058  (class class class)co 7356  ℂcc 11022  ℝcr 11023  0cc0 11024  1c1 11025  ici 11026   + caddc 11027   · cmul 11029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-1cn 11082  ax-addrcl 11085  ax-rnegex 11095  ax-cnre 11097

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-clel 2809  df-rex 3059

This theorem is referenced by:  0red  11133  0xr  11177  axmulgt0  11205  ne0gt0  11236  00id  11306  mul02lem1  11307  mul02lem2  11308  mul02  11309  addrid  11311  ltaddneg  11347  addgt0  11621  addgegt0  11622  addgtge0  11623  addge0  11624  ltaddpos  11625  ltneg  11635  leneg  11638  lt0neg1  11641  lt0neg2  11642  le0neg1  11643  le0neg2  11644  addge01  11645  suble0  11649  mulge0  11653  msqge0  11656  0le1  11658  relin01  11659  gt0ne0i  11670  lt0ne0d  11700  elimge0  11978  ltm1  11981  recgt0  11985  prodgt0  11986  lemul1a  11993  ltmul12a  11995  lemul12a  11997  mulgt1OLD  11998  gt0div  12006  ge0div  12007  mulge0b  12010  lediv12a  12033  recgt1i  12037  recreclt  12039  ledivp1  12042  squeeze0  12043  recgt0ii  12046  ledivp1i  12065  ltdivp1i  12066  fimaxre2  12085  inelr  12133  crne0  12136  nnge1  12171  nngt0  12174  nnnle0  12176  nnne0  12177  nnrecgt0  12186  0le0  12244  halfge0  12355  nn0ssre  12403  nn0ge0  12424  nn0nlt0  12425  nn0le0eq0  12427  0mnnnnn0  12431  elnnnn0b  12443  elnnnn0c  12444  nn0sub  12449  elnnz  12496  0z  12497  elnn0z  12499  elnnz1  12515  recnz  12565  gtndiv  12567  fnn0ind  12589  10re  12624  rpge0  12917  rpneg  12937  0nrp  12940  0ltpnf  13034  mnflt0  13037  qsqueeze  13114  xneg0  13125  xaddrid  13154  xnn0xadd0  13160  xmulpnf1  13187  xlemul1a  13201  xadddi  13208  xrsupsslem  13220  xrinfmsslem  13221  elrege0  13368  0e0icopnf  13372  elicc01  13380  0elunit  13383  unitssre  13413  0nelfz1  13457  fzpreddisj  13487  fz0to4untppr  13544  fz0to5un2tp  13545  nn0p1elfzo  13616  ico01fl0  13737  rpsup  13784  modelico  13799  0mod  13820  1mod  13821  le2sq2  14056  expubnd  14099  sqlecan  14130  bernneq2  14151  expnbnd  14153  expnlbnd  14154  expmulnbnd  14156  discr1  14160  discr  14161  faclbnd  14211  faclbnd3  14213  faclbnd6  14220  bcval4  14228  bcval5  14239  bcpasc  14242  hasheq0  14284  hashneq0  14285  hashnn0n0nn  14312  hashgt12el  14343  hashgt12el2  14344  hashge2el2dif  14401  lsw0  14486  swrdccatin2  14650  pfxccatin12lem3  14653  reim0  15039  re0  15073  im0  15074  rei  15077  imi  15078  cj0  15079  sqeqd  15087  rennim  15160  cnpart  15161  sqrt0  15162  01sqrexlem4  15166  resqrex  15171  sqrtgt0  15179  sqrt00  15184  sqrtneglem  15187  sqrt9  15194  sqrt2gt1lt2  15195  leabs  15220  absor  15221  max0add  15231  eqsqrt2d  15290  sqrtpclii  15304  rlimconst  15465  rlimrege0  15500  lo1mul  15549  iserge0  15582  fsum00  15719  isumless  15766  arisum2  15782  georeclim  15793  geo2sum  15794  geoisumr  15799  0.999...  15802  cvgrat  15804  fprodge0  15914  bpoly4  15980  cos0  16073  ef01bndlem  16107  sin01bnd  16108  cos01bnd  16109  cos2bnd  16111  sin01gt0  16113  cos01gt0  16114  sincos2sgn  16117  sin4lt0  16118  absef  16120  absefib  16121  efieq1re  16122  epos  16130  rpnnen2lem2  16138  rpnnen2lem3  16139  rpnnen2lem4  16140  rpnnen2lem9  16145  ruclem6  16158  dvdslelem  16234  divalglem1  16319  divalglem5  16322  divalglem6  16323  flodddiv4  16340  sadcadd  16383  gcdn0gt0  16443  nn0seqcvgd  16495  algcvgblem  16502  algcvga  16504  pythagtriplem12  16752  pythagtriplem13  16753  pythagtriplem14  16754  pythagtriplem16  16756  prmreclem4  16845  prmreclem5  16846  prmreclem6  16847  1arith  16853  ramz  16951  chnub  18543  mulgnegnn  19012  subgmulg  19068  srgbinomlem4  20162  isabvd  20743  abvtrivd  20763  rge0srg  21391  xrs1mnd  21393  xrs10  21394  psgnodpmr  21543  re0g  21565  psrbaglesupp  21876  psdmvr  22110  mnfnei  23163  imasdsf1olem  24315  ssblps  24364  ssbl  24365  xmeter  24375  dscmet  24514  dscopn  24515  nmoi  24670  nmoeq0  24678  0nghm  24683  idnghm  24685  cnbl0  24715  xrsxmet  24752  metdseq0  24797  iicmp  24833  iiconn  24834  iihalf1  24879  iihalf1cnOLD  24881  elii1  24885  icopnfcnv  24894  icopnfhmeo  24895  iccpnfcnv  24896  xrhmeo  24898  xrhmph  24899  htpycc  24933  reparphti  24950  reparphtiOLD  24951  pcoval1  24967  pco0  24968  pcoval2  24970  pcocn  24971  pcohtpylem  24973  pcopt  24976  pcopt2  24977  pcoass  24978  pcorevlem  24980  reust  25335  recusp  25336  rrx0el  25352  minveclem4c  25379  minveclem2  25380  minveclem3b  25382  minveclem4  25386  minveclem7  25389  pjthlem1  25391  cniccbdd  25416  ovolunnul  25455  ovoliunnul  25462  ovolicc1  25471  ovolre  25480  iccvolcl  25522  ovolioo  25523  ioovolcl  25525  ioorcl  25532  vitalilem4  25566  vitalilem5  25567  vitali  25568  ismbf  25583  mbfmulc2lem  25602  mbfpos  25606  mbfposr  25607  i1f0  25642  i1f1  25645  itg1addlem2  25652  itg1addlem4  25654  itg1addlem5  25655  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  mbfi1flimlem  25677  xrge0f  25686  itg2ge0  25690  itg2const  25695  itg2mulc  25702  itg2splitlem  25703  itg2gt0  25715  itg2cnlem1  25716  ibl0  25742  iblrelem  25746  iblposlem  25747  iblpos  25748  iblre  25749  itgreval  25752  itgneg  25759  iblss  25760  i1fibl  25763  itgitg1  25764  itgle  25765  itgeqa  25769  itgless  25772  iblconst  25773  itgconst  25774  ibladdlem  25775  itgaddlem2  25779  iblabslem  25783  iblabsr  25785  iblmulc2  25786  itgmulc2lem2  25788  itgabs  25790  itgsplit  25791  bddmulibl  25794  dvferm1  25943  dvferm2  25945  dvferm  25946  dvlip  25952  c1lip1  25956  dveq0  25959  dv11cn  25960  dvne0  25970  ftc1lem4  26000  ply1divex  26096  dgrco  26235  plyrecj  26241  vieta1lem2  26273  aalioulem2  26295  aalioulem3  26296  pserulm  26385  psercnlem2  26388  psercnlem1  26389  psercn  26390  abelth  26405  reeff1olem  26410  reeff1o  26411  pilem2  26416  pilem3  26417  pipos  26422  sinhalfpilem  26426  sincosq1sgn  26461  sincosq2sgn  26462  coseq00topi  26465  coseq0negpitopi  26466  tangtx  26468  tanabsge  26469  sinq12ge0  26471  sinq34lt0t  26472  cosq14ge0  26474  sincos4thpi  26476  sincos6thpi  26479  pige3ALT  26483  sineq0  26487  cosordlem  26493  cosord  26494  cos0pilt1  26495  cos11  26496  sinord  26497  recosf1o  26498  resinf1o  26499  tanord1  26500  tanord  26501  tanregt0  26502  efif1olem4  26508  efifo  26510  relogrn  26524  log1  26548  logi  26550  logneg  26551  argregt0  26573  argrege0  26574  argimgt0  26575  logneg2  26578  logdivlti  26583  logdivlt  26584  ellogdm  26602  logdmn0  26603  logdmnrp  26604  logcnlem3  26607  dvloglem  26611  logdmopn  26612  logf1o2  26613  dvlog2lem  26615  efopnlem1  26619  logtayl  26623  recxpcl  26638  cxpge0  26646  cxple2  26660  cxple2a  26662  cxpsqrtlem  26665  cxpcn3  26712  cxpaddlelem  26715  cxpaddle  26716  loglesqrt  26725  logbrec  26746  ang180lem3  26775  ang180lem4  26776  asinneg  26850  asin1  26858  reasinsin  26860  acosbnd  26864  atan0  26872  atanrecl  26875  atanlogaddlem  26877  atanlogsublem  26879  atanlogsub  26880  atantan  26887  atanbnd  26890  atan1  26892  atans2  26895  ressatans  26898  log2cnv  26908  log2tlbnd  26909  log2ub  26913  log2le1  26914  rlimcnp  26929  rlimcnp2  26930  o1cxp  26939  jensen  26953  amgm  26955  emgt0  26971  harmonicbnd3  26972  harmoniclbnd  26973  harmonicbnd4  26975  zetacvg  26979  eldmgm  26986  lgamgulmlem2  26994  basellem3  27047  basellem8  27052  efnnfsumcl  27067  ppisval  27068  vmage0  27085  chpge0  27090  efchtdvds  27123  ppiltx  27141  ppiub  27169  chpeq0  27173  chteq0  27174  chtleppi  27175  chpchtsum  27184  chpub  27185  dchr1re  27228  bcmono  27242  efexple  27246  bposlem1  27249  bposlem4  27252  bposlem5  27253  bposlem7  27255  bposlem8  27256  bposlem9  27257  lgsval2lem  27272  lgsval4a  27284  lgsneg  27286  lgsdilem  27289  lgsdir2lem1  27290  2lgsoddprmlem3a  27375  2lgsoddprmlem3b  27376  2lgsoddprmlem3c  27377  2lgsoddprmlem3d  27378  rplogsumlem2  27450  rpvmasumlem  27452  dchrisum0flblem1  27473  dchrisum0flblem2  27474  dchrisum0fno1  27476  rplogsum  27492  logdivsum  27498  mulog2sumlem2  27500  selberg2lem  27515  logdivbnd  27521  pntrsumo1  27530  pntrlog2bndlem4  27545  pntrlog2bndlem5  27546  pntpbnd1  27551  pntpbnd2  27552  pntlem3  27574  pntleml  27576  ostth2  27602  trgcgrg  28536  ttgcontlem1  28906  axlowdimlem1  28964  axlowdimlem6  28969  axlowdimlem7  28970  axlowdimlem10  28973  axlowdim1  28981  axlowdim2  28982  axlowdim  28983  elntg2  29007  umgrislfupgrlem  29144  lfgrnloop  29147  lfuhgr1v0e  29276  usgrexmplef  29281  pthdlem2  29790  crctcshwlkn0lem7  29838  rusgrnumwwlks  29999  clwwlkn0  30052  konigsberg  30281  ex-po  30459  ex-sqrt  30478  ex-gcd  30481  nvz0  30692  0blo  30816  nmlno0lem  30817  nmblolbii  30823  siilem2  30876  minvecolem2  30899  minvecolem3  30900  minvecolem4c  30903  minvecolem4  30904  minvecolem5  30905  minvecolem7  30907  htthlem  30941  hiidge0  31122  normlem6  31139  normgt0  31151  norm-i  31153  normpyc  31170  bcsiALT  31203  pjhthlem1  31415  pjneli  31747  nmlnop0iALT  32019  unopbd  32039  nmbdoplbi  32048  nmcoplbi  32052  nmbdfnlbi  32073  nmbdfnlb  32074  nmcfnlbi  32076  cnlnadjlem7  32097  nmopcoi  32119  branmfn  32129  leopmul  32158  nmopleid  32163  pjbdlni  32173  pjnormssi  32192  stle0i  32263  cdj3lem1  32458  xaddeq0  32782  expgt0b  32846  pr01ssre  32854  sgnclre  32862  sgnnbi  32868  sgnpbi  32869  indf  32883  indfval  32884  dp20u  32908  dp20h  32909  dp2clq  32911  dp2lt10  32914  dp2lt  32915  dp0u  32931  dplti  32935  dpexpp1  32938  xdiv0  32959  xrge0slmod  33378  evl1deg3  33608  fldext2chn  33834  cos9thpiminplylem1  33888  unitdivcld  34007  sqsscirc1  34014  xrge0iifcnv  34039  xrge0iifiso  34041  rezh  34075  esumcvgsum  34194  voliune  34335  volfiniune  34336  sibfinima  34445  sitmcl  34457  0rrv  34557  coinfliprv  34589  ballotlem2  34595  ballotlem4  34605  ballotlemi1  34609  ballotlemic  34613  plymulx0  34653  signsply0  34657  signswch  34667  signstf  34672  signstf0  34674  signstfveq0  34683  signlem0  34693  signshf  34694  itgexpif  34712  hgt750lemd  34754  hgt750lem  34757  hgt750lem2  34758  hgt750leme  34764  iisconn  35395  iillysconn  35396  cvmliftlem10  35437  fz0n  35874  bcneg1  35879  nn0prpwlem  36465  dnizeq0  36618  dnizphlfeqhlf  36619  knoppndvlem13  36667  cnndvlem1  36680  bj-pinftyccb  37365  bj-minftyccb  37369  bj-pinftynminfty  37371  taupilemrplb  37464  irrdiff  37470  sin2h  37750  tan2h  37752  ptrecube  37760  poimirlem16  37776  poimirlem17  37777  poimirlem20  37780  poimirlem22  37782  poimirlem23  37783  poimirlem29  37789  poimirlem31  37791  poimir  37793  heicant  37795  mblfinlem2  37798  ismblfin  37801  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  mbfposadd  37807  itg2addnclem  37811  itg2addnclem2  37812  ibladdnclem  37816  itgaddnclem2  37819  iblabsnclem  37823  iblmulc2nc  37825  itgmulc2nclem2  37827  itgabsnc  37829  ftc1cnnclem  37831  ftc1anclem5  37837  ftc1anclem8  37840  asindmre  37843  dvasin  37844  areacirclem4  37851  areacirc  37853  isbnd3  37924  ssbnd  37928  prdsbnd  37933  bfplem2  37963  bfp  37964  renegclALT  39162  0cnALT3  42450  sn-1ne2  42462  itrere  42515  oexpreposd  42519  tan3rdpi  42549  asin1half  42554  readvrec2  42558  sn-00idlem2  42596  sn-00idlem3  42597  sn-00id  42598  sn-0tie0  42648  sn-ltaddpos  42650  sn-ltaddneg  42651  relt0neg1  42653  sn-nnne0  42657  reelznn0nn  42658  sn-0lt1  42672  sn-inelr  42684  sn-itrere  42685  sn-retire  42686  pellexlem6  43018  elpell14qr2  43046  oddcomabszz  43128  zindbi  43130  jm2.24  43147  acongeq  43167  arearect  43399  areaquad  43400  reabsifneg  43815  reabsifnpos  43816  reabsifpos  43817  reabsifnneg  43818  imsqrtvalex  43829  relexp01min  43896  imo72b2lem2  44350  imo72b2lem1  44352  imo72b2  44355  dvconstbi  44517  binomcxplemnn0  44532  binomcxplemdvbinom  44536  binomcxplemcvg  44537  binomcxplemnotnn0  44539  sineq0ALT  45119  halffl  45486  ren0  45588  rexanuz2nf  45678  sqrlearg  45741  limsup10ex  45959  dvnmptdivc  46124  dvnmul  46129  itgsin0pilem1  46136  itgsinexplem1  46140  itgsinexp  46141  iblempty  46151  stoweidlem17  46203  stoweidlem36  46222  stoweidlem55  46241  wallispilem1  46251  wallispilem2  46252  wallispilem4  46254  stirlinglem4  46263  stirlinglem13  46272  stirlinglem14  46273  stirlinglem15  46274  stirlingr  46276  dirker2re  46278  dirkerdenne0  46279  dirkerre  46281  dirkertrigeqlem1  46284  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem11  46304  fourierdlem16  46309  fourierdlem21  46314  fourierdlem22  46315  fourierdlem41  46334  fourierdlem42  46335  fourierdlem48  46340  fourierdlem62  46354  fourierdlem66  46358  fourierdlem79  46371  fourierdlem83  46375  fourierdlem94  46386  fourierdlem102  46394  fourierdlem103  46395  fourierdlem104  46396  fourierdlem111  46403  fourierdlem112  46404  fourierdlem113  46405  fourierdlem114  46406  sqwvfoura  46414  sqwvfourb  46415  fourierswlem  46416  fouriersw  46417  etransclem23  46443  etransclem44  46464  etransclem46  46466  salexct3  46528  salgensscntex  46530  sge0rnn0  46554  sge00  46562  0ome  46715  ovn0lem  46751  ovnhoilem1  46787  smfmullem1  46977  smfmullem2  46978  smfmullem3  46979  smfmullem4  46980  squeezedltsq  47074  zm1nn  47490  sqrtnegnre  47495  m1mod0mod1  47542  fmtnoprmfac2lem1  47754  31prm  47785  mod42tp1mod8  47790  nfermltl2rev  47931  tgblthelfgott  48003  usgrexmpl1lem  48209  usgrexmpl2lem  48214  usgrexmpl2nb0  48219  usgrexmpl2nb5  48224  usgrexmpl2trifr  48225  gpgusgralem  48244  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  gpg5edgnedg  48318  altgsumbcALT  48541  expnegico01  48706  dignnld  48791  eenglngeehlnmlem1  48925  line2ylem  48939  line2y  48943  itsclc0yqsollem2  48951  icccldii  49106  i0oii  49107  sepfsepc  49115  ex-gt  49915