Theorem 0re 11176

Description: The number 0 is real. Remark: the first step could also be ax-icn 11127. See also 0reALT 11519. (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 11126	. 2 ⊢ 1 ∈ ℂ
2		cnre 11171	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11139	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11151	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2816	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3134	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3126	. 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 7387  ℂcc 11066  ℝcr 11067  0cc0 11068  1c1 11069  ici 11070   + caddc 11071   · cmul 11073

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 11126  ax-addrcl 11129  ax-rnegex 11139  ax-cnre 11141

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  11177  0xr  11221  axmulgt0  11248  ne0gt0  11279  00id  11349  mul02lem1  11350  mul02lem2  11351  mul02  11352  addrid  11354  ltaddneg  11390  addgt0  11664  addgegt0  11665  addgtge0  11666  addge0  11667  ltaddpos  11668  ltneg  11678  leneg  11681  lt0neg1  11684  lt0neg2  11685  le0neg1  11686  le0neg2  11687  addge01  11688  suble0  11692  mulge0  11696  msqge0  11699  0le1  11701  relin01  11702  gt0ne0i  11713  lt0ne0d  11743  elimge0  12021  ltm1  12024  recgt0  12028  prodgt0  12029  lemul1a  12036  ltmul12a  12038  lemul12a  12040  mulgt1OLD  12041  gt0div  12049  ge0div  12050  mulge0b  12053  lediv12a  12076  recgt1i  12080  recreclt  12082  ledivp1  12085  squeeze0  12086  recgt0ii  12089  ledivp1i  12108  ltdivp1i  12109  fimaxre2  12128  inelr  12176  crne0  12179  nnge1  12214  nngt0  12217  nnnle0  12219  nnne0  12220  nnrecgt0  12229  0le0  12287  halfge0  12398  nn0ssre  12446  nn0ge0  12467  nn0nlt0  12468  nn0le0eq0  12470  0mnnnnn0  12474  elnnnn0b  12486  elnnnn0c  12487  nn0sub  12492  elnnz  12539  0z  12540  elnn0z  12542  elnnz1  12559  recnz  12609  gtndiv  12611  fnn0ind  12633  10re  12668  rpge0  12965  rpneg  12985  0nrp  12988  0ltpnf  13082  mnflt0  13085  qsqueeze  13161  xneg0  13172  xaddrid  13201  xnn0xadd0  13207  xmulpnf1  13234  xlemul1a  13248  xadddi  13255  xrsupsslem  13267  xrinfmsslem  13268  elrege0  13415  0e0icopnf  13419  elicc01  13427  0elunit  13430  unitssre  13460  0nelfz1  13504  fzpreddisj  13534  fz0to4untppr  13591  fz0to5un2tp  13592  nn0p1elfzo  13663  ico01fl0  13781  rpsup  13828  modelico  13843  0mod  13864  1mod  13865  le2sq2  14100  expubnd  14143  sqlecan  14174  bernneq2  14195  expnbnd  14197  expnlbnd  14198  expmulnbnd  14200  discr1  14204  discr  14205  faclbnd  14255  faclbnd3  14257  faclbnd6  14264  bcval4  14272  bcval5  14283  bcpasc  14286  hasheq0  14328  hashneq0  14329  hashnn0n0nn  14356  hashgt12el  14387  hashgt12el2  14388  hashge2el2dif  14445  lsw0  14530  swrdccatin2  14694  pfxccatin12lem3  14697  reim0  15084  re0  15118  im0  15119  rei  15122  imi  15123  cj0  15124  sqeqd  15132  rennim  15205  cnpart  15206  sqrt0  15207  01sqrexlem4  15211  resqrex  15216  sqrtgt0  15224  sqrt00  15229  sqrtneglem  15232  sqrt9  15239  sqrt2gt1lt2  15240  leabs  15265  absor  15266  max0add  15276  eqsqrt2d  15335  sqrtpclii  15349  rlimconst  15510  rlimrege0  15545  lo1mul  15594  iserge0  15627  fsum00  15764  isumless  15811  arisum2  15827  georeclim  15838  geo2sum  15839  geoisumr  15844  0.999...  15847  cvgrat  15849  fprodge0  15959  bpoly4  16025  cos0  16118  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  cos2bnd  16156  sin01gt0  16158  cos01gt0  16159  sincos2sgn  16162  sin4lt0  16163  absef  16165  absefib  16166  efieq1re  16167  epos  16175  rpnnen2lem2  16183  rpnnen2lem3  16184  rpnnen2lem4  16185  rpnnen2lem9  16190  ruclem6  16203  dvdslelem  16279  divalglem1  16364  divalglem5  16367  divalglem6  16368  flodddiv4  16385  sadcadd  16428  gcdn0gt0  16488  nn0seqcvgd  16540  algcvgblem  16547  algcvga  16549  pythagtriplem12  16797  pythagtriplem13  16798  pythagtriplem14  16799  pythagtriplem16  16801  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  1arith  16898  ramz  16996  mulgnegnn  19016  subgmulg  19072  srgbinomlem4  20138  isabvd  20721  abvtrivd  20741  xrs1mnd  21321  xrs10  21322  rge0srg  21355  psgnodpmr  21499  re0g  21521  psrbaglesupp  21831  psdmvr  22056  mnfnei  23108  imasdsf1olem  24261  ssblps  24310  ssbl  24311  xmeter  24321  dscmet  24460  dscopn  24461  nmoi  24616  nmoeq0  24624  0nghm  24629  idnghm  24631  cnbl0  24661  xrsxmet  24698  metdseq0  24743  iicmp  24779  iiconn  24780  iihalf1  24825  iihalf1cnOLD  24827  elii1  24831  icopnfcnv  24840  icopnfhmeo  24841  iccpnfcnv  24842  xrhmeo  24844  xrhmph  24845  htpycc  24879  reparphti  24896  reparphtiOLD  24897  pcoval1  24913  pco0  24914  pcoval2  24916  pcocn  24917  pcohtpylem  24919  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevlem  24926  reust  25281  recusp  25282  rrx0el  25298  minveclem4c  25325  minveclem2  25326  minveclem3b  25328  minveclem4  25332  minveclem7  25335  pjthlem1  25337  cniccbdd  25362  ovolunnul  25401  ovoliunnul  25408  ovolicc1  25417  ovolre  25426  iccvolcl  25468  ovolioo  25469  ioovolcl  25471  ioorcl  25478  vitalilem4  25512  vitalilem5  25513  vitali  25514  ismbf  25529  mbfmulc2lem  25548  mbfpos  25552  mbfposr  25553  i1f0  25588  i1f1  25591  itg1addlem2  25598  itg1addlem4  25600  itg1addlem5  25601  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1flimlem  25623  xrge0f  25632  itg2ge0  25636  itg2const  25641  itg2mulc  25648  itg2splitlem  25649  itg2gt0  25661  itg2cnlem1  25662  ibl0  25688  iblrelem  25692  iblposlem  25693  iblpos  25694  iblre  25695  itgreval  25698  itgneg  25705  iblss  25706  i1fibl  25709  itgitg1  25710  itgle  25711  itgeqa  25715  itgless  25718  iblconst  25719  itgconst  25720  ibladdlem  25721  itgaddlem2  25725  iblabslem  25729  iblabsr  25731  iblmulc2  25732  itgmulc2lem2  25734  itgabs  25736  itgsplit  25737  bddmulibl  25740  dvferm1  25889  dvferm2  25891  dvferm  25892  dvlip  25898  c1lip1  25902  dveq0  25905  dv11cn  25906  dvne0  25916  ftc1lem4  25946  ply1divex  26042  dgrco  26181  plyrecj  26187  vieta1lem2  26219  aalioulem2  26241  aalioulem3  26242  pserulm  26331  psercnlem2  26334  psercnlem1  26335  psercn  26336  abelth  26351  reeff1olem  26356  reeff1o  26357  pilem2  26362  pilem3  26363  pipos  26368  sinhalfpilem  26372  sincosq1sgn  26407  sincosq2sgn  26408  coseq00topi  26411  coseq0negpitopi  26412  tangtx  26414  tanabsge  26415  sinq12ge0  26417  sinq34lt0t  26418  cosq14ge0  26420  sincos4thpi  26422  sincos6thpi  26425  pige3ALT  26429  sineq0  26433  cosordlem  26439  cosord  26440  cos0pilt1  26441  cos11  26442  sinord  26443  recosf1o  26444  resinf1o  26445  tanord1  26446  tanord  26447  tanregt0  26448  efif1olem4  26454  efifo  26456  relogrn  26470  log1  26494  logi  26496  logneg  26497  argregt0  26519  argrege0  26520  argimgt0  26521  logneg2  26524  logdivlti  26529  logdivlt  26530  ellogdm  26548  logdmn0  26549  logdmnrp  26550  logcnlem3  26553  dvloglem  26557  logdmopn  26558  logf1o2  26559  dvlog2lem  26561  efopnlem1  26565  logtayl  26569  recxpcl  26584  cxpge0  26592  cxple2  26606  cxple2a  26608  cxpsqrtlem  26611  cxpcn3  26658  cxpaddlelem  26661  cxpaddle  26662  loglesqrt  26671  logbrec  26692  ang180lem3  26721  ang180lem4  26722  asinneg  26796  asin1  26804  reasinsin  26806  acosbnd  26810  atan0  26818  atanrecl  26821  atanlogaddlem  26823  atanlogsublem  26825  atanlogsub  26826  atantan  26833  atanbnd  26836  atan1  26838  atans2  26841  ressatans  26844  log2cnv  26854  log2tlbnd  26855  log2ub  26859  log2le1  26860  rlimcnp  26875  rlimcnp2  26876  o1cxp  26885  jensen  26899  amgm  26901  emgt0  26917  harmonicbnd3  26918  harmoniclbnd  26919  harmonicbnd4  26921  zetacvg  26925  eldmgm  26932  lgamgulmlem2  26940  basellem3  26993  basellem8  26998  efnnfsumcl  27013  ppisval  27014  vmage0  27031  chpge0  27036  efchtdvds  27069  ppiltx  27087  ppiub  27115  chpeq0  27119  chteq0  27120  chtleppi  27121  chpchtsum  27130  chpub  27131  dchr1re  27174  bcmono  27188  efexple  27192  bposlem1  27195  bposlem4  27198  bposlem5  27199  bposlem7  27201  bposlem8  27202  bposlem9  27203  lgsval2lem  27218  lgsval4a  27230  lgsneg  27232  lgsdilem  27235  lgsdir2lem1  27236  2lgsoddprmlem3a  27321  2lgsoddprmlem3b  27322  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  rplogsumlem2  27396  rpvmasumlem  27398  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0fno1  27422  rplogsum  27438  logdivsum  27444  mulog2sumlem2  27446  selberg2lem  27461  logdivbnd  27467  pntrsumo1  27476  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntpbnd1  27497  pntpbnd2  27498  pntlem3  27520  pntleml  27522  ostth2  27548  trgcgrg  28442  ttgcontlem1  28812  axlowdimlem1  28869  axlowdimlem6  28874  axlowdimlem7  28875  axlowdimlem10  28878  axlowdim1  28886  axlowdim2  28887  axlowdim  28888  elntg2  28912  umgrislfupgrlem  29049  lfgrnloop  29052  lfuhgr1v0e  29181  usgrexmplef  29186  pthdlem2  29698  crctcshwlkn0lem7  29746  rusgrnumwwlks  29904  clwwlkn0  29957  konigsberg  30186  ex-po  30364  ex-sqrt  30383  ex-gcd  30386  nvz0  30597  0blo  30721  nmlno0lem  30722  nmblolbii  30728  siilem2  30781  minvecolem2  30804  minvecolem3  30805  minvecolem4c  30808  minvecolem4  30809  minvecolem5  30810  minvecolem7  30812  htthlem  30846  hiidge0  31027  normlem6  31044  normgt0  31056  norm-i  31058  normpyc  31075  bcsiALT  31108  pjhthlem1  31320  pjneli  31652  nmlnop0iALT  31924  unopbd  31944  nmbdoplbi  31953  nmcoplbi  31957  nmbdfnlbi  31978  nmbdfnlb  31979  nmcfnlbi  31981  cnlnadjlem7  32002  nmopcoi  32024  branmfn  32034  leopmul  32063  nmopleid  32068  pjbdlni  32078  pjnormssi  32097  stle0i  32168  cdj3lem1  32363  xaddeq0  32676  expgt0b  32741  pr01ssre  32749  sgnclre  32757  sgnnbi  32763  sgnpbi  32764  indf  32778  indfval  32779  dp20u  32798  dp20h  32799  dp2clq  32801  dp2lt10  32804  dp2lt  32805  dp0u  32821  dplti  32825  dpexpp1  32828  xdiv0  32849  chnub  32938  xrge0slmod  33319  evl1deg3  33547  fldext2chn  33718  cos9thpiminplylem1  33772  unitdivcld  33891  sqsscirc1  33898  xrge0iifcnv  33923  xrge0iifiso  33925  rezh  33959  esumcvgsum  34078  voliune  34219  volfiniune  34220  sibfinima  34330  sitmcl  34342  0rrv  34442  coinfliprv  34474  ballotlem2  34480  ballotlem4  34490  ballotlemi1  34494  ballotlemic  34498  plymulx0  34538  signsply0  34542  signswch  34552  signstf  34557  signstf0  34559  signstfveq0  34568  signlem0  34578  signshf  34579  itgexpif  34597  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  hgt750leme  34649  iisconn  35239  iillysconn  35240  cvmliftlem10  35281  fz0n  35718  bcneg1  35723  nn0prpwlem  36310  dnizeq0  36463  dnizphlfeqhlf  36464  knoppndvlem13  36512  cnndvlem1  36525  bj-pinftyccb  37209  bj-minftyccb  37213  bj-pinftynminfty  37215  taupilemrplb  37308  irrdiff  37314  sin2h  37604  tan2h  37606  ptrecube  37614  poimirlem16  37630  poimirlem17  37631  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem29  37643  poimirlem31  37645  poimir  37647  heicant  37649  mblfinlem2  37652  ismblfin  37655  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  mbfposadd  37661  itg2addnclem  37665  itg2addnclem2  37666  ibladdnclem  37670  itgaddnclem2  37673  iblabsnclem  37677  iblmulc2nc  37679  itgmulc2nclem2  37681  itgabsnc  37683  ftc1cnnclem  37685  ftc1anclem5  37691  ftc1anclem8  37694  asindmre  37697  dvasin  37698  areacirclem4  37705  areacirc  37707  isbnd3  37778  ssbnd  37782  prdsbnd  37787  bfplem2  37817  bfp  37818  renegclALT  38956  0cnALT3  42241  sn-1ne2  42253  itrere  42306  oexpreposd  42310  tan3rdpi  42340  asin1half  42345  readvrec2  42349  sn-00idlem2  42387  sn-00idlem3  42388  sn-00id  42389  sn-0tie0  42439  sn-ltaddpos  42441  sn-ltaddneg  42442  relt0neg1  42444  sn-nnne0  42448  reelznn0nn  42449  sn-0lt1  42463  sn-inelr  42475  sn-itrere  42476  sn-retire  42477  pellexlem6  42822  elpell14qr2  42850  oddcomabszz  42933  zindbi  42935  jm2.24  42952  acongeq  42972  arearect  43204  areaquad  43205  reabsifneg  43621  reabsifnpos  43622  reabsifpos  43623  reabsifnneg  43624  imsqrtvalex  43635  relexp01min  43702  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  dvconstbi  44323  binomcxplemnn0  44338  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemnotnn0  44345  sineq0ALT  44926  halffl  45294  ren0  45398  rexanuz2nf  45488  sqrlearg  45551  limsup10ex  45771  dvnmptdivc  45936  dvnmul  45941  itgsin0pilem1  45948  itgsinexplem1  45952  itgsinexp  45953  iblempty  45963  stoweidlem17  46015  stoweidlem36  46034  stoweidlem55  46053  wallispilem1  46063  wallispilem2  46064  wallispilem4  46066  stirlinglem4  46075  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  stirlingr  46088  dirker2re  46090  dirkerdenne0  46091  dirkerre  46093  dirkertrigeqlem1  46096  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem11  46116  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fourierdlem62  46166  fourierdlem66  46170  fourierdlem79  46183  fourierdlem83  46187  fourierdlem94  46198  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fourierdlem114  46218  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  etransclem23  46255  etransclem44  46276  etransclem46  46278  salexct3  46340  salgensscntex  46342  sge0rnn0  46366  sge00  46374  0ome  46527  ovn0lem  46563  ovnhoilem1  46599  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  smfmullem4  46792  squeezedltsq  46887  zm1nn  47303  sqrtnegnre  47308  m1mod0mod1  47355  fmtnoprmfac2lem1  47567  31prm  47598  mod42tp1mod8  47603  nfermltl2rev  47744  tgblthelfgott  47816  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  gpgusgralem  48047  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  altgsumbcALT  48341  expnegico01  48507  dignnld  48592  eenglngeehlnmlem1  48726  line2ylem  48740  line2y  48744  itsclc0yqsollem2  48752  icccldii  48907  i0oii  48908  sepfsepc  48916  ex-gt  49717