Theorem 0re 11146

Description: The number 0 is real. Remark: the first step could also be ax-icn 11097. See also 0reALT 11490. (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 11096	. 2 ⊢ 1 ∈ ℂ
2		cnre 11141	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11109	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11121	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2825	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3139	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3131	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  (class class class)co 7368  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039  ici 11040   + caddc 11041   · cmul 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-rex 3063

This theorem is referenced by:  0red  11147  0xr  11191  axmulgt0  11219  ne0gt0  11250  00id  11320  mul02lem1  11321  mul02lem2  11322  mul02  11323  addrid  11325  ltaddneg  11361  addgt0  11635  addgegt0  11636  addgtge0  11637  addge0  11638  ltaddpos  11639  ltneg  11649  leneg  11652  lt0neg1  11655  lt0neg2  11656  le0neg1  11657  le0neg2  11658  addge01  11659  suble0  11663  mulge0  11667  msqge0  11670  0le1  11672  relin01  11673  gt0ne0i  11684  lt0ne0d  11714  elimge0  11992  ltm1  11995  recgt0  11999  prodgt0  12000  lemul1a  12007  ltmul12a  12009  lemul12a  12011  mulgt1OLD  12012  gt0div  12020  ge0div  12021  mulge0b  12024  lediv12a  12047  recgt1i  12051  recreclt  12053  ledivp1  12056  squeeze0  12057  recgt0ii  12060  ledivp1i  12079  ltdivp1i  12080  fimaxre2  12099  inelr  12147  crne0  12150  nnge1  12185  nngt0  12188  nnnle0  12190  nnne0  12191  nnrecgt0  12200  0le0  12258  halfge0  12369  nn0ssre  12417  nn0ge0  12438  nn0nlt0  12439  nn0le0eq0  12441  0mnnnnn0  12445  elnnnn0b  12457  elnnnn0c  12458  nn0sub  12463  elnnz  12510  0z  12511  elnn0z  12513  elnnz1  12529  recnz  12579  gtndiv  12581  fnn0ind  12603  10re  12638  rpge0  12931  rpneg  12951  0nrp  12954  0ltpnf  13048  mnflt0  13051  qsqueeze  13128  xneg0  13139  xaddrid  13168  xnn0xadd0  13174  xmulpnf1  13201  xlemul1a  13215  xadddi  13222  xrsupsslem  13234  xrinfmsslem  13235  elrege0  13382  0e0icopnf  13386  elicc01  13394  0elunit  13397  unitssre  13427  0nelfz1  13471  fzpreddisj  13501  fz0to4untppr  13558  fz0to5un2tp  13559  nn0p1elfzo  13630  ico01fl0  13751  rpsup  13798  modelico  13813  0mod  13834  1mod  13835  le2sq2  14070  expubnd  14113  sqlecan  14144  bernneq2  14165  expnbnd  14167  expnlbnd  14168  expmulnbnd  14170  discr1  14174  discr  14175  faclbnd  14225  faclbnd3  14227  faclbnd6  14234  bcval4  14242  bcval5  14253  bcpasc  14256  hasheq0  14298  hashneq0  14299  hashnn0n0nn  14326  hashgt12el  14357  hashgt12el2  14358  hashge2el2dif  14415  lsw0  14500  swrdccatin2  14664  pfxccatin12lem3  14667  reim0  15053  re0  15087  im0  15088  rei  15091  imi  15092  cj0  15093  sqeqd  15101  rennim  15174  cnpart  15175  sqrt0  15176  01sqrexlem4  15180  resqrex  15185  sqrtgt0  15193  sqrt00  15198  sqrtneglem  15201  sqrt9  15208  sqrt2gt1lt2  15209  leabs  15234  absor  15235  max0add  15245  eqsqrt2d  15304  sqrtpclii  15318  rlimconst  15479  rlimrege0  15514  lo1mul  15563  iserge0  15596  fsum00  15733  isumless  15780  arisum2  15796  georeclim  15807  geo2sum  15808  geoisumr  15813  0.999...  15816  cvgrat  15818  fprodge0  15928  bpoly4  15994  cos0  16087  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  cos2bnd  16125  sin01gt0  16127  cos01gt0  16128  sincos2sgn  16131  sin4lt0  16132  absef  16134  absefib  16135  efieq1re  16136  epos  16144  rpnnen2lem2  16152  rpnnen2lem3  16153  rpnnen2lem4  16154  rpnnen2lem9  16159  ruclem6  16172  dvdslelem  16248  divalglem1  16333  divalglem5  16336  divalglem6  16337  flodddiv4  16354  sadcadd  16397  gcdn0gt0  16457  nn0seqcvgd  16509  algcvgblem  16516  algcvga  16518  pythagtriplem12  16766  pythagtriplem13  16767  pythagtriplem14  16768  pythagtriplem16  16770  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  1arith  16867  ramz  16965  chnub  18557  mulgnegnn  19026  subgmulg  19082  srgbinomlem4  20176  isabvd  20757  abvtrivd  20777  rge0srg  21405  xrs1mnd  21407  xrs10  21408  psgnodpmr  21557  re0g  21579  psrbaglesupp  21890  psdmvr  22124  mnfnei  23177  imasdsf1olem  24329  ssblps  24378  ssbl  24379  xmeter  24389  dscmet  24528  dscopn  24529  nmoi  24684  nmoeq0  24692  0nghm  24697  idnghm  24699  cnbl0  24729  xrsxmet  24766  metdseq0  24811  iicmp  24847  iiconn  24848  iihalf1  24893  iihalf1cnOLD  24895  elii1  24899  icopnfcnv  24908  icopnfhmeo  24909  iccpnfcnv  24910  xrhmeo  24912  xrhmph  24913  htpycc  24947  reparphti  24964  reparphtiOLD  24965  pcoval1  24981  pco0  24982  pcoval2  24984  pcocn  24985  pcohtpylem  24987  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevlem  24994  reust  25349  recusp  25350  rrx0el  25366  minveclem4c  25393  minveclem2  25394  minveclem3b  25396  minveclem4  25400  minveclem7  25403  pjthlem1  25405  cniccbdd  25430  ovolunnul  25469  ovoliunnul  25476  ovolicc1  25485  ovolre  25494  iccvolcl  25536  ovolioo  25537  ioovolcl  25539  ioorcl  25546  vitalilem4  25580  vitalilem5  25581  vitali  25582  ismbf  25597  mbfmulc2lem  25616  mbfpos  25620  mbfposr  25621  i1f0  25656  i1f1  25659  itg1addlem2  25666  itg1addlem4  25668  itg1addlem5  25669  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1flimlem  25691  xrge0f  25700  itg2ge0  25704  itg2const  25709  itg2mulc  25716  itg2splitlem  25717  itg2gt0  25729  itg2cnlem1  25730  ibl0  25756  iblrelem  25760  iblposlem  25761  iblpos  25762  iblre  25763  itgreval  25766  itgneg  25773  iblss  25774  i1fibl  25777  itgitg1  25778  itgle  25779  itgeqa  25783  itgless  25786  iblconst  25787  itgconst  25788  ibladdlem  25789  itgaddlem2  25793  iblabslem  25797  iblabsr  25799  iblmulc2  25800  itgmulc2lem2  25802  itgabs  25804  itgsplit  25805  bddmulibl  25808  dvferm1  25957  dvferm2  25959  dvferm  25960  dvlip  25966  c1lip1  25970  dveq0  25973  dv11cn  25974  dvne0  25984  ftc1lem4  26014  ply1divex  26110  dgrco  26249  plyrecj  26255  vieta1lem2  26287  aalioulem2  26309  aalioulem3  26310  pserulm  26399  psercnlem2  26402  psercnlem1  26403  psercn  26404  abelth  26419  reeff1olem  26424  reeff1o  26425  pilem2  26430  pilem3  26431  pipos  26436  sinhalfpilem  26440  sincosq1sgn  26475  sincosq2sgn  26476  coseq00topi  26479  coseq0negpitopi  26480  tangtx  26482  tanabsge  26483  sinq12ge0  26485  sinq34lt0t  26486  cosq14ge0  26488  sincos4thpi  26490  sincos6thpi  26493  pige3ALT  26497  sineq0  26501  cosordlem  26507  cosord  26508  cos0pilt1  26509  cos11  26510  sinord  26511  recosf1o  26512  resinf1o  26513  tanord1  26514  tanord  26515  tanregt0  26516  efif1olem4  26522  efifo  26524  relogrn  26538  log1  26562  logi  26564  logneg  26565  argregt0  26587  argrege0  26588  argimgt0  26589  logneg2  26592  logdivlti  26597  logdivlt  26598  ellogdm  26616  logdmn0  26617  logdmnrp  26618  logcnlem3  26621  dvloglem  26625  logdmopn  26626  logf1o2  26627  dvlog2lem  26629  efopnlem1  26633  logtayl  26637  recxpcl  26652  cxpge0  26660  cxple2  26674  cxple2a  26676  cxpsqrtlem  26679  cxpcn3  26726  cxpaddlelem  26729  cxpaddle  26730  loglesqrt  26739  logbrec  26760  ang180lem3  26789  ang180lem4  26790  asinneg  26864  asin1  26872  reasinsin  26874  acosbnd  26878  atan0  26886  atanrecl  26889  atanlogaddlem  26891  atanlogsublem  26893  atanlogsub  26894  atantan  26901  atanbnd  26904  atan1  26906  atans2  26909  ressatans  26912  log2cnv  26922  log2tlbnd  26923  log2ub  26927  log2le1  26928  rlimcnp  26943  rlimcnp2  26944  o1cxp  26953  jensen  26967  amgm  26969  emgt0  26985  harmonicbnd3  26986  harmoniclbnd  26987  harmonicbnd4  26989  zetacvg  26993  eldmgm  27000  lgamgulmlem2  27008  basellem3  27061  basellem8  27066  efnnfsumcl  27081  ppisval  27082  vmage0  27099  chpge0  27104  efchtdvds  27137  ppiltx  27155  ppiub  27183  chpeq0  27187  chteq0  27188  chtleppi  27189  chpchtsum  27198  chpub  27199  dchr1re  27242  bcmono  27256  efexple  27260  bposlem1  27263  bposlem4  27266  bposlem5  27267  bposlem7  27269  bposlem8  27270  bposlem9  27271  lgsval2lem  27286  lgsval4a  27298  lgsneg  27300  lgsdilem  27303  lgsdir2lem1  27304  2lgsoddprmlem3a  27389  2lgsoddprmlem3b  27390  2lgsoddprmlem3c  27391  2lgsoddprmlem3d  27392  rplogsumlem2  27464  rpvmasumlem  27466  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0fno1  27490  rplogsum  27506  logdivsum  27512  mulog2sumlem2  27514  selberg2lem  27529  logdivbnd  27535  pntrsumo1  27544  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntpbnd1  27565  pntpbnd2  27566  pntlem3  27588  pntleml  27590  ostth2  27616  trgcgrg  28599  ttgcontlem1  28969  axlowdimlem1  29027  axlowdimlem6  29032  axlowdimlem7  29033  axlowdimlem10  29036  axlowdim1  29044  axlowdim2  29045  axlowdim  29046  elntg2  29070  umgrislfupgrlem  29207  lfgrnloop  29210  lfuhgr1v0e  29339  usgrexmplef  29344  pthdlem2  29853  crctcshwlkn0lem7  29901  rusgrnumwwlks  30062  clwwlkn0  30115  konigsberg  30344  ex-po  30522  ex-sqrt  30541  ex-gcd  30544  nvz0  30756  0blo  30880  nmlno0lem  30881  nmblolbii  30887  siilem2  30940  minvecolem2  30963  minvecolem3  30964  minvecolem4c  30967  minvecolem4  30968  minvecolem5  30969  minvecolem7  30971  htthlem  31005  hiidge0  31186  normlem6  31203  normgt0  31215  norm-i  31217  normpyc  31234  bcsiALT  31267  pjhthlem1  31479  pjneli  31811  nmlnop0iALT  32083  unopbd  32103  nmbdoplbi  32112  nmcoplbi  32116  nmbdfnlbi  32137  nmbdfnlb  32138  nmcfnlbi  32140  cnlnadjlem7  32161  nmopcoi  32183  branmfn  32193  leopmul  32222  nmopleid  32227  pjbdlni  32237  pjnormssi  32256  stle0i  32327  cdj3lem1  32522  xaddeq0  32844  expgt0b  32908  pr01ssre  32916  sgnclre  32924  sgnnbi  32930  sgnpbi  32931  indf  32945  indfval  32946  dp20u  32970  dp20h  32971  dp2clq  32973  dp2lt10  32976  dp2lt  32977  dp0u  32993  dplti  32997  dpexpp1  33000  xdiv0  33021  xrge0slmod  33441  evl1deg3  33671  fldext2chn  33906  cos9thpiminplylem1  33960  unitdivcld  34079  sqsscirc1  34086  xrge0iifcnv  34111  xrge0iifiso  34113  rezh  34147  esumcvgsum  34266  voliune  34407  volfiniune  34408  sibfinima  34517  sitmcl  34529  0rrv  34629  coinfliprv  34661  ballotlem2  34667  ballotlem4  34677  ballotlemi1  34681  ballotlemic  34685  plymulx0  34725  signsply0  34729  signswch  34739  signstf  34744  signstf0  34746  signstfveq0  34755  signlem0  34765  signshf  34766  itgexpif  34784  hgt750lemd  34826  hgt750lem  34829  hgt750lem2  34830  hgt750leme  34836  iisconn  35468  iillysconn  35469  cvmliftlem10  35510  fz0n  35947  bcneg1  35952  nn0prpwlem  36538  dnizeq0  36697  dnizphlfeqhlf  36698  knoppndvlem13  36746  cnndvlem1  36759  bj-pinftyccb  37476  bj-minftyccb  37480  bj-pinftynminfty  37482  taupilemrplb  37575  irrdiff  37581  sin2h  37861  tan2h  37863  ptrecube  37871  poimirlem16  37887  poimirlem17  37888  poimirlem20  37891  poimirlem22  37893  poimirlem23  37894  poimirlem29  37900  poimirlem31  37902  poimir  37904  heicant  37906  mblfinlem2  37909  ismblfin  37912  ovoliunnfl  37913  voliunnfl  37915  volsupnfl  37916  mbfposadd  37918  itg2addnclem  37922  itg2addnclem2  37923  ibladdnclem  37927  itgaddnclem2  37930  iblabsnclem  37934  iblmulc2nc  37936  itgmulc2nclem2  37938  itgabsnc  37940  ftc1cnnclem  37942  ftc1anclem5  37948  ftc1anclem8  37951  asindmre  37954  dvasin  37955  areacirclem4  37962  areacirc  37964  isbnd3  38035  ssbnd  38039  prdsbnd  38044  bfplem2  38074  bfp  38075  renegclALT  39339  0cnALT3  42623  sn-1ne2  42635  itrere  42688  oexpreposd  42692  tan3rdpi  42722  asin1half  42727  readvrec2  42731  sn-00idlem2  42769  sn-00idlem3  42770  sn-00id  42771  sn-0tie0  42821  sn-ltaddpos  42823  sn-ltaddneg  42824  relt0neg1  42826  sn-nnne0  42830  reelznn0nn  42831  sn-0lt1  42845  sn-inelr  42857  sn-itrere  42858  sn-retire  42859  pellexlem6  43191  elpell14qr2  43219  oddcomabszz  43301  zindbi  43303  jm2.24  43320  acongeq  43340  arearect  43572  areaquad  43573  reabsifneg  43988  reabsifnpos  43989  reabsifpos  43990  reabsifnneg  43991  imsqrtvalex  44002  relexp01min  44069  imo72b2lem2  44523  imo72b2lem1  44525  imo72b2  44528  dvconstbi  44690  binomcxplemnn0  44705  binomcxplemdvbinom  44709  binomcxplemcvg  44710  binomcxplemnotnn0  44712  sineq0ALT  45292  halffl  45658  ren0  45760  rexanuz2nf  45850  sqrlearg  45913  limsup10ex  46131  dvnmptdivc  46296  dvnmul  46301  itgsin0pilem1  46308  itgsinexplem1  46312  itgsinexp  46313  iblempty  46323  stoweidlem17  46375  stoweidlem36  46394  stoweidlem55  46413  wallispilem1  46423  wallispilem2  46424  wallispilem4  46426  stirlinglem4  46435  stirlinglem13  46444  stirlinglem14  46445  stirlinglem15  46446  stirlingr  46448  dirker2re  46450  dirkerdenne0  46451  dirkerre  46453  dirkertrigeqlem1  46456  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem11  46476  fourierdlem16  46481  fourierdlem21  46486  fourierdlem22  46487  fourierdlem41  46506  fourierdlem42  46507  fourierdlem48  46512  fourierdlem62  46526  fourierdlem66  46530  fourierdlem79  46543  fourierdlem83  46547  fourierdlem94  46558  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  fourierdlem112  46576  fourierdlem113  46577  fourierdlem114  46578  sqwvfoura  46586  sqwvfourb  46587  fourierswlem  46588  fouriersw  46589  etransclem23  46615  etransclem44  46636  etransclem46  46638  salexct3  46700  salgensscntex  46702  sge0rnn0  46726  sge00  46734  0ome  46887  ovn0lem  46923  ovnhoilem1  46959  smfmullem1  47149  smfmullem2  47150  smfmullem3  47151  smfmullem4  47152  squeezedltsq  47246  zm1nn  47662  sqrtnegnre  47667  m1mod0mod1  47714  fmtnoprmfac2lem1  47926  31prm  47957  mod42tp1mod8  47962  nfermltl2rev  48103  tgblthelfgott  48175  usgrexmpl1lem  48381  usgrexmpl2lem  48386  usgrexmpl2nb0  48391  usgrexmpl2nb5  48396  usgrexmpl2trifr  48397  gpgusgralem  48416  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  gpg5edgnedg  48490  altgsumbcALT  48713  expnegico01  48878  dignnld  48963  eenglngeehlnmlem1  49097  line2ylem  49111  line2y  49115  itsclc0yqsollem2  49123  icccldii  49278  i0oii  49279  sepfsepc  49287  ex-gt  50087