Theorem 0re 11152

Description: The number 0 is real. Remark: the first step could also be ax-icn 11103. See also 0reALT 11495. (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 11102	. 2 ⊢ 1 ∈ ℂ
2		cnre 11147	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11115	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11127	. . . . . . 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 7369  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045  ici 11046   + caddc 11047   · cmul 11049

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 11102  ax-addrcl 11105  ax-rnegex 11115  ax-cnre 11117

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  11153  0xr  11197  axmulgt0  11224  ne0gt0  11255  00id  11325  mul02lem1  11326  mul02lem2  11327  mul02  11328  addrid  11330  ltaddneg  11366  addgt0  11640  addgegt0  11641  addgtge0  11642  addge0  11643  ltaddpos  11644  ltneg  11654  leneg  11657  lt0neg1  11660  lt0neg2  11661  le0neg1  11662  le0neg2  11663  addge01  11664  suble0  11668  mulge0  11672  msqge0  11675  0le1  11677  relin01  11678  gt0ne0i  11689  lt0ne0d  11719  elimge0  11997  ltm1  12000  recgt0  12004  prodgt0  12005  lemul1a  12012  ltmul12a  12014  lemul12a  12016  mulgt1OLD  12017  gt0div  12025  ge0div  12026  mulge0b  12029  lediv12a  12052  recgt1i  12056  recreclt  12058  ledivp1  12061  squeeze0  12062  recgt0ii  12065  ledivp1i  12084  ltdivp1i  12085  fimaxre2  12104  inelr  12152  crne0  12155  nnge1  12190  nngt0  12193  nnnle0  12195  nnne0  12196  nnrecgt0  12205  0le0  12263  halfge0  12374  nn0ssre  12422  nn0ge0  12443  nn0nlt0  12444  nn0le0eq0  12446  0mnnnnn0  12450  elnnnn0b  12462  elnnnn0c  12463  nn0sub  12468  elnnz  12515  0z  12516  elnn0z  12518  elnnz1  12535  recnz  12585  gtndiv  12587  fnn0ind  12609  10re  12644  rpge0  12941  rpneg  12961  0nrp  12964  0ltpnf  13058  mnflt0  13061  qsqueeze  13137  xneg0  13148  xaddrid  13177  xnn0xadd0  13183  xmulpnf1  13210  xlemul1a  13224  xadddi  13231  xrsupsslem  13243  xrinfmsslem  13244  elrege0  13391  0e0icopnf  13395  elicc01  13403  0elunit  13406  unitssre  13436  0nelfz1  13480  fzpreddisj  13510  fz0to4untppr  13567  fz0to5un2tp  13568  nn0p1elfzo  13639  ico01fl0  13757  rpsup  13804  modelico  13819  0mod  13840  1mod  13841  le2sq2  14076  expubnd  14119  sqlecan  14150  bernneq2  14171  expnbnd  14173  expnlbnd  14174  expmulnbnd  14176  discr1  14180  discr  14181  faclbnd  14231  faclbnd3  14233  faclbnd6  14240  bcval4  14248  bcval5  14259  bcpasc  14262  hasheq0  14304  hashneq0  14305  hashnn0n0nn  14332  hashgt12el  14363  hashgt12el2  14364  hashge2el2dif  14421  lsw0  14506  swrdccatin2  14670  pfxccatin12lem3  14673  reim0  15060  re0  15094  im0  15095  rei  15098  imi  15099  cj0  15100  sqeqd  15108  rennim  15181  cnpart  15182  sqrt0  15183  01sqrexlem4  15187  resqrex  15192  sqrtgt0  15200  sqrt00  15205  sqrtneglem  15208  sqrt9  15215  sqrt2gt1lt2  15216  leabs  15241  absor  15242  max0add  15252  eqsqrt2d  15311  sqrtpclii  15325  rlimconst  15486  rlimrege0  15521  lo1mul  15570  iserge0  15603  fsum00  15740  isumless  15787  arisum2  15803  georeclim  15814  geo2sum  15815  geoisumr  15820  0.999...  15823  cvgrat  15825  fprodge0  15935  bpoly4  16001  cos0  16094  ef01bndlem  16128  sin01bnd  16129  cos01bnd  16130  cos2bnd  16132  sin01gt0  16134  cos01gt0  16135  sincos2sgn  16138  sin4lt0  16139  absef  16141  absefib  16142  efieq1re  16143  epos  16151  rpnnen2lem2  16159  rpnnen2lem3  16160  rpnnen2lem4  16161  rpnnen2lem9  16166  ruclem6  16179  dvdslelem  16255  divalglem1  16340  divalglem5  16343  divalglem6  16344  flodddiv4  16361  sadcadd  16404  gcdn0gt0  16464  nn0seqcvgd  16516  algcvgblem  16523  algcvga  16525  pythagtriplem12  16773  pythagtriplem13  16774  pythagtriplem14  16775  pythagtriplem16  16777  prmreclem4  16866  prmreclem5  16867  prmreclem6  16868  1arith  16874  ramz  16972  mulgnegnn  18992  subgmulg  19048  srgbinomlem4  20114  isabvd  20697  abvtrivd  20717  xrs1mnd  21297  xrs10  21298  rge0srg  21331  psgnodpmr  21475  re0g  21497  psrbaglesupp  21807  psdmvr  22032  mnfnei  23084  imasdsf1olem  24237  ssblps  24286  ssbl  24287  xmeter  24297  dscmet  24436  dscopn  24437  nmoi  24592  nmoeq0  24600  0nghm  24605  idnghm  24607  cnbl0  24637  xrsxmet  24674  metdseq0  24719  iicmp  24755  iiconn  24756  iihalf1  24801  iihalf1cnOLD  24803  elii1  24807  icopnfcnv  24816  icopnfhmeo  24817  iccpnfcnv  24818  xrhmeo  24820  xrhmph  24821  htpycc  24855  reparphti  24872  reparphtiOLD  24873  pcoval1  24889  pco0  24890  pcoval2  24892  pcocn  24893  pcohtpylem  24895  pcopt  24898  pcopt2  24899  pcoass  24900  pcorevlem  24902  reust  25257  recusp  25258  rrx0el  25274  minveclem4c  25301  minveclem2  25302  minveclem3b  25304  minveclem4  25308  minveclem7  25311  pjthlem1  25313  cniccbdd  25338  ovolunnul  25377  ovoliunnul  25384  ovolicc1  25393  ovolre  25402  iccvolcl  25444  ovolioo  25445  ioovolcl  25447  ioorcl  25454  vitalilem4  25488  vitalilem5  25489  vitali  25490  ismbf  25505  mbfmulc2lem  25524  mbfpos  25528  mbfposr  25529  i1f0  25564  i1f1  25567  itg1addlem2  25574  itg1addlem4  25576  itg1addlem5  25577  mbfi1fseqlem4  25595  mbfi1fseqlem5  25596  mbfi1flimlem  25599  xrge0f  25608  itg2ge0  25612  itg2const  25617  itg2mulc  25624  itg2splitlem  25625  itg2gt0  25637  itg2cnlem1  25638  ibl0  25664  iblrelem  25668  iblposlem  25669  iblpos  25670  iblre  25671  itgreval  25674  itgneg  25681  iblss  25682  i1fibl  25685  itgitg1  25686  itgle  25687  itgeqa  25691  itgless  25694  iblconst  25695  itgconst  25696  ibladdlem  25697  itgaddlem2  25701  iblabslem  25705  iblabsr  25707  iblmulc2  25708  itgmulc2lem2  25710  itgabs  25712  itgsplit  25713  bddmulibl  25716  dvferm1  25865  dvferm2  25867  dvferm  25868  dvlip  25874  c1lip1  25878  dveq0  25881  dv11cn  25882  dvne0  25892  ftc1lem4  25922  ply1divex  26018  dgrco  26157  plyrecj  26163  vieta1lem2  26195  aalioulem2  26217  aalioulem3  26218  pserulm  26307  psercnlem2  26310  psercnlem1  26311  psercn  26312  abelth  26327  reeff1olem  26332  reeff1o  26333  pilem2  26338  pilem3  26339  pipos  26344  sinhalfpilem  26348  sincosq1sgn  26383  sincosq2sgn  26384  coseq00topi  26387  coseq0negpitopi  26388  tangtx  26390  tanabsge  26391  sinq12ge0  26393  sinq34lt0t  26394  cosq14ge0  26396  sincos4thpi  26398  sincos6thpi  26401  pige3ALT  26405  sineq0  26409  cosordlem  26415  cosord  26416  cos0pilt1  26417  cos11  26418  sinord  26419  recosf1o  26420  resinf1o  26421  tanord1  26422  tanord  26423  tanregt0  26424  efif1olem4  26430  efifo  26432  relogrn  26446  log1  26470  logi  26472  logneg  26473  argregt0  26495  argrege0  26496  argimgt0  26497  logneg2  26500  logdivlti  26505  logdivlt  26506  ellogdm  26524  logdmn0  26525  logdmnrp  26526  logcnlem3  26529  dvloglem  26533  logdmopn  26534  logf1o2  26535  dvlog2lem  26537  efopnlem1  26541  logtayl  26545  recxpcl  26560  cxpge0  26568  cxple2  26582  cxple2a  26584  cxpsqrtlem  26587  cxpcn3  26634  cxpaddlelem  26637  cxpaddle  26638  loglesqrt  26647  logbrec  26668  ang180lem3  26697  ang180lem4  26698  asinneg  26772  asin1  26780  reasinsin  26782  acosbnd  26786  atan0  26794  atanrecl  26797  atanlogaddlem  26799  atanlogsublem  26801  atanlogsub  26802  atantan  26809  atanbnd  26812  atan1  26814  atans2  26817  ressatans  26820  log2cnv  26830  log2tlbnd  26831  log2ub  26835  log2le1  26836  rlimcnp  26851  rlimcnp2  26852  o1cxp  26861  jensen  26875  amgm  26877  emgt0  26893  harmonicbnd3  26894  harmoniclbnd  26895  harmonicbnd4  26897  zetacvg  26901  eldmgm  26908  lgamgulmlem2  26916  basellem3  26969  basellem8  26974  efnnfsumcl  26989  ppisval  26990  vmage0  27007  chpge0  27012  efchtdvds  27045  ppiltx  27063  ppiub  27091  chpeq0  27095  chteq0  27096  chtleppi  27097  chpchtsum  27106  chpub  27107  dchr1re  27150  bcmono  27164  efexple  27168  bposlem1  27171  bposlem4  27174  bposlem5  27175  bposlem7  27177  bposlem8  27178  bposlem9  27179  lgsval2lem  27194  lgsval4a  27206  lgsneg  27208  lgsdilem  27211  lgsdir2lem1  27212  2lgsoddprmlem3a  27297  2lgsoddprmlem3b  27298  2lgsoddprmlem3c  27299  2lgsoddprmlem3d  27300  rplogsumlem2  27372  rpvmasumlem  27374  dchrisum0flblem1  27395  dchrisum0flblem2  27396  dchrisum0fno1  27398  rplogsum  27414  logdivsum  27420  mulog2sumlem2  27422  selberg2lem  27437  logdivbnd  27443  pntrsumo1  27452  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  pntpbnd1  27473  pntpbnd2  27474  pntlem3  27496  pntleml  27498  ostth2  27524  trgcgrg  28418  ttgcontlem1  28788  axlowdimlem1  28845  axlowdimlem6  28850  axlowdimlem7  28851  axlowdimlem10  28854  axlowdim1  28862  axlowdim2  28863  axlowdim  28864  elntg2  28888  umgrislfupgrlem  29025  lfgrnloop  29028  lfuhgr1v0e  29157  usgrexmplef  29162  pthdlem2  29671  crctcshwlkn0lem7  29719  rusgrnumwwlks  29877  clwwlkn0  29930  konigsberg  30159  ex-po  30337  ex-sqrt  30356  ex-gcd  30359  nvz0  30570  0blo  30694  nmlno0lem  30695  nmblolbii  30701  siilem2  30754  minvecolem2  30777  minvecolem3  30778  minvecolem4c  30781  minvecolem4  30782  minvecolem5  30783  minvecolem7  30785  htthlem  30819  hiidge0  31000  normlem6  31017  normgt0  31029  norm-i  31031  normpyc  31048  bcsiALT  31081  pjhthlem1  31293  pjneli  31625  nmlnop0iALT  31897  unopbd  31917  nmbdoplbi  31926  nmcoplbi  31930  nmbdfnlbi  31951  nmbdfnlb  31952  nmcfnlbi  31954  cnlnadjlem7  31975  nmopcoi  31997  branmfn  32007  leopmul  32036  nmopleid  32041  pjbdlni  32051  pjnormssi  32070  stle0i  32141  cdj3lem1  32336  xaddeq0  32649  expgt0b  32714  pr01ssre  32722  sgnclre  32730  sgnnbi  32736  sgnpbi  32737  indf  32751  indfval  32752  dp20u  32771  dp20h  32772  dp2clq  32774  dp2lt10  32777  dp2lt  32778  dp0u  32794  dplti  32798  dpexpp1  32801  xdiv0  32822  chnub  32911  xrge0slmod  33292  evl1deg3  33520  fldext2chn  33691  cos9thpiminplylem1  33745  unitdivcld  33864  sqsscirc1  33871  xrge0iifcnv  33896  xrge0iifiso  33898  rezh  33932  esumcvgsum  34051  voliune  34192  volfiniune  34193  sibfinima  34303  sitmcl  34315  0rrv  34415  coinfliprv  34447  ballotlem2  34453  ballotlem4  34463  ballotlemi1  34467  ballotlemic  34471  plymulx0  34511  signsply0  34515  signswch  34525  signstf  34530  signstf0  34532  signstfveq0  34541  signlem0  34551  signshf  34552  itgexpif  34570  hgt750lemd  34612  hgt750lem  34615  hgt750lem2  34616  hgt750leme  34622  iisconn  35212  iillysconn  35213  cvmliftlem10  35254  fz0n  35691  bcneg1  35696  nn0prpwlem  36283  dnizeq0  36436  dnizphlfeqhlf  36437  knoppndvlem13  36485  cnndvlem1  36498  bj-pinftyccb  37182  bj-minftyccb  37186  bj-pinftynminfty  37188  taupilemrplb  37281  irrdiff  37287  sin2h  37577  tan2h  37579  ptrecube  37587  poimirlem16  37603  poimirlem17  37604  poimirlem20  37607  poimirlem22  37609  poimirlem23  37610  poimirlem29  37616  poimirlem31  37618  poimir  37620  heicant  37622  mblfinlem2  37625  ismblfin  37628  ovoliunnfl  37629  voliunnfl  37631  volsupnfl  37632  mbfposadd  37634  itg2addnclem  37638  itg2addnclem2  37639  ibladdnclem  37643  itgaddnclem2  37646  iblabsnclem  37650  iblmulc2nc  37652  itgmulc2nclem2  37654  itgabsnc  37656  ftc1cnnclem  37658  ftc1anclem5  37664  ftc1anclem8  37667  asindmre  37670  dvasin  37671  areacirclem4  37678  areacirc  37680  isbnd3  37751  ssbnd  37755  prdsbnd  37760  bfplem2  37790  bfp  37791  renegclALT  38929  0cnALT3  42214  sn-1ne2  42226  itrere  42279  oexpreposd  42283  tan3rdpi  42313  asin1half  42318  readvrec2  42322  sn-00idlem2  42360  sn-00idlem3  42361  sn-00id  42362  sn-0tie0  42412  sn-ltaddpos  42414  sn-ltaddneg  42415  relt0neg1  42417  sn-nnne0  42421  reelznn0nn  42422  sn-0lt1  42436  sn-inelr  42448  sn-itrere  42449  sn-retire  42450  pellexlem6  42795  elpell14qr2  42823  oddcomabszz  42906  zindbi  42908  jm2.24  42925  acongeq  42945  arearect  43177  areaquad  43178  reabsifneg  43594  reabsifnpos  43595  reabsifpos  43596  reabsifnneg  43597  imsqrtvalex  43608  relexp01min  43675  imo72b2lem2  44129  imo72b2lem1  44131  imo72b2  44134  dvconstbi  44296  binomcxplemnn0  44311  binomcxplemdvbinom  44315  binomcxplemcvg  44316  binomcxplemnotnn0  44318  sineq0ALT  44899  halffl  45267  ren0  45371  rexanuz2nf  45461  sqrlearg  45524  limsup10ex  45744  dvnmptdivc  45909  dvnmul  45914  itgsin0pilem1  45921  itgsinexplem1  45925  itgsinexp  45926  iblempty  45936  stoweidlem17  45988  stoweidlem36  46007  stoweidlem55  46026  wallispilem1  46036  wallispilem2  46037  wallispilem4  46039  stirlinglem4  46048  stirlinglem13  46057  stirlinglem14  46058  stirlinglem15  46059  stirlingr  46061  dirker2re  46063  dirkerdenne0  46064  dirkerre  46066  dirkertrigeqlem1  46069  dirkercncflem2  46075  dirkercncflem4  46077  fourierdlem11  46089  fourierdlem16  46094  fourierdlem21  46099  fourierdlem22  46100  fourierdlem41  46119  fourierdlem42  46120  fourierdlem48  46125  fourierdlem62  46139  fourierdlem66  46143  fourierdlem79  46156  fourierdlem83  46160  fourierdlem94  46171  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem111  46188  fourierdlem112  46189  fourierdlem113  46190  fourierdlem114  46191  sqwvfoura  46199  sqwvfourb  46200  fourierswlem  46201  fouriersw  46202  etransclem23  46228  etransclem44  46249  etransclem46  46251  salexct3  46313  salgensscntex  46315  sge0rnn0  46339  sge00  46347  0ome  46500  ovn0lem  46536  ovnhoilem1  46572  smfmullem1  46762  smfmullem2  46763  smfmullem3  46764  smfmullem4  46765  squeezedltsq  46860  zm1nn  47276  sqrtnegnre  47281  m1mod0mod1  47328  fmtnoprmfac2lem1  47540  31prm  47571  mod42tp1mod8  47576  nfermltl2rev  47717  tgblthelfgott  47789  usgrexmpl1lem  47985  usgrexmpl2lem  47990  usgrexmpl2nb0  47995  usgrexmpl2nb5  48000  usgrexmpl2trifr  48001  gpgusgralem  48020  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  altgsumbcALT  48314  expnegico01  48480  dignnld  48565  eenglngeehlnmlem1  48699  line2ylem  48713  line2y  48717  itsclc0yqsollem2  48725  icccldii  48880  i0oii  48881  sepfsepc  48889  ex-gt  49690