Theorem 0re 11146

Description: The number 0 is real. Remark: the first step could also be ax-icn 11097. See also 0reALT 11491. (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 2824	. . . . . . 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 7367  ℂ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 2708  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 2728  df-clel 2811  df-rex 3062

This theorem is referenced by:  0red  11147  pr01ssre  11148  0xr  11192  axmulgt0  11220  ne0gt0  11251  00id  11321  mul02lem1  11322  mul02lem2  11323  mul02  11324  addrid  11326  ltaddneg  11362  addgt0  11636  addgegt0  11637  addgtge0  11638  addge0  11639  ltaddpos  11640  ltneg  11650  leneg  11653  lt0neg1  11656  lt0neg2  11657  le0neg1  11658  le0neg2  11659  addge01  11660  suble0  11664  mulge0  11668  msqge0  11671  0le1  11673  relin01  11674  gt0ne0i  11685  lt0ne0d  11715  elimge0  11994  ltm1  11997  recgt0  12001  prodgt0  12002  lemul1a  12009  ltmul12a  12011  lemul12a  12013  mulgt1OLD  12014  gt0div  12022  ge0div  12023  mulge0b  12026  lediv12a  12049  recgt1i  12053  recreclt  12055  ledivp1  12058  squeeze0  12059  recgt0ii  12062  ledivp1i  12081  ltdivp1i  12082  fimaxre2  12101  inelr  12149  crne0  12152  indf  12165  indfval  12166  nnge1  12205  nngt0  12208  nnnle0  12210  nnne0  12211  nnrecgt0  12220  0le0  12282  halfge0  12393  nn0ssre  12441  nn0ge0  12462  nn0nlt0  12463  nn0le0eq0  12465  0mnnnnn0  12469  elnnnn0b  12481  elnnnn0c  12482  nn0sub  12487  elnnz  12534  0z  12535  elnn0z  12537  elnnz1  12553  recnz  12604  gtndiv  12606  fnn0ind  12628  10re  12663  rpge0  12956  rpneg  12976  0nrp  12979  0ltpnf  13073  mnflt0  13076  qsqueeze  13153  xneg0  13164  xaddrid  13193  xnn0xadd0  13199  xmulpnf1  13226  xlemul1a  13240  xadddi  13247  xrsupsslem  13259  xrinfmsslem  13260  elrege0  13407  0e0icopnf  13411  elicc01  13419  0elunit  13422  unitssre  13452  nnge2recico01  13460  0nelfz1  13497  fzpreddisj  13527  fz0to4untppr  13584  fz0to5un2tp  13585  nn0p1elfzo  13657  ico01fl0  13778  rpsup  13825  modelico  13840  0mod  13861  1mod  13862  le2sq2  14097  expubnd  14140  sqlecan  14171  bernneq2  14192  expnbnd  14194  expnlbnd  14195  expmulnbnd  14197  discr1  14201  discr  14202  faclbnd  14252  faclbnd3  14254  faclbnd6  14261  bcval4  14269  bcval5  14280  bcpasc  14283  hasheq0  14325  hashneq0  14326  hashnn0n0nn  14353  hashgt12el  14384  hashgt12el2  14385  hashge2el2dif  14442  lsw0  14527  swrdccatin2  14691  pfxccatin12lem3  14694  reim0  15080  re0  15114  im0  15115  rei  15118  imi  15119  cj0  15120  sqeqd  15128  rennim  15201  cnpart  15202  sqrt0  15203  01sqrexlem4  15207  resqrex  15212  sqrtgt0  15220  sqrt00  15225  sqrtneglem  15228  sqrt9  15235  sqrt2gt1lt2  15236  leabs  15261  absor  15262  max0add  15272  eqsqrt2d  15331  sqrtpclii  15345  rlimconst  15506  rlimrege0  15541  lo1mul  15590  iserge0  15623  fsum00  15761  isumless  15810  arisum2  15826  georeclim  15837  geo2sum  15838  geoisumr  15843  0.999...  15846  cvgrat  15848  fprodge0  15958  bpoly4  16024  cos0  16117  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  cos2bnd  16155  sin01gt0  16157  cos01gt0  16158  sincos2sgn  16161  sin4lt0  16162  absef  16164  absefib  16165  efieq1re  16166  epos  16174  rpnnen2lem2  16182  rpnnen2lem3  16183  rpnnen2lem4  16184  rpnnen2lem9  16189  ruclem6  16202  dvdslelem  16278  divalglem1  16363  divalglem5  16366  divalglem6  16367  flodddiv4  16384  sadcadd  16427  gcdn0gt0  16487  nn0seqcvgd  16539  algcvgblem  16546  algcvga  16548  pythagtriplem12  16797  pythagtriplem13  16798  pythagtriplem14  16799  pythagtriplem16  16801  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  1arith  16898  ramz  16996  chnub  18588  mulgnegnn  19060  subgmulg  19116  srgbinomlem4  20210  isabvd  20789  abvtrivd  20809  rge0srg  21418  xrs1mnd  21420  xrs10  21421  psgnodpmr  21570  re0g  21592  psrbaglesupp  21902  psdmvr  22135  mnfnei  23186  imasdsf1olem  24338  ssblps  24387  ssbl  24388  xmeter  24398  dscmet  24537  dscopn  24538  nmoi  24693  nmoeq0  24701  0nghm  24706  idnghm  24708  cnbl0  24738  xrsxmet  24775  metdseq0  24820  iicmp  24853  iiconn  24854  iihalf1  24898  elii1  24902  icopnfcnv  24909  icopnfhmeo  24910  iccpnfcnv  24911  xrhmeo  24913  xrhmph  24914  htpycc  24947  reparphti  24964  pcoval1  24980  pco0  24981  pcoval2  24983  pcocn  24984  pcohtpylem  24986  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  reust  25348  recusp  25349  rrx0el  25365  minveclem4c  25392  minveclem2  25393  minveclem3b  25395  minveclem4  25399  minveclem7  25402  pjthlem1  25404  cniccbdd  25428  ovolunnul  25467  ovoliunnul  25474  ovolicc1  25483  ovolre  25492  iccvolcl  25534  ovolioo  25535  ioovolcl  25537  ioorcl  25544  vitalilem4  25578  vitalilem5  25579  vitali  25580  ismbf  25595  mbfmulc2lem  25614  mbfpos  25618  mbfposr  25619  i1f0  25654  i1f1  25657  itg1addlem2  25664  itg1addlem4  25666  itg1addlem5  25667  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1flimlem  25689  xrge0f  25698  itg2ge0  25702  itg2const  25707  itg2mulc  25714  itg2splitlem  25715  itg2gt0  25727  itg2cnlem1  25728  ibl0  25754  iblrelem  25758  iblposlem  25759  iblpos  25760  iblre  25761  itgreval  25764  itgneg  25771  iblss  25772  i1fibl  25775  itgitg1  25776  itgle  25777  itgeqa  25781  itgless  25784  iblconst  25785  itgconst  25786  ibladdlem  25787  itgaddlem2  25791  iblabslem  25795  iblabsr  25797  iblmulc2  25798  itgmulc2lem2  25800  itgabs  25802  itgsplit  25803  bddmulibl  25806  dvferm1  25952  dvferm2  25954  dvferm  25955  dvlip  25960  c1lip1  25964  dveq0  25967  dv11cn  25968  dvne0  25978  ftc1lem4  26006  ply1divex  26102  dgrco  26240  plyrecj  26246  vieta1lem2  26277  aalioulem2  26299  aalioulem3  26300  pserulm  26387  psercnlem2  26389  psercnlem1  26390  psercn  26391  abelth  26406  reeff1olem  26411  reeff1o  26412  pilem2  26417  pilem3  26418  pipos  26423  sinhalfpilem  26427  sincosq1sgn  26462  sincosq2sgn  26463  coseq00topi  26466  coseq0negpitopi  26467  tangtx  26469  tanabsge  26470  sinq12ge0  26472  sinq34lt0t  26473  cosq14ge0  26475  sincos4thpi  26477  sincos6thpi  26480  pige3ALT  26484  sineq0  26488  cosordlem  26494  cosord  26495  cos0pilt1  26496  cos11  26497  sinord  26498  recosf1o  26499  resinf1o  26500  tanord1  26501  tanord  26502  tanregt0  26503  efif1olem4  26509  efifo  26511  relogrn  26525  log1  26549  logi  26551  logneg  26552  argregt0  26574  argrege0  26575  argimgt0  26576  logneg2  26579  logdivlti  26584  logdivlt  26585  ellogdm  26603  logdmn0  26604  logdmnrp  26605  logcnlem3  26608  dvloglem  26612  logdmopn  26613  logf1o2  26614  dvlog2lem  26616  efopnlem1  26620  logtayl  26624  recxpcl  26639  cxpge0  26647  cxple2  26661  cxple2a  26663  cxpsqrtlem  26666  cxpcn3  26712  cxpaddlelem  26715  cxpaddle  26716  loglesqrt  26725  logbrec  26746  ang180lem3  26775  ang180lem4  26776  asinneg  26850  asin1  26858  reasinsin  26860  acosbnd  26864  atan0  26872  atanrecl  26875  atanlogaddlem  26877  atanlogsublem  26879  atanlogsub  26880  atantan  26887  atanbnd  26890  atan1  26892  atans2  26895  ressatans  26898  log2cnv  26908  log2tlbnd  26909  log2ub  26913  log2le1  26914  rlimcnp  26929  rlimcnp2  26930  o1cxp  26938  jensen  26952  amgm  26954  emgt0  26970  harmonicbnd3  26971  harmoniclbnd  26972  harmonicbnd4  26974  zetacvg  26978  eldmgm  26985  lgamgulmlem2  26993  basellem3  27046  basellem8  27051  efnnfsumcl  27066  ppisval  27067  vmage0  27084  chpge0  27089  efchtdvds  27122  ppiltx  27140  ppiub  27167  chpeq0  27171  chteq0  27172  chtleppi  27173  chpchtsum  27182  chpub  27183  dchr1re  27226  bcmono  27240  efexple  27244  bposlem1  27247  bposlem4  27250  bposlem5  27251  bposlem7  27253  bposlem8  27254  bposlem9  27255  lgsval2lem  27270  lgsval4a  27282  lgsneg  27284  lgsdilem  27287  lgsdir2lem1  27288  2lgsoddprmlem3a  27373  2lgsoddprmlem3b  27374  2lgsoddprmlem3c  27375  2lgsoddprmlem3d  27376  rplogsumlem2  27448  rpvmasumlem  27450  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0fno1  27474  rplogsum  27490  logdivsum  27496  mulog2sumlem2  27498  selberg2lem  27513  logdivbnd  27519  pntrsumo1  27528  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntpbnd1  27549  pntpbnd2  27550  pntlem3  27572  pntleml  27574  ostth2  27600  trgcgrg  28583  ttgcontlem1  28953  axlowdimlem1  29011  axlowdimlem6  29016  axlowdimlem7  29017  axlowdimlem10  29020  axlowdim1  29028  axlowdim2  29029  axlowdim  29030  elntg2  29054  umgrislfupgrlem  29191  lfgrnloop  29194  lfuhgr1v0e  29323  usgrexmplef  29328  pthdlem2  29836  crctcshwlkn0lem7  29884  rusgrnumwwlks  30045  clwwlkn0  30098  konigsberg  30327  ex-po  30505  ex-sqrt  30524  ex-gcd  30527  nvz0  30739  0blo  30863  nmlno0lem  30864  nmblolbii  30870  siilem2  30923  minvecolem2  30946  minvecolem3  30947  minvecolem4c  30950  minvecolem4  30951  minvecolem5  30952  minvecolem7  30954  htthlem  30988  hiidge0  31169  normlem6  31186  normgt0  31198  norm-i  31200  normpyc  31217  bcsiALT  31250  pjhthlem1  31462  pjneli  31794  nmlnop0iALT  32066  unopbd  32086  nmbdoplbi  32095  nmcoplbi  32099  nmbdfnlbi  32120  nmbdfnlb  32121  nmcfnlbi  32123  cnlnadjlem7  32144  nmopcoi  32166  branmfn  32176  leopmul  32205  nmopleid  32210  pjbdlni  32220  pjnormssi  32239  stle0i  32310  cdj3lem1  32505  xaddeq0  32826  expgt0b  32890  sgnclre  32905  sgnnbi  32911  sgnpbi  32912  dp20u  32937  dp20h  32938  dp2clq  32940  dp2lt10  32943  dp2lt  32944  dp0u  32960  dplti  32964  dpexpp1  32967  xdiv0  32988  xrge0slmod  33408  evl1deg3  33638  fldext2chn  33872  cos9thpiminplylem1  33926  unitdivcld  34045  sqsscirc1  34052  xrge0iifcnv  34077  xrge0iifiso  34079  rezh  34113  esumcvgsum  34232  voliune  34373  volfiniune  34374  sibfinima  34483  sitmcl  34495  0rrv  34595  coinfliprv  34627  ballotlem2  34633  ballotlem4  34643  ballotlemi1  34647  ballotlemic  34651  plymulx0  34691  signsply0  34695  signswch  34705  signstf  34710  signstf0  34712  signstfveq0  34721  signlem0  34731  signshf  34732  itgexpif  34750  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  iisconn  35434  iillysconn  35435  cvmliftlem10  35476  fz0n  35913  bcneg1  35918  nn0prpwlem  36504  dnizeq0  36735  dnizphlfeqhlf  36736  knoppndvlem13  36784  cnndvlem1  36797  bj-pinftyccb  37535  bj-minftyccb  37539  bj-pinftynminfty  37541  taupilemrplb  37634  irrdiff  37640  sin2h  37931  tan2h  37933  ptrecube  37941  poimirlem16  37957  poimirlem17  37958  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem29  37970  poimirlem31  37972  poimir  37974  heicant  37976  mblfinlem2  37979  ismblfin  37982  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  mbfposadd  37988  itg2addnclem  37992  itg2addnclem2  37993  ibladdnclem  37997  itgaddnclem2  38000  iblabsnclem  38004  iblmulc2nc  38006  itgmulc2nclem2  38008  itgabsnc  38010  ftc1cnnclem  38012  ftc1anclem5  38018  ftc1anclem8  38021  asindmre  38024  dvasin  38025  areacirclem4  38032  areacirc  38034  isbnd3  38105  ssbnd  38109  prdsbnd  38114  bfplem2  38144  bfp  38145  renegclALT  39409  0cnALT3  42692  sn-1ne2  42703  itrere  42750  oexpreposd  42754  tan3rdpi  42784  asin1half  42789  readvrec2  42793  sn-00idlem2  42831  sn-00idlem3  42832  sn-00id  42833  sn-0tie0  42896  sn-ltaddpos  42898  sn-ltaddneg  42899  relt0neg1  42901  sn-nnne0  42905  reelznn0nn  42906  sn-0lt1  42920  sn-inelr  42932  sn-itrere  42933  sn-retire  42934  pellexlem6  43262  elpell14qr2  43290  oddcomabszz  43372  zindbi  43374  jm2.24  43391  acongeq  43411  arearect  43643  areaquad  43644  reabsifneg  44059  reabsifnpos  44060  reabsifpos  44061  reabsifnneg  44062  imsqrtvalex  44073  relexp01min  44140  imo72b2lem2  44594  imo72b2lem1  44596  imo72b2  44599  dvconstbi  44761  binomcxplemnn0  44776  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemnotnn0  44783  sineq0ALT  45363  halffl  45729  ren0  45830  rexanuz2nf  45920  sqrlearg  45983  limsup10ex  46201  dvnmptdivc  46366  dvnmul  46371  itgsin0pilem1  46378  itgsinexplem1  46382  itgsinexp  46383  iblempty  46393  stoweidlem17  46445  stoweidlem36  46464  stoweidlem55  46483  wallispilem1  46493  wallispilem2  46494  wallispilem4  46496  stirlinglem4  46505  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  stirlingr  46518  dirker2re  46520  dirkerdenne0  46521  dirkerre  46523  dirkertrigeqlem1  46526  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem11  46546  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem62  46596  fourierdlem66  46600  fourierdlem79  46613  fourierdlem83  46617  fourierdlem94  46628  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fourierdlem114  46648  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  etransclem23  46685  etransclem44  46706  etransclem46  46708  salexct3  46770  salgensscntex  46772  sge0rnn0  46796  sge00  46804  0ome  46957  ovn0lem  46993  ovnhoilem1  47029  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  smfmullem4  47222  squeezedltsq  47318  goldrapos  47331  zm1nn  47750  sqrtnegnre  47755  flmrecm1  47791  m1mod0mod1  47808  muldvdsfacgt  47834  fmtnoprmfac2lem1  48029  31prm  48060  mod42tp1mod8  48065  nfermltl2rev  48219  tgblthelfgott  48291  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  gpgusgralem  48532  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  gpg5edgnedg  48606  altgsumbcALT  48829  expnegico01  48994  dignnld  49079  eenglngeehlnmlem1  49213  line2ylem  49227  line2y  49231  itsclc0yqsollem2  49239  icccldii  49394  i0oii  49395  sepfsepc  49403  ex-gt  50203