Theorem 0re 11138

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3061  (class class class)co 7360  ℂcc 11028  ℝcr 11029  0cc0 11030  1c1 11031  ici 11032   + caddc 11033   · cmul 11035

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 11088  ax-addrcl 11091  ax-rnegex 11101  ax-cnre 11103

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

This theorem is referenced by:  0red  11139  0xr  11183  axmulgt0  11211  ne0gt0  11242  00id  11312  mul02lem1  11313  mul02lem2  11314  mul02  11315  addrid  11317  ltaddneg  11353  addgt0  11627  addgegt0  11628  addgtge0  11629  addge0  11630  ltaddpos  11631  ltneg  11641  leneg  11644  lt0neg1  11647  lt0neg2  11648  le0neg1  11649  le0neg2  11650  addge01  11651  suble0  11655  mulge0  11659  msqge0  11662  0le1  11664  relin01  11665  gt0ne0i  11676  lt0ne0d  11706  elimge0  11984  ltm1  11987  recgt0  11991  prodgt0  11992  lemul1a  11999  ltmul12a  12001  lemul12a  12003  mulgt1OLD  12004  gt0div  12012  ge0div  12013  mulge0b  12016  lediv12a  12039  recgt1i  12043  recreclt  12045  ledivp1  12048  squeeze0  12049  recgt0ii  12052  ledivp1i  12071  ltdivp1i  12072  fimaxre2  12091  inelr  12139  crne0  12142  nnge1  12177  nngt0  12180  nnnle0  12182  nnne0  12183  nnrecgt0  12192  0le0  12250  halfge0  12361  nn0ssre  12409  nn0ge0  12430  nn0nlt0  12431  nn0le0eq0  12433  0mnnnnn0  12437  elnnnn0b  12449  elnnnn0c  12450  nn0sub  12455  elnnz  12502  0z  12503  elnn0z  12505  elnnz1  12521  recnz  12571  gtndiv  12573  fnn0ind  12595  10re  12630  rpge0  12923  rpneg  12943  0nrp  12946  0ltpnf  13040  mnflt0  13043  qsqueeze  13120  xneg0  13131  xaddrid  13160  xnn0xadd0  13166  xmulpnf1  13193  xlemul1a  13207  xadddi  13214  xrsupsslem  13226  xrinfmsslem  13227  elrege0  13374  0e0icopnf  13378  elicc01  13386  0elunit  13389  unitssre  13419  0nelfz1  13463  fzpreddisj  13493  fz0to4untppr  13550  fz0to5un2tp  13551  nn0p1elfzo  13622  ico01fl0  13743  rpsup  13790  modelico  13805  0mod  13826  1mod  13827  le2sq2  14062  expubnd  14105  sqlecan  14136  bernneq2  14157  expnbnd  14159  expnlbnd  14160  expmulnbnd  14162  discr1  14166  discr  14167  faclbnd  14217  faclbnd3  14219  faclbnd6  14226  bcval4  14234  bcval5  14245  bcpasc  14248  hasheq0  14290  hashneq0  14291  hashnn0n0nn  14318  hashgt12el  14349  hashgt12el2  14350  hashge2el2dif  14407  lsw0  14492  swrdccatin2  14656  pfxccatin12lem3  14659  reim0  15045  re0  15079  im0  15080  rei  15083  imi  15084  cj0  15085  sqeqd  15093  rennim  15166  cnpart  15167  sqrt0  15168  01sqrexlem4  15172  resqrex  15177  sqrtgt0  15185  sqrt00  15190  sqrtneglem  15193  sqrt9  15200  sqrt2gt1lt2  15201  leabs  15226  absor  15227  max0add  15237  eqsqrt2d  15296  sqrtpclii  15310  rlimconst  15471  rlimrege0  15506  lo1mul  15555  iserge0  15588  fsum00  15725  isumless  15772  arisum2  15788  georeclim  15799  geo2sum  15800  geoisumr  15805  0.999...  15808  cvgrat  15810  fprodge0  15920  bpoly4  15986  cos0  16079  ef01bndlem  16113  sin01bnd  16114  cos01bnd  16115  cos2bnd  16117  sin01gt0  16119  cos01gt0  16120  sincos2sgn  16123  sin4lt0  16124  absef  16126  absefib  16127  efieq1re  16128  epos  16136  rpnnen2lem2  16144  rpnnen2lem3  16145  rpnnen2lem4  16146  rpnnen2lem9  16151  ruclem6  16164  dvdslelem  16240  divalglem1  16325  divalglem5  16328  divalglem6  16329  flodddiv4  16346  sadcadd  16389  gcdn0gt0  16449  nn0seqcvgd  16501  algcvgblem  16508  algcvga  16510  pythagtriplem12  16758  pythagtriplem13  16759  pythagtriplem14  16760  pythagtriplem16  16762  prmreclem4  16851  prmreclem5  16852  prmreclem6  16853  1arith  16859  ramz  16957  chnub  18549  mulgnegnn  19018  subgmulg  19074  srgbinomlem4  20168  isabvd  20749  abvtrivd  20769  rge0srg  21397  xrs1mnd  21399  xrs10  21400  psgnodpmr  21549  re0g  21571  psrbaglesupp  21882  psdmvr  22116  mnfnei  23169  imasdsf1olem  24321  ssblps  24370  ssbl  24371  xmeter  24381  dscmet  24520  dscopn  24521  nmoi  24676  nmoeq0  24684  0nghm  24689  idnghm  24691  cnbl0  24721  xrsxmet  24758  metdseq0  24803  iicmp  24839  iiconn  24840  iihalf1  24885  iihalf1cnOLD  24887  elii1  24891  icopnfcnv  24900  icopnfhmeo  24901  iccpnfcnv  24902  xrhmeo  24904  xrhmph  24905  htpycc  24939  reparphti  24956  reparphtiOLD  24957  pcoval1  24973  pco0  24974  pcoval2  24976  pcocn  24977  pcohtpylem  24979  pcopt  24982  pcopt2  24983  pcoass  24984  pcorevlem  24986  reust  25341  recusp  25342  rrx0el  25358  minveclem4c  25385  minveclem2  25386  minveclem3b  25388  minveclem4  25392  minveclem7  25395  pjthlem1  25397  cniccbdd  25422  ovolunnul  25461  ovoliunnul  25468  ovolicc1  25477  ovolre  25486  iccvolcl  25528  ovolioo  25529  ioovolcl  25531  ioorcl  25538  vitalilem4  25572  vitalilem5  25573  vitali  25574  ismbf  25589  mbfmulc2lem  25608  mbfpos  25612  mbfposr  25613  i1f0  25648  i1f1  25651  itg1addlem2  25658  itg1addlem4  25660  itg1addlem5  25661  mbfi1fseqlem4  25679  mbfi1fseqlem5  25680  mbfi1flimlem  25683  xrge0f  25692  itg2ge0  25696  itg2const  25701  itg2mulc  25708  itg2splitlem  25709  itg2gt0  25721  itg2cnlem1  25722  ibl0  25748  iblrelem  25752  iblposlem  25753  iblpos  25754  iblre  25755  itgreval  25758  itgneg  25765  iblss  25766  i1fibl  25769  itgitg1  25770  itgle  25771  itgeqa  25775  itgless  25778  iblconst  25779  itgconst  25780  ibladdlem  25781  itgaddlem2  25785  iblabslem  25789  iblabsr  25791  iblmulc2  25792  itgmulc2lem2  25794  itgabs  25796  itgsplit  25797  bddmulibl  25800  dvferm1  25949  dvferm2  25951  dvferm  25952  dvlip  25958  c1lip1  25962  dveq0  25965  dv11cn  25966  dvne0  25976  ftc1lem4  26006  ply1divex  26102  dgrco  26241  plyrecj  26247  vieta1lem2  26279  aalioulem2  26301  aalioulem3  26302  pserulm  26391  psercnlem2  26394  psercnlem1  26395  psercn  26396  abelth  26411  reeff1olem  26416  reeff1o  26417  pilem2  26422  pilem3  26423  pipos  26428  sinhalfpilem  26432  sincosq1sgn  26467  sincosq2sgn  26468  coseq00topi  26471  coseq0negpitopi  26472  tangtx  26474  tanabsge  26475  sinq12ge0  26477  sinq34lt0t  26478  cosq14ge0  26480  sincos4thpi  26482  sincos6thpi  26485  pige3ALT  26489  sineq0  26493  cosordlem  26499  cosord  26500  cos0pilt1  26501  cos11  26502  sinord  26503  recosf1o  26504  resinf1o  26505  tanord1  26506  tanord  26507  tanregt0  26508  efif1olem4  26514  efifo  26516  relogrn  26530  log1  26554  logi  26556  logneg  26557  argregt0  26579  argrege0  26580  argimgt0  26581  logneg2  26584  logdivlti  26589  logdivlt  26590  ellogdm  26608  logdmn0  26609  logdmnrp  26610  logcnlem3  26613  dvloglem  26617  logdmopn  26618  logf1o2  26619  dvlog2lem  26621  efopnlem1  26625  logtayl  26629  recxpcl  26644  cxpge0  26652  cxple2  26666  cxple2a  26668  cxpsqrtlem  26671  cxpcn3  26718  cxpaddlelem  26721  cxpaddle  26722  loglesqrt  26731  logbrec  26752  ang180lem3  26781  ang180lem4  26782  asinneg  26856  asin1  26864  reasinsin  26866  acosbnd  26870  atan0  26878  atanrecl  26881  atanlogaddlem  26883  atanlogsublem  26885  atanlogsub  26886  atantan  26893  atanbnd  26896  atan1  26898  atans2  26901  ressatans  26904  log2cnv  26914  log2tlbnd  26915  log2ub  26919  log2le1  26920  rlimcnp  26935  rlimcnp2  26936  o1cxp  26945  jensen  26959  amgm  26961  emgt0  26977  harmonicbnd3  26978  harmoniclbnd  26979  harmonicbnd4  26981  zetacvg  26985  eldmgm  26992  lgamgulmlem2  27000  basellem3  27053  basellem8  27058  efnnfsumcl  27073  ppisval  27074  vmage0  27091  chpge0  27096  efchtdvds  27129  ppiltx  27147  ppiub  27175  chpeq0  27179  chteq0  27180  chtleppi  27181  chpchtsum  27190  chpub  27191  dchr1re  27234  bcmono  27248  efexple  27252  bposlem1  27255  bposlem4  27258  bposlem5  27259  bposlem7  27261  bposlem8  27262  bposlem9  27263  lgsval2lem  27278  lgsval4a  27290  lgsneg  27292  lgsdilem  27295  lgsdir2lem1  27296  2lgsoddprmlem3a  27381  2lgsoddprmlem3b  27382  2lgsoddprmlem3c  27383  2lgsoddprmlem3d  27384  rplogsumlem2  27456  rpvmasumlem  27458  dchrisum0flblem1  27479  dchrisum0flblem2  27480  dchrisum0fno1  27482  rplogsum  27498  logdivsum  27504  mulog2sumlem2  27506  selberg2lem  27521  logdivbnd  27527  pntrsumo1  27536  pntrlog2bndlem4  27551  pntrlog2bndlem5  27552  pntpbnd1  27557  pntpbnd2  27558  pntlem3  27580  pntleml  27582  ostth2  27608  trgcgrg  28570  ttgcontlem1  28940  axlowdimlem1  28998  axlowdimlem6  29003  axlowdimlem7  29004  axlowdimlem10  29007  axlowdim1  29015  axlowdim2  29016  axlowdim  29017  elntg2  29041  umgrislfupgrlem  29178  lfgrnloop  29181  lfuhgr1v0e  29310  usgrexmplef  29315  pthdlem2  29824  crctcshwlkn0lem7  29872  rusgrnumwwlks  30033  clwwlkn0  30086  konigsberg  30315  ex-po  30493  ex-sqrt  30512  ex-gcd  30515  nvz0  30726  0blo  30850  nmlno0lem  30851  nmblolbii  30857  siilem2  30910  minvecolem2  30933  minvecolem3  30934  minvecolem4c  30937  minvecolem4  30938  minvecolem5  30939  minvecolem7  30941  htthlem  30975  hiidge0  31156  normlem6  31173  normgt0  31185  norm-i  31187  normpyc  31204  bcsiALT  31237  pjhthlem1  31449  pjneli  31781  nmlnop0iALT  32053  unopbd  32073  nmbdoplbi  32082  nmcoplbi  32086  nmbdfnlbi  32107  nmbdfnlb  32108  nmcfnlbi  32110  cnlnadjlem7  32131  nmopcoi  32153  branmfn  32163  leopmul  32192  nmopleid  32197  pjbdlni  32207  pjnormssi  32226  stle0i  32297  cdj3lem1  32492  xaddeq0  32814  expgt0b  32878  pr01ssre  32886  sgnclre  32894  sgnnbi  32900  sgnpbi  32901  indf  32915  indfval  32916  dp20u  32940  dp20h  32941  dp2clq  32943  dp2lt10  32946  dp2lt  32947  dp0u  32963  dplti  32967  dpexpp1  32970  xdiv0  32991  xrge0slmod  33410  evl1deg3  33640  fldext2chn  33866  cos9thpiminplylem1  33920  unitdivcld  34039  sqsscirc1  34046  xrge0iifcnv  34071  xrge0iifiso  34073  rezh  34107  esumcvgsum  34226  voliune  34367  volfiniune  34368  sibfinima  34477  sitmcl  34489  0rrv  34589  coinfliprv  34621  ballotlem2  34627  ballotlem4  34637  ballotlemi1  34641  ballotlemic  34645  plymulx0  34685  signsply0  34689  signswch  34699  signstf  34704  signstf0  34706  signstfveq0  34715  signlem0  34725  signshf  34726  itgexpif  34744  hgt750lemd  34786  hgt750lem  34789  hgt750lem2  34790  hgt750leme  34796  iisconn  35427  iillysconn  35428  cvmliftlem10  35469  fz0n  35906  bcneg1  35911  nn0prpwlem  36497  dnizeq0  36650  dnizphlfeqhlf  36651  knoppndvlem13  36699  cnndvlem1  36712  bj-pinftyccb  37397  bj-minftyccb  37401  bj-pinftynminfty  37403  taupilemrplb  37496  irrdiff  37502  sin2h  37782  tan2h  37784  ptrecube  37792  poimirlem16  37808  poimirlem17  37809  poimirlem20  37812  poimirlem22  37814  poimirlem23  37815  poimirlem29  37821  poimirlem31  37823  poimir  37825  heicant  37827  mblfinlem2  37830  ismblfin  37833  ovoliunnfl  37834  voliunnfl  37836  volsupnfl  37837  mbfposadd  37839  itg2addnclem  37843  itg2addnclem2  37844  ibladdnclem  37848  itgaddnclem2  37851  iblabsnclem  37855  iblmulc2nc  37857  itgmulc2nclem2  37859  itgabsnc  37861  ftc1cnnclem  37863  ftc1anclem5  37869  ftc1anclem8  37872  asindmre  37875  dvasin  37876  areacirclem4  37883  areacirc  37885  isbnd3  37956  ssbnd  37960  prdsbnd  37965  bfplem2  37995  bfp  37996  renegclALT  39260  0cnALT3  42544  sn-1ne2  42556  itrere  42609  oexpreposd  42613  tan3rdpi  42643  asin1half  42648  readvrec2  42652  sn-00idlem2  42690  sn-00idlem3  42691  sn-00id  42692  sn-0tie0  42742  sn-ltaddpos  42744  sn-ltaddneg  42745  relt0neg1  42747  sn-nnne0  42751  reelznn0nn  42752  sn-0lt1  42766  sn-inelr  42778  sn-itrere  42779  sn-retire  42780  pellexlem6  43112  elpell14qr2  43140  oddcomabszz  43222  zindbi  43224  jm2.24  43241  acongeq  43261  arearect  43493  areaquad  43494  reabsifneg  43909  reabsifnpos  43910  reabsifpos  43911  reabsifnneg  43912  imsqrtvalex  43923  relexp01min  43990  imo72b2lem2  44444  imo72b2lem1  44446  imo72b2  44449  dvconstbi  44611  binomcxplemnn0  44626  binomcxplemdvbinom  44630  binomcxplemcvg  44631  binomcxplemnotnn0  44633  sineq0ALT  45213  halffl  45580  ren0  45682  rexanuz2nf  45772  sqrlearg  45835  limsup10ex  46053  dvnmptdivc  46218  dvnmul  46223  itgsin0pilem1  46230  itgsinexplem1  46234  itgsinexp  46235  iblempty  46245  stoweidlem17  46297  stoweidlem36  46316  stoweidlem55  46335  wallispilem1  46345  wallispilem2  46346  wallispilem4  46348  stirlinglem4  46357  stirlinglem13  46366  stirlinglem14  46367  stirlinglem15  46368  stirlingr  46370  dirker2re  46372  dirkerdenne0  46373  dirkerre  46375  dirkertrigeqlem1  46378  dirkercncflem2  46384  dirkercncflem4  46386  fourierdlem11  46398  fourierdlem16  46403  fourierdlem21  46408  fourierdlem22  46409  fourierdlem41  46428  fourierdlem42  46429  fourierdlem48  46434  fourierdlem62  46448  fourierdlem66  46452  fourierdlem79  46465  fourierdlem83  46469  fourierdlem94  46480  fourierdlem102  46488  fourierdlem103  46489  fourierdlem104  46490  fourierdlem111  46497  fourierdlem112  46498  fourierdlem113  46499  fourierdlem114  46500  sqwvfoura  46508  sqwvfourb  46509  fourierswlem  46510  fouriersw  46511  etransclem23  46537  etransclem44  46558  etransclem46  46560  salexct3  46622  salgensscntex  46624  sge0rnn0  46648  sge00  46656  0ome  46809  ovn0lem  46845  ovnhoilem1  46881  smfmullem1  47071  smfmullem2  47072  smfmullem3  47073  smfmullem4  47074  squeezedltsq  47168  zm1nn  47584  sqrtnegnre  47589  m1mod0mod1  47636  fmtnoprmfac2lem1  47848  31prm  47879  mod42tp1mod8  47884  nfermltl2rev  48025  tgblthelfgott  48097  usgrexmpl1lem  48303  usgrexmpl2lem  48308  usgrexmpl2nb0  48313  usgrexmpl2nb5  48318  usgrexmpl2trifr  48319  gpgusgralem  48338  pgnbgreunbgrlem2lem1  48396  pgnbgreunbgrlem2lem2  48397  pgnbgreunbgrlem2lem3  48398  gpg5edgnedg  48412  altgsumbcALT  48635  expnegico01  48800  dignnld  48885  eenglngeehlnmlem1  49019  line2ylem  49033  line2y  49037  itsclc0yqsollem2  49045  icccldii  49200  i0oii  49201  sepfsepc  49209  ex-gt  50009