Theorem 0re 11349

Description: The number 0 is real. Remark: the first step could also be ax-icn 11298. See also 0reALT 11694. (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 11297	. 2 ⊢ 1 ∈ ℂ
2		cnre 11344	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11310	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11322	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2852	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 248	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3167	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 16	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 486	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3159	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  (class class class)co 7451  ℂcc 11237  ℝcr 11238  0cc0 11239  1c1 11240  ici 11241   + caddc 11242   · cmul 11244

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addrcl 11300  ax-rnegex 11310  ax-cnre 11312

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-rex 3091

This theorem is used by:  0red  11350  pr01ssre  11351  0xr  11395  axmulgt0  11423  ne0gt0  11454  00id  11524  mul02lem1  11525  mul02lem2  11526  mul02  11527  addrid  11529  ltaddneg  11565  addgt0  11842  addgegt0  11843  addgtge0  11844  addge0  11845  ltaddpos  11846  ltneg  11856  leneg  11859  lt0neg1  11862  lt0neg2  11863  le0neg1  11864  le0neg2  11865  addge01  11866  suble0  11870  mulge0  11874  msqge0  11877  0le1  11879  relin01  11880  gt0ne0i  11891  lt0ne0d  11921  elimge0  12196  ltm1  12199  recgt0  12203  prodgt0  12204  lemul1a  12211  ltmul12a  12213  lemul12a  12215  gt0div  12223  ge0div  12224  mulge0b  12227  lediv12a  12250  recgt1i  12254  recreclt  12256  ledivp1  12259  squeeze0  12260  recgt0ii  12263  ledivp1i  12282  ltdivp1i  12283  fimaxre2  12302  inelr  12350  crne0  12353  indf  12366  indfval  12367  nnge1  12406  nngt0  12409  nnnle0  12411  nnne0  12412  nnrecgt0  12421  0le0  12484  0le2  12485  halfge0  12602  nn0ssre  12650  nn0ge0  12671  nn0nlt0  12672  nn0le0eq0  12674  0mnnnnn0  12678  elnnnn0b  12690  elnnnn0c  12691  nn0sub  12696  elnnz  12743  0z  12744  elnn0z  12746  elnnz1  12762  recnz  12814  gtndiv  12816  fnn0ind  12838  10re  12877  rpge0  13174  rpneg  13194  0nrp  13197  0ltpnf  13291  mnflt0  13294  qsqueeze  13371  xneg0  13382  xaddrid  13411  xnn0xadd0  13417  xmulpnf1  13444  xlemul1a  13458  xadddi  13465  xrsupsslem  13477  xrinfmsslem  13478  elrege0  13625  0e0icopnf  13629  elicc01  13637  0elunit  13640  unitssre  13670  nnge2recico01  13678  0nelfz1  13716  fzpreddisj  13747  fz0to4untppr  13804  fz0to5un2tp  13805  nn0p1elfzo  13877  ico01fl0  13999  rpsup  14046  modelico  14061  0mod  14082  1mod  14083  le2sq2  14318  expubnd  14361  sqlecan  14393  bernneq2  14415  expnbnd  14417  expnlbnd  14418  expmulnbnd  14420  discr1  14424  discr  14425  faclbnd  14475  faclbnd3  14477  faclbnd6  14484  bcval4  14492  bcval5  14503  bcpasc  14506  hasheq0  14548  hashneq0  14549  hashnn0n0nn  14576  hashgt12el  14608  hashgt12el2  14609  hashge2el2dif  14666  lsw0  14751  swrdccatin2  14920  pfxccatin12lem3  14923  sgnclre  15298  sgnnbi  15300  sgnpbi  15301  reim0  15328  re0  15362  im0  15363  rei  15366  imi  15367  cj0  15368  sqeqd  15376  rennim  15449  cnpart  15450  sqrt0  15451  01sqrexlem4  15455  resqrex  15460  sqrtgt0  15468  sqrt00  15473  sqrtneglem  15476  sqrt9  15483  sqrt2gt1lt2  15484  leabs  15509  absor  15510  max0add  15520  eqsqrt2d  15580  sqrtpclii  15594  rlimconst  15755  rlimrege0  15790  lo1mul  15839  iserge0  15872  fsum00  16009  isumless  16058  georeclim  16085  geo2sum  16086  geoisumr  16091  0.999...  16094  cvgrat  16096  fprodge0  16204  bpoly4  16269  cos0  16362  ef01bndlem  16396  sin01bnd  16397  cos01bnd  16398  cos2bnd  16400  sin01gt0  16402  cos01gt0  16403  sincos2sgn  16406  sin4lt0  16407  absef  16409  absefib  16410  efieq1re  16411  epos  16419  rpnnen2lem2  16427  rpnnen2lem3  16428  rpnnen2lem4  16429  rpnnen2lem9  16434  ruclem6  16447  dvdslelem  16523  divalglem1  16608  divalglem5  16611  divalglem6  16612  flodddiv4  16629  sadcadd  16672  gcdn0gt0  16734  nn0seqcvgd  16789  algcvgblem  16796  algcvga  16798  pythagtriplem12  17048  pythagtriplem13  17049  pythagtriplem14  17050  pythagtriplem16  17052  prmreclem4  17141  prmreclem5  17142  prmreclem6  17143  1arith  17149  ramz  17247  chnub  18846  mulgnegnn  19344  subgmulg  19401  srgbinomlem4  20506  isabvd  21120  abvtrivd  21140  rge0srg  21798  xrs1mnd  21800  xrs10  21801  psgnodpmr  21951  re0g  21973  psrbaglesupp  22285  psdmvr  22545  mnfnei  23594  imasdsf1olem  24747  ssblps  24796  ssbl  24797  xmeter  24807  dscmet  24946  dscopn  24947  nmoi  25102  nmoeq0  25110  0nghm  25115  idnghm  25117  cnbl0  25147  xrsxmet  25184  metdseq0  25229  iicmp  25262  iiconn  25263  iihalf1  25307  elii1  25311  icopnfcnv  25318  icopnfhmeo  25319  iccpnfcnv  25320  xrhmeo  25322  xrhmph  25323  htpycc  25356  reparphti  25373  pcoval1  25389  pco0  25390  pcoval2  25392  pcocn  25393  pcohtpylem  25395  pcopt  25398  pcopt2  25399  pcoass  25400  pcorevlem  25402  reust  25757  recusp  25758  rrx0el  25774  minveclem4c  25801  minveclem2  25802  minveclem3b  25804  minveclem4  25808  minveclem7  25811  pjthlem1  25813  cniccbdd  25837  ovolunnul  25876  ovoliunnul  25883  ovolicc1  25892  ovolre  25901  iccvolcl  25943  ovolioo  25944  ioovolcl  25946  ioorcl  25953  vitalilem4  25987  vitalilem5  25988  vitali  25989  ismbf  26004  mbfmulc2lem  26023  mbfpos  26027  mbfposr  26028  i1f0  26063  i1f1  26066  itg1addlem2  26073  itg1addlem4  26075  itg1addlem5  26076  mbfi1fseqlem4  26094  mbfi1fseqlem5  26095  mbfi1flimlem  26098  xrge0f  26107  itg2ge0  26111  itg2const  26116  itg2mulc  26123  itg2splitlem  26124  itg2gt0  26136  itg2cnlem1  26137  ibl0  26162  iblrelem  26166  iblposlem  26167  iblpos  26168  iblre  26169  itgreval  26172  itgneg  26179  iblss  26180  i1fibl  26183  itgitg1  26184  itgle  26185  itgeqa  26189  itgless  26192  iblconst  26193  itgconst  26194  ibladdlem  26195  itgaddlem2  26199  iblabslem  26203  iblabsr  26205  iblmulc2  26206  itgmulc2lem2  26208  itgabs  26210  itgsplit  26211  bddmulibl  26214  dvferm1  26360  dvferm2  26362  dvferm  26363  dvlip  26368  c1lip1  26372  dveq0  26375  dv11cn  26376  dvne0  26386  ftc1lem4  26414  ply1divex  26510  dgrco  26649  plyrecj  26653  plyn0mulidp  26657  vieta1lem2  26689  aalioulem2  26717  aalioulem3  26718  pserulm  26806  psercnlem2  26808  psercnlem1  26809  psercn  26810  abelth  26825  reeff1olem  26830  reeff1o  26831  pilem2  26836  pilem3  26837  pipos  26844  pige0  26845  sinhalfpilem  26849  sincosq1sgn  26884  sincosq2sgn  26885  coseq00topi  26888  coseq0negpitopi  26889  tangtx  26891  tanabsge  26892  sinq12ge0  26894  sinq34lt0t  26895  cosq14ge0  26897  sincos4thpi  26899  sincos6thpi  26901  pige3ALT  26905  sineq0  26909  cosordlem  26915  cosord  26916  cos11  26918  sinord  26919  recosf1o  26920  resinf1o  26921  tanord1  26922  tanord  26923  tanregt0  26924  efif1olem4  26930  efifo  26932  relogrn  26946  log1  26970  logi  26972  logneg  26973  argregt0  26995  argrege0  26996  argimgt0  26997  logneg2  27000  logdivlti  27005  logdivlt  27006  ellogdm  27024  logdmn0  27025  logdmnrp  27026  logcnlem3  27029  dvloglem  27033  logdmopn  27034  logf1o2  27035  dvlog2lem  27037  efopnlem1  27041  logtayl  27045  recxpcl  27060  cxpge0  27068  cxple2  27082  cxple2a  27084  cxpsqrtlem  27087  cxpcn3  27133  cxpaddlelem  27136  cxpaddle  27137  loglesqrt  27146  logbrec  27167  ang180lem3  27196  ang180lem4  27197  asinneg  27271  asin1  27279  reasinsin  27281  acosbnd  27285  atan0  27293  atanrecl  27296  atanlogaddlem  27298  atanlogsublem  27300  atanlogsub  27301  atantan  27308  atanbnd  27311  atan1  27313  atans2  27316  ressatans  27319  log2cnv  27329  log2tlbnd  27330  log2ub  27334  log2le1  27335  rlimcnp  27350  rlimcnp2  27351  o1cxp  27359  jensen  27373  amgm  27375  emgt0  27391  harmonicbnd3  27392  harmoniclbnd  27393  harmonicbnd4  27395  zetacvg  27399  eldmgm  27406  lgamgulmlem2  27414  basellem3  27467  basellem8  27472  efnnfsumcl  27487  ppisval  27488  vmage0  27505  chpge0  27510  efchtdvds  27543  ppiltx  27561  ppiub  27588  chpeq0  27592  chteq0  27593  chtleppi  27594  chpchtsum  27603  chpub  27604  dchr1re  27647  bcmono  27661  efexple  27665  bposlem1  27668  bposlem4  27671  bposlem5  27672  bposlem7  27674  bposlem8  27675  bposlem9  27676  lgsval2lem  27691  lgsval4a  27703  lgsneg  27705  lgsdilem  27708  lgsdir2lem1  27709  2lgsoddprmlem3a  27794  2lgsoddprmlem3b  27795  2lgsoddprmlem3c  27796  2lgsoddprmlem3d  27797  rplogsumlem2  27869  rpvmasumlem  27871  dchrisum0flblem1  27892  dchrisum0flblem2  27893  dchrisum0fno1  27895  rplogsum  27911  logdivsum  27917  mulog2sumlem2  27919  selberg2lem  27934  logdivbnd  27940  pntrsumo1  27949  pntrlog2bndlem4  27964  pntrlog2bndlem5  27965  pntpbnd1  27970  pntpbnd2  27971  pntlem3  27993  pntleml  27995  ostth2  28021  trgcgrg  29035  ttgcontlem1  29519  axlowdimlem1  29577  axlowdimlem6  29582  axlowdimlem7  29583  axlowdimlem10  29586  axlowdim1  29594  axlowdim2  29595  axlowdim  29596  elntg2  29620  umgrislfupgrlem  29757  lfgrnloop  29760  lfuhgr1v0e  29892  usgrexmplef  29897  pthdlem2  30411  crctcshwlkn0lem7  30462  rusgrnumwwlks  30623  clwwlkn0  30676  konigsberg  30915  ex-po  31093  ex-sqrt  31112  ex-gcd  31115  nvz0  31327  0blo  31451  nmlno0lem  31452  nmblolbii  31458  siilem2  31511  minvecolem2  31534  minvecolem3  31535  minvecolem4c  31538  minvecolem4  31539  minvecolem5  31540  minvecolem7  31542  htthlem  31576  hiidge0  31757  normlem6  31774  normgt0  31786  norm-i  31788  normpyc  31805  bcsiALT  31838  pjhthlem1  32050  pjneli  32382  nmlnop0iALT  32654  unopbd  32674  nmbdoplbi  32683  nmcoplbi  32687  nmbdfnlbi  32708  nmbdfnlb  32709  nmcfnlbi  32711  cnlnadjlem7  32732  nmopcoi  32754  branmfn  32764  leopmul  32793  nmopleid  32798  pjbdlni  32808  pjnormssi  32827  stle0i  32898  cdj3lem1  33093  xaddeq0  33441  expgt0b  33504  dp20u  33540  dp20h  33541  dp2clq  33543  dp2lt10  33546  dp2lt  33547  dp0u  33563  dplti  33567  dpexpp1  33570  xdiv0  33591  xrge0slmod  34013  evl1deg3  34213  fldext2chn  34471  cos9thpiminplylem1  34525  unitdivcld  34644  sqsscirc1  34651  xrge0iifcnv  34676  xrge0iifiso  34678  rezh  34712  esumcvgsum  34831  voliune  34973  volfiniune  34974  sibfinima  35082  sitmcl  35094  0rrv  35194  coinfliprv  35226  ballotlem2  35232  ballotlem4  35242  ballotlemi1  35246  ballotlemic  35250  signsply0  35291  signswch  35301  signstf  35306  signstf0  35308  signstfveq0  35317  signlem0  35327  signshf  35328  itgexpif  35346  hgt750lemd  35388  hgt750lem  35391  hgt750lem2  35392  hgt750leme  35398  iisconn  36225  iillysconn  36226  cvmliftlem10  36267  fz0n  36711  bcneg1  36716  nn0prpwlem  37325  dnizeq0  37556  dnizphlfeqhlf  37557  knoppndvlem13  37605  cnndvlem1  37618  bj-pinftyccb  38410  bj-minftyccb  38414  bj-pinftynminfty  38416  taupilemrplb  38509  irrdiff  38515  sin2h  38801  tan2h  38803  ptrecube  38806  poimirlem16  38822  poimirlem17  38823  poimirlem20  38826  poimirlem22  38828  poimirlem23  38829  poimirlem29  38835  poimirlem31  38837  poimir  38839  heicant  38841  mblfinlem2  38844  ismblfin  38847  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  mbfposadd  38853  itg2addnclem  38857  itg2addnclem2  38858  ibladdnclem  38862  itgaddnclem2  38865  iblabsnclem  38869  iblmulc2nc  38871  itgmulc2nclem2  38873  itgabsnc  38875  ftc1cnnclem  38877  ftc1anclem5  38883  ftc1anclem8  38886  asindmre  38889  dvasin  38890  areacirclem4  38897  areacirc  38899  isbnd3  38984  ssbnd  38988  prdsbnd  38993  bfplem2  39023  bfp  39024  renegclALT  40286  0cnALT3  43570  sn-1ne2  43596  itrere  43641  oexpreposd  43645  tan3rdpi  43669  asin1half  43674  readvrec2  43678  sn-00idlem2  43716  sn-00idlem3  43717  sn-00id  43718  sn-0tie0  43781  sn-ltaddpos  43783  sn-ltaddneg  43784  relt0neg1  43786  sn-nnne0  43790  reelznn0nn  43791  sn-0lt1  43805  sn-inelr  43817  sn-itrere  43818  sn-retire  43819  pellexlem6  44107  elpell14qr2  44135  oddcomabszz  44217  zindbi  44219  jm2.24  44236  acongeq  44256  arearect  44478  areaquad  44479  reabsifneg  44893  reabsifnpos  44894  reabsifpos  44895  reabsifnneg  44896  imsqrtvalex  44907  relexp01min  44974  imo72b2lem2  45428  imo72b2lem1  45430  imo72b2  45433  dvconstbi  45579  binomcxplemnn0  45594  binomcxplemdvbinom  45598  binomcxplemcvg  45599  binomcxplemnotnn0  45601  sineq0ALT  46179  halffl  46585  ren0  46685  rexanuz2nf  46775  sqrlearg  46838  limsup10ex  47056  dvnmptdivc  47221  dvnmul  47226  itgsin0pilem1  47233  itgsinexplem1  47237  itgsinexp  47238  iblempty  47248  stoweidlem17  47300  stoweidlem36  47319  stoweidlem55  47338  wallispilem1  47348  wallispilem2  47349  wallispilem4  47351  stirlinglem4  47360  stirlinglem13  47369  stirlinglem14  47370  stirlingr  47373  dirker2re  47375  dirkerdenne0  47376  dirkerre  47378  dirkertrigeqlem1  47381  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem11  47401  fourierdlem16  47406  fourierdlem21  47411  fourierdlem22  47412  fourierdlem41  47431  fourierdlem42  47432  fourierdlem62  47451  fourierdlem66  47455  fourierdlem79  47468  fourierdlem83  47472  fourierdlem94  47483  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  fourierdlem112  47501  fourierdlem113  47502  fourierdlem114  47503  sqwvfoura  47511  sqwvfourb  47512  fourierswlem  47513  fouriersw  47514  etransclem23  47540  etransclem44  47561  etransclem46  47563  salexct3  47625  salgensscntex  47627  sge0rnn0  47651  sge00  47659  0ome  47812  ovn0lem  47848  ovnhoilem1  47884  smfmullem1  48074  smfmullem2  48075  smfmullem3  48076  smfmullem4  48077  squeezedltsq  48185  goldrapos  48203  goldratval  48209  zm1nn  48645  sqrtnegnre  48650  flmrecm1  48686  m1mod0mod1  48703  muldvdsfacgt  48729  fmtnoprmfac2lem1  48924  31prm  48955  mod42tp1mod8  48960  nfermltl2rev  49114  tgblthelfgott  49186  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb0  49402  usgrexmpl2nb5  49407  usgrexmpl2trifr  49408  gpgusgralem  49427  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  gpg5edgnedg  49501  altgsumbcALT  49796  expnegico01  49961  dignnld  50046  eenglngeehlnmlem1  50181  2sphere0  50193  line2ylem  50194  line2  50195  line2x  50197  line2y  50198  itsclc0yqsollem2  50206  icccldii  50364  i0oii  50365  sepfsepc  50373  ex-gt  51227