Theorem 0re 11263

Description: The number 0 is real. Remark: the first step could also be ax-icn 11214. See also 0reALT 11606. (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 11213	. 2 ⊢ 1 ∈ ℂ
2		cnre 11258	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11226	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11238	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2829	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3155	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3147	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∃wrex 3070  (class class class)co 7431  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156  ici 11157   + caddc 11158   · cmul 11160

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addrcl 11216  ax-rnegex 11226  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-rex 3071

This theorem is referenced by:  0red  11264  0xr  11308  axmulgt0  11335  ne0gt0  11366  00id  11436  mul02lem1  11437  mul02lem2  11438  mul02  11439  addrid  11441  ltaddneg  11477  addgt0  11749  addgegt0  11750  addgtge0  11751  addge0  11752  ltaddpos  11753  ltneg  11763  leneg  11766  lt0neg1  11769  lt0neg2  11770  le0neg1  11771  le0neg2  11772  addge01  11773  suble0  11777  mulge0  11781  msqge0  11784  0le1  11786  relin01  11787  gt0ne0i  11798  gt0ne0d  11827  lt0ne0d  11828  elimge0  12106  ltm1  12109  recgt0  12113  prodgt0  12114  lemul1a  12121  ltmul12a  12123  lemul12a  12125  mulgt1OLD  12126  gt0div  12134  ge0div  12135  mulge0b  12138  lediv12a  12161  recgt1i  12165  recreclt  12167  ledivp1  12170  squeeze0  12171  recgt0ii  12174  ledivp1i  12193  ltdivp1i  12194  fimaxre2  12213  inelr  12256  crne0  12259  nnge1  12294  nngt0  12297  nnnle0  12299  nnne0  12300  nnrecgt0  12309  0le0  12367  neg1lt0  12383  halfge0  12483  nn0ssre  12530  nn0ge0  12551  nn0nlt0  12552  nn0le0eq0  12554  0mnnnnn0  12558  elnnnn0b  12570  elnnnn0c  12571  nn0sub  12576  elnnz  12623  0z  12624  elnn0z  12626  elnnz1  12643  recnz  12693  gtndiv  12695  fnn0ind  12717  10re  12752  rpge0  13048  rpneg  13067  0nrp  13070  0ltpnf  13164  mnflt0  13167  qsqueeze  13243  xneg0  13254  xaddrid  13283  xnn0xadd0  13289  xmulpnf1  13316  xlemul1a  13330  xadddi  13337  xrsupsslem  13349  xrinfmsslem  13350  elrege0  13494  0e0icopnf  13498  elicc01  13506  0elunit  13509  unitssre  13539  0nelfz1  13583  fzpreddisj  13613  fz0to4untppr  13670  fz0to5un2tp  13671  nn0p1elfzo  13742  ico01fl0  13859  rpsup  13906  modelico  13921  0mod  13942  1mod  13943  le2sq2  14175  expubnd  14217  sqlecan  14248  bernneq2  14269  expnbnd  14271  expnlbnd  14272  expmulnbnd  14274  discr1  14278  discr  14279  faclbnd  14329  faclbnd3  14331  faclbnd6  14338  bcval4  14346  bcval5  14357  bcpasc  14360  hasheq0  14402  hashneq0  14403  hashnn0n0nn  14430  hashgt12el  14461  hashgt12el2  14462  hashge2el2dif  14519  lsw0  14603  swrdccatin2  14767  pfxccatin12lem3  14770  reim0  15157  re0  15191  im0  15192  rei  15195  imi  15196  cj0  15197  sqeqd  15205  rennim  15278  cnpart  15279  sqrt0  15280  01sqrexlem4  15284  resqrex  15289  sqrtgt0  15297  sqrt00  15302  sqrtneglem  15305  sqrt9  15312  sqrt2gt1lt2  15313  leabs  15338  absor  15339  max0add  15349  eqsqrt2d  15407  sqrtpclii  15421  rlimconst  15580  rlimrege0  15615  lo1mul  15664  iserge0  15697  fsum00  15834  isumless  15881  arisum2  15897  georeclim  15908  geo2sum  15909  geoisumr  15914  0.999...  15917  cvgrat  15919  fprodge0  16029  bpoly4  16095  cos0  16186  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  cos2bnd  16224  sin01gt0  16226  cos01gt0  16227  sincos2sgn  16230  sin4lt0  16231  absef  16233  absefib  16234  efieq1re  16235  epos  16243  rpnnen2lem2  16251  rpnnen2lem3  16252  rpnnen2lem4  16253  rpnnen2lem9  16258  ruclem6  16271  dvdslelem  16346  divalglem1  16431  divalglem5  16434  divalglem6  16435  flodddiv4  16452  sadcadd  16495  gcdn0gt0  16555  nn0seqcvgd  16607  algcvgblem  16614  algcvga  16616  pythagtriplem12  16864  pythagtriplem13  16865  pythagtriplem14  16866  pythagtriplem16  16868  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  1arith  16965  ramz  17063  mulgnegnn  19102  subgmulg  19158  srgbinomlem4  20226  isabvd  20813  abvtrivd  20833  xrs1mnd  21422  xrs10  21423  rge0srg  21456  psgnodpmr  21608  re0g  21630  psrbaglesupp  21942  psdmvr  22173  mnfnei  23229  imasdsf1olem  24383  ssblps  24432  ssbl  24433  xmeter  24443  dscmet  24585  dscopn  24586  nmoi  24749  nmoeq0  24757  0nghm  24762  idnghm  24764  cnbl0  24794  xrsxmet  24831  metdseq0  24876  iicmp  24912  iiconn  24913  iihalf1  24958  iihalf1cnOLD  24960  elii1  24964  icopnfcnv  24973  icopnfhmeo  24974  iccpnfcnv  24975  xrhmeo  24977  xrhmph  24978  htpycc  25012  reparphti  25029  reparphtiOLD  25030  pcoval1  25046  pco0  25047  pcoval2  25049  pcocn  25050  pcohtpylem  25052  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  reust  25415  recusp  25416  rrx0el  25432  minveclem4c  25459  minveclem2  25460  minveclem3b  25462  minveclem4  25466  minveclem7  25469  pjthlem1  25471  cniccbdd  25496  ovolunnul  25535  ovoliunnul  25542  ovolicc1  25551  ovolre  25560  iccvolcl  25602  ovolioo  25603  ioovolcl  25605  ioorcl  25612  vitalilem4  25646  vitalilem5  25647  vitali  25648  ismbf  25663  mbfmulc2lem  25682  mbfpos  25686  mbfposr  25687  i1f0  25722  i1f1  25725  itg1addlem2  25732  itg1addlem4  25734  itg1addlem5  25735  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1flimlem  25757  xrge0f  25766  itg2ge0  25770  itg2const  25775  itg2mulc  25782  itg2splitlem  25783  itg2gt0  25795  itg2cnlem1  25796  ibl0  25822  iblrelem  25826  iblposlem  25827  iblpos  25828  iblre  25829  itgreval  25832  itgneg  25839  iblss  25840  i1fibl  25843  itgitg1  25844  itgle  25845  itgeqa  25849  itgless  25852  iblconst  25853  itgconst  25854  ibladdlem  25855  itgaddlem2  25859  iblabslem  25863  iblabsr  25865  iblmulc2  25866  itgmulc2lem2  25868  itgabs  25870  itgsplit  25871  bddmulibl  25874  dvferm1  26023  dvferm2  26025  dvferm  26026  dvlip  26032  c1lip1  26036  dveq0  26039  dv11cn  26040  dvne0  26050  ftc1lem4  26080  ply1divex  26176  dgrco  26315  plyrecj  26321  vieta1lem2  26353  aalioulem2  26375  aalioulem3  26376  pserulm  26465  psercnlem2  26468  psercnlem1  26469  psercn  26470  abelth  26485  reeff1olem  26490  reeff1o  26491  pilem2  26496  pilem3  26497  pipos  26502  sinhalfpilem  26505  sincosq1sgn  26540  sincosq2sgn  26541  coseq00topi  26544  coseq0negpitopi  26545  tangtx  26547  tanabsge  26548  sinq12ge0  26550  sinq34lt0t  26551  cosq14ge0  26553  sincos4thpi  26555  sincos6thpi  26558  pige3ALT  26562  sineq0  26566  cosordlem  26572  cosord  26573  cos0pilt1  26574  cos11  26575  sinord  26576  recosf1o  26577  resinf1o  26578  tanord1  26579  tanord  26580  tanregt0  26581  efif1olem4  26587  efifo  26589  relogrn  26603  log1  26627  logi  26629  logneg  26630  argregt0  26652  argrege0  26653  argimgt0  26654  logneg2  26657  logdivlti  26662  logdivlt  26663  ellogdm  26681  logdmn0  26682  logdmnrp  26683  logcnlem3  26686  dvloglem  26690  logdmopn  26691  logf1o2  26692  dvlog2lem  26694  efopnlem1  26698  logtayl  26702  recxpcl  26717  cxpge0  26725  cxple2  26739  cxple2a  26741  cxpsqrtlem  26744  cxpcn3  26791  cxpaddlelem  26794  cxpaddle  26795  loglesqrt  26804  logbrec  26825  ang180lem3  26854  ang180lem4  26855  asinneg  26929  asin1  26937  reasinsin  26939  acosbnd  26943  atan0  26951  atanrecl  26954  atanlogaddlem  26956  atanlogsublem  26958  atanlogsub  26959  atantan  26966  atanbnd  26969  atan1  26971  atans2  26974  ressatans  26977  log2cnv  26987  log2tlbnd  26988  log2ub  26992  log2le1  26993  rlimcnp  27008  rlimcnp2  27009  o1cxp  27018  jensen  27032  amgm  27034  emgt0  27050  harmonicbnd3  27051  harmoniclbnd  27052  harmonicbnd4  27054  zetacvg  27058  eldmgm  27065  lgamgulmlem2  27073  basellem3  27126  basellem8  27131  efnnfsumcl  27146  ppisval  27147  vmage0  27164  chpge0  27169  efchtdvds  27202  ppiltx  27220  ppiub  27248  chpeq0  27252  chteq0  27253  chtleppi  27254  chpchtsum  27263  chpub  27264  dchr1re  27307  bcmono  27321  efexple  27325  bposlem1  27328  bposlem4  27331  bposlem5  27332  bposlem7  27334  bposlem8  27335  bposlem9  27336  lgsval2lem  27351  lgsval4a  27363  lgsneg  27365  lgsdilem  27368  lgsdir2lem1  27369  2lgsoddprmlem3a  27454  2lgsoddprmlem3b  27455  2lgsoddprmlem3c  27456  2lgsoddprmlem3d  27457  rplogsumlem2  27529  rpvmasumlem  27531  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0fno1  27555  rplogsum  27571  logdivsum  27577  mulog2sumlem2  27579  selberg2lem  27594  logdivbnd  27600  pntrsumo1  27609  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntpbnd1  27630  pntpbnd2  27631  pntlem3  27653  pntleml  27655  ostth2  27681  trgcgrg  28523  ttgcontlem1  28899  axlowdimlem1  28957  axlowdimlem6  28962  axlowdimlem7  28963  axlowdimlem10  28966  axlowdim1  28974  axlowdim2  28975  axlowdim  28976  elntg2  29000  umgrislfupgrlem  29139  lfgrnloop  29142  lfuhgr1v0e  29271  usgrexmplef  29276  pthdlem2  29788  crctcshwlkn0lem7  29836  rusgrnumwwlks  29994  clwwlkn0  30047  konigsberg  30276  ex-po  30454  ex-sqrt  30473  ex-gcd  30476  nvz0  30687  0blo  30811  nmlno0lem  30812  nmblolbii  30818  siilem2  30871  minvecolem2  30894  minvecolem3  30895  minvecolem4c  30898  minvecolem4  30899  minvecolem5  30900  minvecolem7  30902  htthlem  30936  hiidge0  31117  normlem6  31134  normgt0  31146  norm-i  31148  normpyc  31165  bcsiALT  31198  pjhthlem1  31410  pjneli  31742  nmlnop0iALT  32014  unopbd  32034  nmbdoplbi  32043  nmcoplbi  32047  nmbdfnlbi  32068  nmbdfnlb  32069  nmcfnlbi  32071  cnlnadjlem7  32092  nmopcoi  32114  branmfn  32124  leopmul  32153  nmopleid  32158  pjbdlni  32168  pjnormssi  32187  stle0i  32258  cdj3lem1  32453  xaddeq0  32757  expgt0b  32818  pr01ssre  32826  indf  32840  indfval  32841  dp20u  32860  dp20h  32861  dp2clq  32863  dp2lt10  32866  dp2lt  32867  dp0u  32883  dplti  32887  dpexpp1  32890  xdiv0  32911  chnub  33002  xrge0slmod  33376  evl1deg3  33603  fldext2chn  33769  unitdivcld  33900  sqsscirc1  33907  xrge0iifcnv  33932  xrge0iifiso  33934  rezh  33970  esumcvgsum  34089  voliune  34230  volfiniune  34231  sibfinima  34341  sitmcl  34353  0rrv  34453  coinfliprv  34485  ballotlem2  34491  ballotlem4  34501  ballotlemi1  34505  ballotlemic  34509  sgnclre  34542  sgnnbi  34548  sgnpbi  34549  plymulx0  34562  signsply0  34566  signswch  34576  signstf  34581  signstf0  34583  signstfveq0  34592  signlem0  34602  signshf  34603  itgexpif  34621  hgt750lemd  34663  hgt750lem  34666  hgt750lem2  34667  hgt750leme  34673  iisconn  35257  iillysconn  35258  cvmliftlem10  35299  fz0n  35731  bcneg1  35736  nn0prpwlem  36323  dnizeq0  36476  dnizphlfeqhlf  36477  knoppndvlem13  36525  cnndvlem1  36538  bj-pinftyccb  37222  bj-minftyccb  37226  bj-pinftynminfty  37228  taupilemrplb  37321  irrdiff  37327  sin2h  37617  tan2h  37619  ptrecube  37627  poimirlem16  37643  poimirlem17  37644  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem29  37656  poimirlem31  37658  poimir  37660  heicant  37662  mblfinlem2  37665  ismblfin  37668  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  mbfposadd  37674  itg2addnclem  37678  itg2addnclem2  37679  ibladdnclem  37683  itgaddnclem2  37686  iblabsnclem  37690  iblmulc2nc  37692  itgmulc2nclem2  37694  itgabsnc  37696  ftc1cnnclem  37698  ftc1anclem5  37704  ftc1anclem8  37707  asindmre  37710  dvasin  37711  areacirclem4  37718  areacirc  37720  isbnd3  37791  ssbnd  37795  prdsbnd  37800  bfplem2  37830  bfp  37831  renegclALT  38964  2xp3dxp2ge1d  42242  factwoffsmonot  42243  0cnALT3  42294  sn-1ne2  42300  itrere  42353  oexpreposd  42357  tan3rdpi  42386  asin1half  42387  readvrec2  42391  sn-00idlem2  42429  sn-00idlem3  42430  sn-00id  42431  sn-0tie0  42469  sn-ltaddpos  42471  sn-ltaddneg  42472  relt0neg1  42474  sn-nnne0  42478  reelznn0nn  42479  sn-0lt1  42493  sn-inelr  42497  sn-itrere  42498  sn-retire  42499  pellexlem6  42845  elpell14qr2  42873  oddcomabszz  42956  zindbi  42958  jm2.24  42975  acongeq  42995  arearect  43227  areaquad  43228  reabsifneg  43645  reabsifnpos  43646  reabsifpos  43647  reabsifnneg  43648  imsqrtvalex  43659  relexp01min  43726  imo72b2lem2  44180  imo72b2lem1  44182  imo72b2  44185  dvconstbi  44353  binomcxplemnn0  44368  binomcxplemdvbinom  44372  binomcxplemcvg  44373  binomcxplemnotnn0  44375  sineq0ALT  44957  halffl  45308  ren0  45413  rexanuz2nf  45503  sqrlearg  45566  limsup10ex  45788  dvnmptdivc  45953  dvnmul  45958  itgsin0pilem1  45965  itgsinexplem1  45969  itgsinexp  45970  iblempty  45980  stoweidlem17  46032  stoweidlem36  46051  stoweidlem55  46070  wallispilem1  46080  wallispilem2  46081  wallispilem4  46083  stirlinglem4  46092  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  stirlingr  46105  dirker2re  46107  dirkerdenne0  46108  dirkerre  46110  dirkertrigeqlem1  46113  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem11  46133  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem62  46183  fourierdlem66  46187  fourierdlem79  46200  fourierdlem83  46204  fourierdlem94  46215  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fourierdlem113  46234  fourierdlem114  46235  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  etransclem23  46272  etransclem44  46293  etransclem46  46295  salexct3  46357  salgensscntex  46359  sge0rnn0  46383  sge00  46391  0ome  46544  ovn0lem  46580  ovnhoilem1  46616  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808  smfmullem4  46809  zm1nn  47314  sqrtnegnre  47319  m1mod0mod1  47356  fmtnoprmfac2lem1  47553  31prm  47584  mod42tp1mod8  47589  nfermltl2rev  47730  tgblthelfgott  47802  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996  gpgusgralem  48011  altgsumbcALT  48269  expnegico01  48435  dignnld  48524  eenglngeehlnmlem1  48658  line2ylem  48672  line2y  48676  itsclc0yqsollem2  48684  icccldii  48816  i0oii  48817  sepfsepc  48825  ex-gt  49247