Theorem 0re 11227

Description: The number 0 is real. Remark: the first step could also be ax-icn 11176. See also 0reALT 11572. (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 11175	. 2 ⊢ 1 ∈ ℂ
2		cnre 11222	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11188	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11200	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2853	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 248	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3168	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 16	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 486	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3160	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∃wrex 3091  (class class class)co 7419  ℂcc 11115  ℝcr 11116  0cc0 11117  1c1 11118  ici 11119   + caddc 11120   · cmul 11122

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-addrcl 11178  ax-rnegex 11188  ax-cnre 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-rex 3092

This theorem is used by:  0red  11228  pr01ssre  11229  0xr  11273  axmulgt0  11301  ne0gt0  11332  00id  11402  mul02lem1  11403  mul02lem2  11404  mul02  11405  addrid  11407  ltaddneg  11443  addgt0  11717  addgegt0  11718  addgtge0  11719  addge0  11720  ltaddpos  11721  ltneg  11731  leneg  11734  lt0neg1  11737  lt0neg2  11738  le0neg1  11739  le0neg2  11740  addge01  11741  suble0  11745  mulge0  11749  msqge0  11752  0le1  11754  relin01  11755  gt0ne0i  11766  lt0ne0d  11796  elimge0  12071  ltm1  12074  recgt0  12078  prodgt0  12079  lemul1a  12086  ltmul12a  12088  lemul12a  12090  gt0div  12098  ge0div  12099  mulge0b  12102  lediv12a  12125  recgt1i  12129  recreclt  12131  ledivp1  12134  squeeze0  12135  recgt0ii  12138  ledivp1i  12157  ltdivp1i  12158  fimaxre2  12177  inelr  12225  crne0  12228  indf  12241  indfval  12242  nnge1  12281  nngt0  12284  nnnle0  12286  nnne0  12287  nnrecgt0  12296  0le0  12359  0le2  12360  halfge0  12477  nn0ssre  12525  nn0ge0  12546  nn0nlt0  12547  nn0le0eq0  12549  0mnnnnn0  12553  elnnnn0b  12565  elnnnn0c  12566  nn0sub  12571  elnnz  12618  0z  12619  elnn0z  12621  elnnz1  12637  recnz  12689  gtndiv  12691  fnn0ind  12713  10re  12752  rpge0  13048  rpneg  13068  0nrp  13071  0ltpnf  13165  mnflt0  13168  qsqueeze  13245  xneg0  13256  xaddrid  13285  xnn0xadd0  13291  xmulpnf1  13318  xlemul1a  13332  xadddi  13339  xrsupsslem  13351  xrinfmsslem  13352  elrege0  13499  0e0icopnf  13503  elicc01  13511  0elunit  13514  unitssre  13544  nnge2recico01  13552  0nelfz1  13589  fzpreddisj  13620  fz0to4untppr  13677  fz0to5un2tp  13678  nn0p1elfzo  13750  ico01fl0  13872  rpsup  13919  modelico  13934  0mod  13955  1mod  13956  le2sq2  14191  expubnd  14234  sqlecan  14265  bernneq2  14286  expnbnd  14288  expnlbnd  14289  expmulnbnd  14291  discr1  14295  discr  14296  faclbnd  14346  faclbnd3  14348  faclbnd6  14355  bcval4  14363  bcval5  14374  bcpasc  14377  hasheq0  14419  hashneq0  14420  hashnn0n0nn  14447  hashgt12el  14479  hashgt12el2  14480  hashge2el2dif  14537  lsw0  14622  swrdccatin2  14790  pfxccatin12lem3  14793  sgnclre  15165  sgnnbi  15167  sgnpbi  15168  reim0  15195  re0  15229  im0  15230  rei  15233  imi  15234  cj0  15235  sqeqd  15243  rennim  15316  cnpart  15317  sqrt0  15318  01sqrexlem4  15322  resqrex  15327  sqrtgt0  15335  sqrt00  15340  sqrtneglem  15343  sqrt9  15350  sqrt2gt1lt2  15351  leabs  15376  absor  15377  max0add  15387  eqsqrt2d  15446  sqrtpclii  15460  rlimconst  15621  rlimrege0  15656  lo1mul  15705  iserge0  15738  fsum00  15875  isumless  15924  arisum2  15940  georeclim  15951  geo2sum  15952  geoisumr  15957  0.999...  15960  cvgrat  15962  fprodge0  16072  bpoly4  16137  cos0  16230  ef01bndlem  16264  sin01bnd  16265  cos01bnd  16266  cos2bnd  16268  sin01gt0  16270  cos01gt0  16271  sincos2sgn  16274  sin4lt0  16275  absef  16277  absefib  16278  efieq1re  16279  epos  16287  rpnnen2lem2  16295  rpnnen2lem3  16296  rpnnen2lem4  16297  rpnnen2lem9  16302  ruclem6  16315  dvdslelem  16391  divalglem1  16476  divalglem5  16479  divalglem6  16480  flodddiv4  16497  sadcadd  16540  gcdn0gt0  16600  nn0seqcvgd  16652  algcvgblem  16659  algcvga  16661  pythagtriplem12  16910  pythagtriplem13  16911  pythagtriplem14  16912  pythagtriplem16  16914  prmreclem4  17003  prmreclem5  17004  prmreclem6  17005  1arith  17011  ramz  17109  chnub  18702  mulgnegnn  19196  subgmulg  19253  srgbinomlem4  20357  isabvd  20967  abvtrivd  20987  rge0srg  21640  xrs1mnd  21642  xrs10  21643  psgnodpmr  21792  re0g  21814  psrbaglesupp  22124  psdmvr  22384  mnfnei  23430  imasdsf1olem  24583  ssblps  24632  ssbl  24633  xmeter  24643  dscmet  24782  dscopn  24783  nmoi  24938  nmoeq0  24946  0nghm  24951  idnghm  24953  cnbl0  24983  xrsxmet  25020  metdseq0  25065  iicmp  25098  iiconn  25099  iihalf1  25143  elii1  25147  icopnfcnv  25154  icopnfhmeo  25155  iccpnfcnv  25156  xrhmeo  25158  xrhmph  25159  htpycc  25192  reparphti  25209  pcoval1  25225  pco0  25226  pcoval2  25228  pcocn  25229  pcohtpylem  25231  pcopt  25234  pcopt2  25235  pcoass  25236  pcorevlem  25238  reust  25593  recusp  25594  rrx0el  25610  minveclem4c  25637  minveclem2  25638  minveclem3b  25640  minveclem4  25644  minveclem7  25647  pjthlem1  25649  cniccbdd  25673  ovolunnul  25712  ovoliunnul  25719  ovolicc1  25728  ovolre  25737  iccvolcl  25779  ovolioo  25780  ioovolcl  25782  ioorcl  25789  vitalilem4  25823  vitalilem5  25824  vitali  25825  ismbf  25840  mbfmulc2lem  25859  mbfpos  25863  mbfposr  25864  i1f0  25899  i1f1  25902  itg1addlem2  25909  itg1addlem4  25911  itg1addlem5  25912  mbfi1fseqlem4  25930  mbfi1fseqlem5  25931  mbfi1flimlem  25934  xrge0f  25943  itg2ge0  25947  itg2const  25952  itg2mulc  25959  itg2splitlem  25960  itg2gt0  25972  itg2cnlem1  25973  ibl0  25999  iblrelem  26003  iblposlem  26004  iblpos  26005  iblre  26006  itgreval  26009  itgneg  26016  iblss  26017  i1fibl  26020  itgitg1  26021  itgle  26022  itgeqa  26026  itgless  26029  iblconst  26030  itgconst  26031  ibladdlem  26032  itgaddlem2  26036  iblabslem  26040  iblabsr  26042  iblmulc2  26043  itgmulc2lem2  26045  itgabs  26047  itgsplit  26048  bddmulibl  26051  dvferm1  26197  dvferm2  26199  dvferm  26200  dvlip  26205  c1lip1  26209  dveq0  26212  dv11cn  26213  dvne0  26223  ftc1lem4  26251  ply1divex  26347  dgrco  26485  plyrecj  26491  plyn0mulidp  26495  vieta1lem2  26525  aalioulem2  26549  aalioulem3  26550  pserulm  26638  psercnlem2  26640  psercnlem1  26641  psercn  26642  abelth  26657  reeff1olem  26662  reeff1o  26663  pilem2  26668  pilem3  26669  pipos  26676  pige0  26677  sinhalfpilem  26681  sincosq1sgn  26716  sincosq2sgn  26717  coseq00topi  26720  coseq0negpitopi  26721  tangtx  26723  tanabsge  26724  sinq12ge0  26726  sinq34lt0t  26727  cosq14ge0  26729  sincos4thpi  26731  sincos6thpi  26734  pige3ALT  26738  sineq0  26742  cosordlem  26748  cosord  26749  cos0pilt1  26750  cos11  26751  sinord  26752  recosf1o  26753  resinf1o  26754  tanord1  26755  tanord  26756  tanregt0  26757  efif1olem4  26763  efifo  26765  relogrn  26779  log1  26803  logi  26805  logneg  26806  argregt0  26828  argrege0  26829  argimgt0  26830  logneg2  26833  logdivlti  26838  logdivlt  26839  ellogdm  26857  logdmn0  26858  logdmnrp  26859  logcnlem3  26862  dvloglem  26866  logdmopn  26867  logf1o2  26868  dvlog2lem  26870  efopnlem1  26874  logtayl  26878  recxpcl  26893  cxpge0  26901  cxple2  26915  cxple2a  26917  cxpsqrtlem  26920  cxpcn3  26966  cxpaddlelem  26969  cxpaddle  26970  loglesqrt  26979  logbrec  27000  ang180lem3  27029  ang180lem4  27030  asinneg  27104  asin1  27112  reasinsin  27114  acosbnd  27118  atan0  27126  atanrecl  27129  atanlogaddlem  27131  atanlogsublem  27133  atanlogsub  27134  atantan  27141  atanbnd  27144  atan1  27146  atans2  27149  ressatans  27152  log2cnv  27162  log2tlbnd  27163  log2ub  27167  log2le1  27168  rlimcnp  27183  rlimcnp2  27184  o1cxp  27192  jensen  27206  amgm  27208  emgt0  27224  harmonicbnd3  27225  harmoniclbnd  27226  harmonicbnd4  27228  zetacvg  27232  eldmgm  27239  lgamgulmlem2  27247  basellem3  27300  basellem8  27305  efnnfsumcl  27320  ppisval  27321  vmage0  27338  chpge0  27343  efchtdvds  27376  ppiltx  27394  ppiub  27421  chpeq0  27425  chteq0  27426  chtleppi  27427  chpchtsum  27436  chpub  27437  dchr1re  27480  bcmono  27494  efexple  27498  bposlem1  27501  bposlem4  27504  bposlem5  27505  bposlem7  27507  bposlem8  27508  bposlem9  27509  lgsval2lem  27524  lgsval4a  27536  lgsneg  27538  lgsdilem  27541  lgsdir2lem1  27542  2lgsoddprmlem3a  27627  2lgsoddprmlem3b  27628  2lgsoddprmlem3c  27629  2lgsoddprmlem3d  27630  rplogsumlem2  27702  rpvmasumlem  27704  dchrisum0flblem1  27725  dchrisum0flblem2  27726  dchrisum0fno1  27728  rplogsum  27744  logdivsum  27750  mulog2sumlem2  27752  selberg2lem  27767  logdivbnd  27773  pntrsumo1  27782  pntrlog2bndlem4  27797  pntrlog2bndlem5  27798  pntpbnd1  27803  pntpbnd2  27804  pntlem3  27826  pntleml  27828  ostth2  27854  trgcgrg  28837  ttgcontlem1  29291  axlowdimlem1  29349  axlowdimlem6  29354  axlowdimlem7  29355  axlowdimlem10  29358  axlowdim1  29366  axlowdim2  29367  axlowdim  29368  elntg2  29392  umgrislfupgrlem  29529  lfgrnloop  29532  lfuhgr1v0e  29664  usgrexmplef  29669  pthdlem2  30183  crctcshwlkn0lem7  30234  rusgrnumwwlks  30395  clwwlkn0  30448  konigsberg  30681  ex-po  30859  ex-sqrt  30878  ex-gcd  30881  nvz0  31093  0blo  31217  nmlno0lem  31218  nmblolbii  31224  siilem2  31277  minvecolem2  31300  minvecolem3  31301  minvecolem4c  31304  minvecolem4  31305  minvecolem5  31306  minvecolem7  31308  htthlem  31342  hiidge0  31523  normlem6  31540  normgt0  31552  norm-i  31554  normpyc  31571  bcsiALT  31604  pjhthlem1  31816  pjneli  32148  nmlnop0iALT  32420  unopbd  32440  nmbdoplbi  32449  nmcoplbi  32453  nmbdfnlbi  32474  nmbdfnlb  32475  nmcfnlbi  32477  cnlnadjlem7  32498  nmopcoi  32520  branmfn  32530  leopmul  32559  nmopleid  32564  pjbdlni  32574  pjnormssi  32593  stle0i  32664  cdj3lem1  32859  xaddeq0  33170  expgt0b  33233  dp20u  33269  dp20h  33270  dp2clq  33272  dp2lt10  33275  dp2lt  33276  dp0u  33292  dplti  33296  dpexpp1  33299  xdiv0  33320  xrge0slmod  33734  evl1deg3  33934  fldext2chn  34184  cos9thpiminplylem1  34238  unitdivcld  34357  sqsscirc1  34364  xrge0iifcnv  34389  xrge0iifiso  34391  rezh  34425  esumcvgsum  34544  voliune  34686  volfiniune  34687  sibfinima  34796  sitmcl  34808  0rrv  34908  coinfliprv  34940  ballotlem2  34946  ballotlem4  34956  ballotlemi1  34960  ballotlemic  34964  signsply0  35005  signswch  35015  signstf  35020  signstf0  35022  signstfveq0  35031  signlem0  35041  signshf  35042  itgexpif  35060  hgt750lemd  35102  hgt750lem  35105  hgt750lem2  35106  hgt750leme  35112  iisconn  35783  iillysconn  35784  cvmliftlem10  35825  fz0n  36262  bcneg1  36267  nn0prpwlem  36892  dnizeq0  37123  dnizphlfeqhlf  37124  knoppndvlem13  37172  cnndvlem1  37185  bj-pinftyccb  37924  bj-minftyccb  37928  bj-pinftynminfty  37930  taupilemrplb  38023  irrdiff  38029  sin2h  38320  tan2h  38322  ptrecube  38330  poimirlem16  38346  poimirlem17  38347  poimirlem20  38350  poimirlem22  38352  poimirlem23  38353  poimirlem29  38359  poimirlem31  38361  poimir  38363  heicant  38365  mblfinlem2  38368  ismblfin  38371  ovoliunnfl  38372  voliunnfl  38374  volsupnfl  38375  mbfposadd  38377  itg2addnclem  38381  itg2addnclem2  38382  ibladdnclem  38386  itgaddnclem2  38389  iblabsnclem  38393  iblmulc2nc  38395  itgmulc2nclem2  38397  itgabsnc  38399  ftc1cnnclem  38401  ftc1anclem5  38407  ftc1anclem8  38410  asindmre  38413  dvasin  38414  areacirclem4  38421  areacirc  38423  isbnd3  38495  ssbnd  38499  prdsbnd  38504  bfplem2  38534  bfp  38535  renegclALT  39797  0cnALT3  43081  sn-1ne2  43092  itrere  43139  oexpreposd  43143  tan3rdpi  43173  asin1half  43178  readvrec2  43182  sn-00idlem2  43220  sn-00idlem3  43221  sn-00id  43222  sn-0tie0  43285  sn-ltaddpos  43287  sn-ltaddneg  43288  relt0neg1  43290  sn-nnne0  43294  reelznn0nn  43295  sn-0lt1  43309  sn-inelr  43321  sn-itrere  43322  sn-retire  43323  pellexlem6  43621  elpell14qr2  43649  oddcomabszz  43731  zindbi  43733  jm2.24  43750  acongeq  43770  arearect  44002  areaquad  44003  reabsifneg  44418  reabsifnpos  44419  reabsifpos  44420  reabsifnneg  44421  imsqrtvalex  44432  relexp01min  44499  imo72b2lem2  44953  imo72b2lem1  44955  imo72b2  44958  dvconstbi  45104  binomcxplemnn0  45119  binomcxplemdvbinom  45123  binomcxplemcvg  45124  binomcxplemnotnn0  45126  sineq0ALT  45705  halffl  46075  ren0  46176  rexanuz2nf  46266  sqrlearg  46329  limsup10ex  46547  dvnmptdivc  46712  dvnmul  46717  itgsin0pilem1  46724  itgsinexplem1  46728  itgsinexp  46729  iblempty  46739  stoweidlem17  46791  stoweidlem36  46810  stoweidlem55  46829  wallispilem1  46839  wallispilem2  46840  wallispilem4  46842  stirlinglem4  46851  stirlinglem13  46860  stirlinglem14  46861  stirlingr  46864  dirker2re  46866  dirkerdenne0  46867  dirkerre  46869  dirkertrigeqlem1  46872  dirkercncflem2  46878  dirkercncflem4  46880  fourierdlem11  46892  fourierdlem16  46897  fourierdlem21  46902  fourierdlem22  46903  fourierdlem41  46922  fourierdlem42  46923  fourierdlem62  46942  fourierdlem66  46946  fourierdlem79  46959  fourierdlem83  46963  fourierdlem94  46974  fourierdlem102  46982  fourierdlem103  46983  fourierdlem104  46984  fourierdlem111  46991  fourierdlem112  46992  fourierdlem113  46993  fourierdlem114  46994  sqwvfoura  47002  sqwvfourb  47003  fourierswlem  47004  fouriersw  47005  etransclem23  47031  etransclem44  47052  etransclem46  47054  salexct3  47116  salgensscntex  47118  sge0rnn0  47142  sge00  47150  0ome  47303  ovn0lem  47339  ovnhoilem1  47375  smfmullem1  47565  smfmullem2  47566  smfmullem3  47567  smfmullem4  47568  squeezedltsq  47663  goldrapos  47680  zm1nn  48099  sqrtnegnre  48104  flmrecm1  48140  m1mod0mod1  48157  muldvdsfacgt  48183  fmtnoprmfac2lem1  48378  31prm  48409  mod42tp1mod8  48414  nfermltl2rev  48568  tgblthelfgott  48640  usgrexmpl1lem  48846  usgrexmpl2lem  48851  usgrexmpl2nb0  48856  usgrexmpl2nb5  48861  usgrexmpl2trifr  48862  gpgusgralem  48881  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  pgnbgreunbgrlem2lem3  48941  gpg5edgnedg  48955  altgsumbcALT  49192  expnegico01  49357  dignnld  49442  eenglngeehlnmlem1  49576  line2ylem  49590  line2y  49594  itsclc0yqsollem2  49602  icccldii  49756  i0oii  49757  sepfsepc  49765  ex-gt  50565