Theorem 0re 11213

Description: The number 0 is real. Remark: the first step could also be ax-icn 11166. See also 0reALT 11554. (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 11165	. 2 ⊢ 1 ∈ ℂ
2		cnre 11208	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11178	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11190	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2822	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 244	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3156	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 482	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3148	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071  (class class class)co 7406  ℂcc 11105  ℝcr 11106  0cc0 11107  1c1 11108  ici 11109   + caddc 11110   · cmul 11112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11165  ax-addrcl 11168  ax-rnegex 11178  ax-cnre 11180

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-rex 3072

This theorem is referenced by:  0red  11214  0xr  11258  axmulgt0  11285  ne0gt0  11316  00id  11386  mul02lem1  11387  mul02lem2  11388  mul02  11389  addrid  11391  ltaddneg  11426  addgt0  11697  addgegt0  11698  addgtge0  11699  addge0  11700  ltaddpos  11701  ltneg  11711  leneg  11714  lt0neg1  11717  lt0neg2  11718  le0neg1  11719  le0neg2  11720  addge01  11721  suble0  11725  mulge0  11729  msqge0  11732  0le1  11734  relin01  11735  gt0ne0i  11746  gt0ne0d  11775  lt0ne0d  11776  elimge0  12050  ltm1  12053  recgt0  12057  prodgt0  12058  lemul1a  12065  ltmul12a  12067  lemul12a  12069  mulgt1  12070  gt0div  12077  ge0div  12078  mulge0b  12081  lediv12a  12104  recgt1i  12108  recreclt  12110  ledivp1  12113  squeeze0  12114  recgt0ii  12117  ledivp1i  12136  ltdivp1i  12137  fimaxre2  12156  inelr  12199  crne0  12202  nnge1  12237  nngt0  12240  nnnle0  12242  nnne0  12243  nnrecgt0  12252  0le0  12310  neg1lt0  12326  halfge0  12426  nn0ssre  12473  nn0ge0  12494  nn0nlt0  12495  nn0le0eq0  12497  0mnnnnn0  12501  elnnnn0b  12513  elnnnn0c  12514  nn0sub  12519  elnnz  12565  0z  12566  elnn0z  12568  elnnz1  12585  recnz  12634  gtndiv  12636  fnn0ind  12658  10re  12693  rpge0  12984  rpneg  13003  0nrp  13006  0ltpnf  13099  mnflt0  13102  qsqueeze  13177  xneg0  13188  xaddrid  13217  xnn0xadd0  13223  xmulpnf1  13250  xlemul1a  13264  xadddi  13271  xrsupsslem  13283  xrinfmsslem  13284  elrege0  13428  0e0icopnf  13432  elicc01  13440  0elunit  13443  unitssre  13473  0nelfz1  13517  fzpreddisj  13547  fz0to4untppr  13601  nn0p1elfzo  13672  ico01fl0  13781  rpsup  13828  modelico  13843  0mod  13864  1mod  13865  le2sq2  14097  expubnd  14139  sqlecan  14170  bernneq2  14190  expnbnd  14192  expnlbnd  14193  expmulnbnd  14195  discr1  14199  discr  14200  faclbnd  14247  faclbnd3  14249  faclbnd6  14256  bcval4  14264  bcval5  14275  bcpasc  14278  hasheq0  14320  hashneq0  14321  hashnn0n0nn  14348  hashgt12el  14379  hashgt12el2  14380  hashge2el2dif  14438  lsw0  14512  swrdccatin2  14676  pfxccatin12lem3  14679  reim0  15062  re0  15096  im0  15097  rei  15100  imi  15101  cj0  15102  sqeqd  15110  rennim  15183  cnpart  15184  sqrt0  15185  01sqrexlem4  15189  resqrex  15194  sqrtgt0  15202  sqrt00  15207  sqrtneglem  15210  sqrt9  15217  sqrt2gt1lt2  15218  leabs  15243  absor  15244  max0add  15254  eqsqrt2d  15312  sqrtpclii  15326  rlimconst  15485  rlimrege0  15520  lo1mul  15569  iserge0  15604  fsum00  15741  isumless  15788  arisum2  15804  georeclim  15815  geo2sum  15816  geoisumr  15821  0.999...  15824  cvgrat  15826  fprodge0  15934  bpoly4  16000  cos0  16090  ef01bndlem  16124  sin01bnd  16125  cos01bnd  16126  cos2bnd  16128  sin01gt0  16130  cos01gt0  16131  sincos2sgn  16134  sin4lt0  16135  absef  16137  absefib  16138  efieq1re  16139  epos  16147  rpnnen2lem2  16155  rpnnen2lem3  16156  rpnnen2lem4  16157  rpnnen2lem9  16162  ruclem6  16175  dvdslelem  16249  divalglem1  16334  divalglem5  16337  divalglem6  16338  flodddiv4  16353  sadcadd  16396  gcdn0gt0  16456  nn0seqcvgd  16504  algcvgblem  16511  algcvga  16513  pythagtriplem12  16756  pythagtriplem13  16757  pythagtriplem14  16758  pythagtriplem16  16760  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  1arith  16857  ramz  16955  mulgnegnn  18959  subgmulg  19015  srgbinomlem4  20046  isabvd  20421  abvtrivd  20441  xrs1mnd  20976  xrs10  20977  rge0srg  21009  psgnodpmr  21135  re0g  21157  psrbaglesupp  21469  psrbaglesuppOLD  21470  mnfnei  22717  imasdsf1olem  23871  ssblps  23920  ssbl  23921  xmeter  23931  dscmet  24073  dscopn  24074  nmoi  24237  nmoeq0  24245  0nghm  24250  idnghm  24252  cnbl0  24282  xrsxmet  24317  metdseq0  24362  iicmp  24394  iiconn  24395  iihalf1  24439  iihalf1cn  24440  elii1  24443  icopnfcnv  24450  icopnfhmeo  24451  iccpnfcnv  24452  xrhmeo  24454  xrhmph  24455  htpycc  24488  reparphti  24505  pcoval1  24521  pco0  24522  pcoval2  24524  pcocn  24525  pcohtpylem  24527  pcopt  24530  pcopt2  24531  pcoass  24532  pcorevlem  24534  reust  24890  recusp  24891  rrx0el  24907  minveclem4c  24934  minveclem2  24935  minveclem3b  24937  minveclem4  24941  minveclem7  24944  pjthlem1  24946  cniccbdd  24970  ovolunnul  25009  ovoliunnul  25016  ovolicc1  25025  ovolre  25034  iccvolcl  25076  ovolioo  25077  ioovolcl  25079  ioorcl  25086  vitalilem4  25120  vitalilem5  25121  vitali  25122  ismbf  25137  mbfmulc2lem  25156  mbfpos  25160  mbfposr  25161  i1f0  25196  i1f1  25199  itg1addlem2  25206  itg1addlem4  25208  itg1addlem4OLD  25209  itg1addlem5  25210  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1flimlem  25232  xrge0f  25241  itg2ge0  25245  itg2const  25250  itg2mulc  25257  itg2splitlem  25258  itg2gt0  25270  itg2cnlem1  25271  ibl0  25296  iblrelem  25300  iblposlem  25301  iblpos  25302  iblre  25303  itgreval  25306  itgneg  25313  iblss  25314  i1fibl  25317  itgitg1  25318  itgle  25319  itgeqa  25323  itgless  25326  iblconst  25327  itgconst  25328  ibladdlem  25329  itgaddlem2  25333  iblabslem  25337  iblabsr  25339  iblmulc2  25340  itgmulc2lem2  25342  itgabs  25344  itgsplit  25345  bddmulibl  25348  dvferm1  25494  dvferm2  25496  dvferm  25497  dvlip  25502  c1lip1  25506  dveq0  25509  dv11cn  25510  dvne0  25520  ftc1lem4  25548  ply1divex  25646  dgrco  25781  plyrecj  25785  vieta1lem2  25816  aalioulem2  25838  aalioulem3  25839  pserulm  25926  psercnlem2  25928  psercnlem1  25929  psercn  25930  abelth  25945  reeff1olem  25950  reeff1o  25951  pilem2  25956  pilem3  25957  pipos  25962  sinhalfpilem  25965  sincosq1sgn  26000  sincosq2sgn  26001  coseq00topi  26004  coseq0negpitopi  26005  tangtx  26007  tanabsge  26008  sinq12ge0  26010  sinq34lt0t  26011  cosq14ge0  26013  sincos4thpi  26015  sincos6thpi  26017  pige3ALT  26021  sineq0  26025  cosordlem  26031  cosord  26032  cos0pilt1  26033  cos11  26034  sinord  26035  recosf1o  26036  resinf1o  26037  tanord1  26038  tanord  26039  tanregt0  26040  efif1olem4  26046  efifo  26048  relogrn  26062  log1  26086  logneg  26088  argregt0  26110  argrege0  26111  argimgt0  26112  logneg2  26115  logdivlti  26120  logdivlt  26121  ellogdm  26139  logdmn0  26140  logdmnrp  26141  logcnlem3  26144  dvloglem  26148  logdmopn  26149  logf1o2  26150  dvlog2lem  26152  efopnlem1  26156  logtayl  26160  recxpcl  26175  cxpge0  26183  cxple2  26197  cxple2a  26199  cxpsqrtlem  26202  cxpcn3  26246  cxpaddlelem  26249  cxpaddle  26250  loglesqrt  26256  logbrec  26277  ang180lem3  26306  ang180lem4  26307  asinneg  26381  asin1  26389  reasinsin  26391  acosbnd  26395  atan0  26403  atanrecl  26406  atanlogaddlem  26408  atanlogsublem  26410  atanlogsub  26411  atantan  26418  atanbnd  26421  atan1  26423  atans2  26426  ressatans  26429  log2cnv  26439  log2tlbnd  26440  log2ub  26444  log2le1  26445  rlimcnp  26460  rlimcnp2  26461  o1cxp  26469  jensen  26483  amgm  26485  emgt0  26501  harmonicbnd3  26502  harmoniclbnd  26503  harmonicbnd4  26505  zetacvg  26509  eldmgm  26516  lgamgulmlem2  26524  basellem3  26577  basellem8  26582  efnnfsumcl  26597  ppisval  26598  vmage0  26615  chpge0  26620  efchtdvds  26653  ppiltx  26671  ppiub  26697  chpeq0  26701  chteq0  26702  chtleppi  26703  chpchtsum  26712  chpub  26713  dchr1re  26756  bcmono  26770  efexple  26774  bposlem1  26777  bposlem4  26780  bposlem5  26781  bposlem7  26783  bposlem8  26784  bposlem9  26785  lgsval2lem  26800  lgsval4a  26812  lgsneg  26814  lgsdilem  26817  lgsdir2lem1  26818  2lgsoddprmlem3a  26903  2lgsoddprmlem3b  26904  2lgsoddprmlem3c  26905  2lgsoddprmlem3d  26906  rplogsumlem2  26978  rpvmasumlem  26980  dchrisum0flblem1  27001  dchrisum0flblem2  27002  dchrisum0fno1  27004  rplogsum  27020  logdivsum  27026  mulog2sumlem2  27028  selberg2lem  27043  logdivbnd  27049  pntrsumo1  27058  pntrlog2bndlem4  27073  pntrlog2bndlem5  27074  pntpbnd1  27079  pntpbnd2  27080  pntlem3  27102  pntleml  27104  ostth2  27130  trgcgrg  27756  ttgcontlem1  28132  axlowdimlem1  28190  axlowdimlem6  28195  axlowdimlem7  28196  axlowdimlem10  28199  axlowdim1  28207  axlowdim2  28208  axlowdim  28209  elntg2  28233  umgrislfupgrlem  28372  lfgrnloop  28375  lfuhgr1v0e  28501  usgrexmplef  28506  pthdlem2  29015  crctcshwlkn0lem7  29060  rusgrnumwwlks  29218  clwwlkn0  29271  konigsberg  29500  ex-po  29678  ex-sqrt  29697  ex-gcd  29700  nvz0  29909  0blo  30033  nmlno0lem  30034  nmblolbii  30040  siilem2  30093  minvecolem2  30116  minvecolem3  30117  minvecolem4c  30120  minvecolem4  30121  minvecolem5  30122  minvecolem7  30124  htthlem  30158  hiidge0  30339  normlem6  30356  normgt0  30368  norm-i  30370  normpyc  30387  bcsiALT  30420  pjhthlem1  30632  pjneli  30964  nmlnop0iALT  31236  unopbd  31256  nmbdoplbi  31265  nmcoplbi  31269  nmbdfnlbi  31290  nmbdfnlb  31291  nmcfnlbi  31293  cnlnadjlem7  31314  nmopcoi  31336  branmfn  31346  leopmul  31375  nmopleid  31380  pjbdlni  31390  pjnormssi  31409  stle0i  31480  cdj3lem1  31675  xaddeq0  31954  pr01ssre  32018  dp20u  32032  dp20h  32033  dp2clq  32035  dp2lt10  32038  dp2lt  32039  dp0u  32055  dplti  32059  dpexpp1  32062  xdiv0  32083  xrge0slmod  32452  unitdivcld  32870  sqsscirc1  32877  xrge0iifcnv  32902  xrge0iifiso  32904  rezh  32940  indf  33002  indfval  33003  esumcvgsum  33075  voliune  33216  volfiniune  33217  sibfinima  33327  sitmcl  33339  0rrv  33439  coinfliprv  33470  ballotlem2  33476  ballotlem4  33486  ballotlemi1  33490  ballotlemic  33494  sgnclre  33527  sgnnbi  33533  sgnpbi  33534  plymulx0  33547  signsply0  33551  signswch  33561  signstf  33566  signstf0  33568  signstfveq0  33577  signlem0  33587  signshf  33588  itgexpif  33607  hgt750lemd  33649  hgt750lem  33652  hgt750lem2  33653  hgt750leme  33659  iisconn  34232  iillysconn  34233  cvmliftlem10  34274  fz0n  34689  logi  34693  bcneg1  34695  gg-iihalf1cn  35156  gg-reparphti  35161  nn0prpwlem  35196  dnizeq0  35340  dnizphlfeqhlf  35341  knoppndvlem13  35389  cnndvlem1  35402  bj-pinftyccb  36091  bj-minftyccb  36095  bj-pinftynminfty  36097  taupilemrplb  36190  irrdiff  36196  sin2h  36467  tan2h  36469  ptrecube  36477  poimirlem16  36493  poimirlem17  36494  poimirlem20  36497  poimirlem22  36499  poimirlem23  36500  poimirlem29  36506  poimirlem31  36508  poimir  36510  heicant  36512  mblfinlem2  36515  ismblfin  36518  ovoliunnfl  36519  voliunnfl  36521  volsupnfl  36522  mbfposadd  36524  itg2addnclem  36528  itg2addnclem2  36529  ibladdnclem  36533  itgaddnclem2  36536  iblabsnclem  36540  iblmulc2nc  36542  itgmulc2nclem2  36544  itgabsnc  36546  ftc1cnnclem  36548  ftc1anclem5  36554  ftc1anclem8  36557  asindmre  36560  dvasin  36561  areacirclem4  36568  areacirc  36570  isbnd3  36641  ssbnd  36645  prdsbnd  36650  bfplem2  36680  bfp  36681  renegclALT  37822  2xp3dxp2ge1d  41011  factwoffsmonot  41012  0cnALT3  41172  sn-1ne2  41177  oexpreposd  41208  sn-00idlem2  41269  sn-00idlem3  41270  sn-00id  41271  sn-0tie0  41309  sn-ltaddpos  41311  sn-ltaddneg  41312  relt0neg1  41314  sn-nnne0  41318  reelznn0nn  41319  sn-0lt1  41332  sn-inelr  41335  itrere  41336  retire  41337  pellexlem6  41558  elpell14qr2  41586  oddcomabszz  41669  zindbi  41671  jm2.24  41688  acongeq  41708  arearect  41950  areaquad  41951  reabsifneg  42369  reabsifnpos  42370  reabsifpos  42371  reabsifnneg  42372  imsqrtvalex  42383  relexp01min  42450  imo72b2lem0  42903  imo72b2lem2  42905  imo72b2lem1  42907  imo72b2  42910  dvconstbi  43079  binomcxplemnn0  43094  binomcxplemdvbinom  43098  binomcxplemcvg  43099  binomcxplemnotnn0  43101  sineq0ALT  43684  halffl  43993  ren0  44099  rexanuz2nf  44190  sqrlearg  44253  limsup10ex  44476  dvnmptdivc  44641  dvnmul  44646  itgsin0pilem1  44653  itgsinexplem1  44657  itgsinexp  44658  iblempty  44668  stoweidlem17  44720  stoweidlem36  44739  stoweidlem55  44758  wallispilem1  44768  wallispilem2  44769  wallispilem4  44771  stirlinglem4  44780  stirlinglem13  44789  stirlinglem14  44790  stirlinglem15  44791  stirlingr  44793  dirker2re  44795  dirkerdenne0  44796  dirkerre  44798  dirkertrigeqlem1  44801  dirkercncflem2  44807  dirkercncflem4  44809  fourierdlem11  44821  fourierdlem16  44826  fourierdlem21  44831  fourierdlem22  44832  fourierdlem41  44851  fourierdlem42  44852  fourierdlem48  44857  fourierdlem62  44871  fourierdlem66  44875  fourierdlem79  44888  fourierdlem83  44892  fourierdlem94  44903  fourierdlem102  44911  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fourierdlem112  44921  fourierdlem113  44922  fourierdlem114  44923  sqwvfoura  44931  sqwvfourb  44932  fourierswlem  44933  fouriersw  44934  etransclem23  44960  etransclem44  44981  etransclem46  44983  salexct3  45045  salgensscntex  45047  sge0rnn0  45071  sge00  45079  0ome  45232  ovn0lem  45268  ovnhoilem1  45304  smfmullem1  45494  smfmullem2  45495  smfmullem3  45496  smfmullem4  45497  zm1nn  45997  sqrtnegnre  46002  m1mod0mod1  46024  fmtnoprmfac2lem1  46221  31prm  46252  mod42tp1mod8  46257  nfermltl2rev  46398  tgblthelfgott  46470  altgsumbcALT  46983  expnegico01  47153  dignnld  47243  eenglngeehlnmlem1  47377  line2ylem  47391  line2y  47395  itsclc0yqsollem2  47403  icccldii  47505  i0oii  47506  sepfsepc  47514  ex-gt  47727