Theorem 0re 11310

Description: The number 0 is real. Remark: the first step could also be ax-icn 11259. See also 0reALT 11655. (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 11258	. 2 ⊢ 1 ∈ ℂ
2		cnre 11305	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11271	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11283	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2849	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 248	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3164	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 16	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 486	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3156	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3087  (class class class)co 7420  ℂcc 11198  ℝcr 11199  0cc0 11200  1c1 11201  ici 11202   + caddc 11203   · cmul 11205

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-addrcl 11261  ax-rnegex 11271  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-rex 3088

This theorem is used by:  0red  11311  pr01ssre  11312  0xr  11356  axmulgt0  11384  ne0gt0  11415  00id  11485  mul02lem1  11486  mul02lem2  11487  mul02  11488  addrid  11490  ltaddneg  11526  addgt0  11802  addgegt0  11803  addgtge0  11804  addge0  11805  ltaddpos  11806  ltneg  11816  leneg  11819  lt0neg1  11822  lt0neg2  11823  le0neg1  11824  le0neg2  11825  addge01  11826  suble0  11830  mulge0  11834  msqge0  11837  0le1  11839  relin01  11840  gt0ne0i  11851  lt0ne0d  11881  elimge0  12156  ltm1  12159  recgt0  12163  prodgt0  12164  lemul1a  12171  ltmul12a  12173  lemul12a  12175  gt0div  12183  ge0div  12184  mulge0b  12187  lediv12a  12210  recgt1i  12214  recreclt  12216  ledivp1  12219  squeeze0  12220  recgt0ii  12223  ledivp1i  12242  ltdivp1i  12243  fimaxre2  12262  inelr  12310  crne0  12313  indf  12326  indfval  12327  nnge1  12366  nngt0  12369  nnnle0  12371  nnne0  12372  nnrecgt0  12381  0le0  12444  0le2  12445  halfge0  12562  nn0ssre  12610  nn0ge0  12631  nn0nlt0  12632  nn0le0eq0  12634  0mnnnnn0  12638  elnnnn0b  12650  elnnnn0c  12651  nn0sub  12656  elnnz  12703  0z  12704  elnn0z  12706  elnnz1  12722  recnz  12774  gtndiv  12776  fnn0ind  12798  10re  12837  rpge0  13134  rpneg  13154  0nrp  13157  0ltpnf  13251  mnflt0  13254  qsqueeze  13331  xneg0  13342  xaddrid  13371  xnn0xadd0  13377  xmulpnf1  13404  xlemul1a  13418  xadddi  13425  xrsupsslem  13437  xrinfmsslem  13438  elrege0  13585  0e0icopnf  13589  elicc01  13597  0elunit  13600  unitssre  13630  nnge2recico01  13638  0nelfz1  13676  fzpreddisj  13707  fz0to4untppr  13764  fz0to5un2tp  13765  nn0p1elfzo  13837  ico01fl0  13959  rpsup  14006  modelico  14021  0mod  14042  1mod  14043  le2sq2  14278  expubnd  14321  sqlecan  14353  bernneq2  14374  expnbnd  14376  expnlbnd  14377  expmulnbnd  14379  discr1  14383  discr  14384  faclbnd  14434  faclbnd3  14436  faclbnd6  14443  bcval4  14451  bcval5  14462  bcpasc  14465  hasheq0  14507  hashneq0  14508  hashnn0n0nn  14535  hashgt12el  14567  hashgt12el2  14568  hashge2el2dif  14625  lsw0  14710  swrdccatin2  14878  pfxccatin12lem3  14881  sgnclre  15255  sgnnbi  15257  sgnpbi  15258  reim0  15285  re0  15319  im0  15320  rei  15323  imi  15324  cj0  15325  sqeqd  15333  rennim  15406  cnpart  15407  sqrt0  15408  01sqrexlem4  15412  resqrex  15417  sqrtgt0  15425  sqrt00  15430  sqrtneglem  15433  sqrt9  15440  sqrt2gt1lt2  15441  leabs  15466  absor  15467  max0add  15477  eqsqrt2d  15536  sqrtpclii  15550  rlimconst  15711  rlimrege0  15746  lo1mul  15795  iserge0  15828  fsum00  15965  isumless  16014  arisum2  16030  georeclim  16041  geo2sum  16042  geoisumr  16047  0.999...  16050  cvgrat  16052  fprodge0  16160  bpoly4  16225  cos0  16318  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  cos2bnd  16356  sin01gt0  16358  cos01gt0  16359  sincos2sgn  16362  sin4lt0  16363  absef  16365  absefib  16366  efieq1re  16367  epos  16375  rpnnen2lem2  16383  rpnnen2lem3  16384  rpnnen2lem4  16385  rpnnen2lem9  16390  ruclem6  16403  dvdslelem  16479  divalglem1  16564  divalglem5  16567  divalglem6  16568  flodddiv4  16585  sadcadd  16628  gcdn0gt0  16690  nn0seqcvgd  16745  algcvgblem  16752  algcvga  16754  pythagtriplem12  17004  pythagtriplem13  17005  pythagtriplem14  17006  pythagtriplem16  17008  prmreclem4  17097  prmreclem5  17098  prmreclem6  17099  1arith  17105  ramz  17203  chnub  18796  mulgnegnn  19294  subgmulg  19351  srgbinomlem4  20455  isabvd  21069  abvtrivd  21089  rge0srg  21744  xrs1mnd  21746  xrs10  21747  psgnodpmr  21896  re0g  21918  psrbaglesupp  22230  psdmvr  22490  mnfnei  23539  imasdsf1olem  24692  ssblps  24741  ssbl  24742  xmeter  24752  dscmet  24891  dscopn  24892  nmoi  25047  nmoeq0  25055  0nghm  25060  idnghm  25062  cnbl0  25092  xrsxmet  25129  metdseq0  25174  iicmp  25207  iiconn  25208  iihalf1  25252  elii1  25256  icopnfcnv  25263  icopnfhmeo  25264  iccpnfcnv  25265  xrhmeo  25267  xrhmph  25268  htpycc  25301  reparphti  25318  pcoval1  25334  pco0  25335  pcoval2  25337  pcocn  25338  pcohtpylem  25340  pcopt  25343  pcopt2  25344  pcoass  25345  pcorevlem  25347  reust  25702  recusp  25703  rrx0el  25719  minveclem4c  25746  minveclem2  25747  minveclem3b  25749  minveclem4  25753  minveclem7  25756  pjthlem1  25758  cniccbdd  25782  ovolunnul  25821  ovoliunnul  25828  ovolicc1  25837  ovolre  25846  iccvolcl  25888  ovolioo  25889  ioovolcl  25891  ioorcl  25898  vitalilem4  25932  vitalilem5  25933  vitali  25934  ismbf  25949  mbfmulc2lem  25968  mbfpos  25972  mbfposr  25973  i1f0  26008  i1f1  26011  itg1addlem2  26018  itg1addlem4  26020  itg1addlem5  26021  mbfi1fseqlem4  26039  mbfi1fseqlem5  26040  mbfi1flimlem  26043  xrge0f  26052  itg2ge0  26056  itg2const  26061  itg2mulc  26068  itg2splitlem  26069  itg2gt0  26081  itg2cnlem1  26082  ibl0  26107  iblrelem  26111  iblposlem  26112  iblpos  26113  iblre  26114  itgreval  26117  itgneg  26124  iblss  26125  i1fibl  26128  itgitg1  26129  itgle  26130  itgeqa  26134  itgless  26137  iblconst  26138  itgconst  26139  ibladdlem  26140  itgaddlem2  26144  iblabslem  26148  iblabsr  26150  iblmulc2  26151  itgmulc2lem2  26153  itgabs  26155  itgsplit  26156  bddmulibl  26159  dvferm1  26305  dvferm2  26307  dvferm  26308  dvlip  26313  c1lip1  26317  dveq0  26320  dv11cn  26321  dvne0  26331  ftc1lem4  26359  ply1divex  26455  dgrco  26594  plyrecj  26598  plyn0mulidp  26602  vieta1lem2  26634  aalioulem2  26660  aalioulem3  26661  pserulm  26749  psercnlem2  26751  psercnlem1  26752  psercn  26753  abelth  26768  reeff1olem  26773  reeff1o  26774  pilem2  26779  pilem3  26780  pipos  26787  pige0  26788  sinhalfpilem  26792  sincosq1sgn  26827  sincosq2sgn  26828  coseq00topi  26831  coseq0negpitopi  26832  tangtx  26834  tanabsge  26835  sinq12ge0  26837  sinq34lt0t  26838  cosq14ge0  26840  sincos4thpi  26842  sincos6thpi  26844  pige3ALT  26848  sineq0  26852  cosordlem  26858  cosord  26859  cos0pilt1  26860  cos11  26861  sinord  26862  recosf1o  26863  resinf1o  26864  tanord1  26865  tanord  26866  tanregt0  26867  efif1olem4  26873  efifo  26875  relogrn  26889  log1  26913  logi  26915  logneg  26916  argregt0  26938  argrege0  26939  argimgt0  26940  logneg2  26943  logdivlti  26948  logdivlt  26949  ellogdm  26967  logdmn0  26968  logdmnrp  26969  logcnlem3  26972  dvloglem  26976  logdmopn  26977  logf1o2  26978  dvlog2lem  26980  efopnlem1  26984  logtayl  26988  recxpcl  27003  cxpge0  27011  cxple2  27025  cxple2a  27027  cxpsqrtlem  27030  cxpcn3  27076  cxpaddlelem  27079  cxpaddle  27080  loglesqrt  27089  logbrec  27110  ang180lem3  27139  ang180lem4  27140  asinneg  27214  asin1  27222  reasinsin  27224  acosbnd  27228  atan0  27236  atanrecl  27239  atanlogaddlem  27241  atanlogsublem  27243  atanlogsub  27244  atantan  27251  atanbnd  27254  atan1  27256  atans2  27259  ressatans  27262  log2cnv  27272  log2tlbnd  27273  log2ub  27277  log2le1  27278  rlimcnp  27293  rlimcnp2  27294  o1cxp  27302  jensen  27316  amgm  27318  emgt0  27334  harmonicbnd3  27335  harmoniclbnd  27336  harmonicbnd4  27338  zetacvg  27342  eldmgm  27349  lgamgulmlem2  27357  basellem3  27410  basellem8  27415  efnnfsumcl  27430  ppisval  27431  vmage0  27448  chpge0  27453  efchtdvds  27486  ppiltx  27504  ppiub  27531  chpeq0  27535  chteq0  27536  chtleppi  27537  chpchtsum  27546  chpub  27547  dchr1re  27590  bcmono  27604  efexple  27608  bposlem1  27611  bposlem4  27614  bposlem5  27615  bposlem7  27617  bposlem8  27618  bposlem9  27619  lgsval2lem  27634  lgsval4a  27646  lgsneg  27648  lgsdilem  27651  lgsdir2lem1  27652  2lgsoddprmlem3a  27737  2lgsoddprmlem3b  27738  2lgsoddprmlem3c  27739  2lgsoddprmlem3d  27740  rplogsumlem2  27812  rpvmasumlem  27814  dchrisum0flblem1  27835  dchrisum0flblem2  27836  dchrisum0fno1  27838  rplogsum  27854  logdivsum  27860  mulog2sumlem2  27862  selberg2lem  27877  logdivbnd  27883  pntrsumo1  27892  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntpbnd1  27913  pntpbnd2  27914  pntlem3  27936  pntleml  27938  ostth2  27964  trgcgrg  28978  ttgcontlem1  29462  axlowdimlem1  29520  axlowdimlem6  29525  axlowdimlem7  29526  axlowdimlem10  29529  axlowdim1  29537  axlowdim2  29538  axlowdim  29539  elntg2  29563  umgrislfupgrlem  29700  lfgrnloop  29703  lfuhgr1v0e  29835  usgrexmplef  29840  pthdlem2  30354  crctcshwlkn0lem7  30405  rusgrnumwwlks  30566  clwwlkn0  30619  konigsberg  30858  ex-po  31036  ex-sqrt  31055  ex-gcd  31058  nvz0  31270  0blo  31394  nmlno0lem  31395  nmblolbii  31401  siilem2  31454  minvecolem2  31477  minvecolem3  31478  minvecolem4c  31481  minvecolem4  31482  minvecolem5  31483  minvecolem7  31485  htthlem  31519  hiidge0  31700  normlem6  31717  normgt0  31729  norm-i  31731  normpyc  31748  bcsiALT  31781  pjhthlem1  31993  pjneli  32325  nmlnop0iALT  32597  unopbd  32617  nmbdoplbi  32626  nmcoplbi  32630  nmbdfnlbi  32651  nmbdfnlb  32652  nmcfnlbi  32654  cnlnadjlem7  32675  nmopcoi  32697  branmfn  32707  leopmul  32736  nmopleid  32741  pjbdlni  32751  pjnormssi  32770  stle0i  32841  cdj3lem1  33036  xaddeq0  33345  expgt0b  33408  dp20u  33444  dp20h  33445  dp2clq  33447  dp2lt10  33450  dp2lt  33451  dp0u  33467  dplti  33471  dpexpp1  33474  xdiv0  33495  xrge0slmod  33909  evl1deg3  34110  fldext2chn  34360  cos9thpiminplylem1  34414  unitdivcld  34533  sqsscirc1  34540  xrge0iifcnv  34565  xrge0iifiso  34567  rezh  34601  esumcvgsum  34720  voliune  34862  volfiniune  34863  sibfinima  34971  sitmcl  34983  0rrv  35083  coinfliprv  35115  ballotlem2  35121  ballotlem4  35131  ballotlemi1  35135  ballotlemic  35139  signsply0  35180  signswch  35190  signstf  35195  signstf0  35197  signstfveq0  35206  signlem0  35216  signshf  35217  itgexpif  35235  hgt750lemd  35277  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  iisconn  36017  iillysconn  36018  cvmliftlem10  36059  fz0n  36496  bcneg1  36501  nn0prpwlem  37110  dnizeq0  37341  dnizphlfeqhlf  37342  knoppndvlem13  37390  cnndvlem1  37403  bj-pinftyccb  38142  bj-minftyccb  38146  bj-pinftynminfty  38148  taupilemrplb  38241  irrdiff  38247  sin2h  38533  tan2h  38535  ptrecube  38538  poimirlem16  38554  poimirlem17  38555  poimirlem20  38558  poimirlem22  38560  poimirlem23  38561  poimirlem29  38567  poimirlem31  38569  poimir  38571  heicant  38573  mblfinlem2  38576  ismblfin  38579  ovoliunnfl  38580  voliunnfl  38582  volsupnfl  38583  mbfposadd  38585  itg2addnclem  38589  itg2addnclem2  38590  ibladdnclem  38594  itgaddnclem2  38597  iblabsnclem  38601  iblmulc2nc  38603  itgmulc2nclem2  38605  itgabsnc  38607  ftc1cnnclem  38609  ftc1anclem5  38615  ftc1anclem8  38618  asindmre  38621  dvasin  38622  areacirclem4  38629  areacirc  38631  isbnd3  38718  ssbnd  38722  prdsbnd  38727  bfplem2  38757  bfp  38758  renegclALT  40020  0cnALT3  43304  sn-1ne2  43330  itrere  43375  oexpreposd  43379  tan3rdpi  43403  asin1half  43408  readvrec2  43412  sn-00idlem2  43450  sn-00idlem3  43451  sn-00id  43452  sn-0tie0  43515  sn-ltaddpos  43517  sn-ltaddneg  43518  relt0neg1  43520  sn-nnne0  43524  reelznn0nn  43525  sn-0lt1  43539  sn-inelr  43551  sn-itrere  43552  sn-retire  43553  pellexlem6  43840  elpell14qr2  43868  oddcomabszz  43950  zindbi  43952  jm2.24  43969  acongeq  43989  arearect  44216  areaquad  44217  reabsifneg  44631  reabsifnpos  44632  reabsifpos  44633  reabsifnneg  44634  imsqrtvalex  44645  relexp01min  44712  imo72b2lem2  45166  imo72b2lem1  45168  imo72b2  45171  dvconstbi  45317  binomcxplemnn0  45332  binomcxplemdvbinom  45336  binomcxplemcvg  45337  binomcxplemnotnn0  45339  sineq0ALT  45918  halffl  46311  ren0  46411  rexanuz2nf  46501  sqrlearg  46564  limsup10ex  46782  dvnmptdivc  46947  dvnmul  46952  itgsin0pilem1  46959  itgsinexplem1  46963  itgsinexp  46964  iblempty  46974  stoweidlem17  47026  stoweidlem36  47045  stoweidlem55  47064  wallispilem1  47074  wallispilem2  47075  wallispilem4  47077  stirlinglem4  47086  stirlinglem13  47095  stirlinglem14  47096  stirlingr  47099  dirker2re  47101  dirkerdenne0  47102  dirkerre  47104  dirkertrigeqlem1  47107  dirkercncflem2  47113  dirkercncflem4  47115  fourierdlem11  47127  fourierdlem16  47132  fourierdlem21  47137  fourierdlem22  47138  fourierdlem41  47157  fourierdlem42  47158  fourierdlem62  47177  fourierdlem66  47181  fourierdlem79  47194  fourierdlem83  47198  fourierdlem94  47209  fourierdlem102  47217  fourierdlem103  47218  fourierdlem104  47219  fourierdlem111  47226  fourierdlem112  47227  fourierdlem113  47228  fourierdlem114  47229  sqwvfoura  47237  sqwvfourb  47238  fourierswlem  47239  fouriersw  47240  etransclem23  47266  etransclem44  47287  etransclem46  47289  salexct3  47351  salgensscntex  47353  sge0rnn0  47377  sge00  47385  0ome  47538  ovn0lem  47574  ovnhoilem1  47610  smfmullem1  47800  smfmullem2  47801  smfmullem3  47802  smfmullem4  47803  squeezedltsq  47911  goldrapos  47929  goldratval  47935  zm1nn  48371  sqrtnegnre  48376  flmrecm1  48412  m1mod0mod1  48429  muldvdsfacgt  48455  fmtnoprmfac2lem1  48650  31prm  48681  mod42tp1mod8  48686  nfermltl2rev  48840  tgblthelfgott  48912  usgrexmpl1lem  49118  usgrexmpl2lem  49123  usgrexmpl2nb0  49128  usgrexmpl2nb5  49133  usgrexmpl2trifr  49134  gpgusgralem  49153  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  gpg5edgnedg  49227  altgsumbcALT  49464  expnegico01  49629  dignnld  49714  eenglngeehlnmlem1  49848  line2ylem  49862  line2y  49866  itsclc0yqsollem2  49874  icccldii  50026  i0oii  50027  sepfsepc  50035  ex-gt  50820