Theorem 0re 11210

Description: The number 0 is real. Remark: the first step could also be ax-icn 11159. See also 0reALT 11555. (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 11158	. 2 ⊢ 1 ∈ ℂ
2		cnre 11205	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11171	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11183	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2857	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 248	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3172	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 16	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 485	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3164	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∃wrex 3095  (class class class)co 7411  ℂcc 11098  ℝcr 11099  0cc0 11100  1c1 11101  ici 11102   + caddc 11103   · cmul 11105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11158  ax-addrcl 11161  ax-rnegex 11171  ax-cnre 11173

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-rex 3096

This theorem is referenced by:  0red  11211  pr01ssre  11212  0xr  11256  axmulgt0  11284  ne0gt0  11315  00id  11385  mul02lem1  11386  mul02lem2  11387  mul02  11388  addrid  11390  ltaddneg  11426  addgt0  11700  addgegt0  11701  addgtge0  11702  addge0  11703  ltaddpos  11704  ltneg  11714  leneg  11717  lt0neg1  11720  lt0neg2  11721  le0neg1  11722  le0neg2  11723  addge01  11724  suble0  11728  mulge0  11732  msqge0  11735  0le1  11737  relin01  11738  gt0ne0i  11749  lt0ne0d  11779  elimge0  12054  ltm1  12057  recgt0  12061  prodgt0  12062  lemul1a  12069  ltmul12a  12071  lemul12a  12073  gt0div  12081  ge0div  12082  mulge0b  12085  lediv12a  12108  recgt1i  12112  recreclt  12114  ledivp1  12117  squeeze0  12118  recgt0ii  12121  ledivp1i  12140  ltdivp1i  12141  fimaxre2  12160  inelr  12208  crne0  12211  indf  12224  indfval  12225  nnge1  12264  nngt0  12267  nnnle0  12269  nnne0  12270  nnrecgt0  12279  0le0  12342  0le2  12343  halfge0  12460  nn0ssre  12508  nn0ge0  12529  nn0nlt0  12530  nn0le0eq0  12532  0mnnnnn0  12536  elnnnn0b  12548  elnnnn0c  12549  nn0sub  12554  elnnz  12601  0z  12602  elnn0z  12604  elnnz1  12620  recnz  12671  gtndiv  12673  fnn0ind  12695  10re  12734  rpge0  13030  rpneg  13050  0nrp  13053  0ltpnf  13147  mnflt0  13150  qsqueeze  13227  xneg0  13238  xaddrid  13267  xnn0xadd0  13273  xmulpnf1  13300  xlemul1a  13314  xadddi  13321  xrsupsslem  13333  xrinfmsslem  13334  elrege0  13481  0e0icopnf  13485  elicc01  13493  0elunit  13496  unitssre  13526  nnge2recico01  13534  0nelfz1  13571  fzpreddisj  13601  fz0to4untppr  13658  fz0to5un2tp  13659  nn0p1elfzo  13731  ico01fl0  13852  rpsup  13899  modelico  13914  0mod  13935  1mod  13936  le2sq2  14171  expubnd  14214  sqlecan  14245  bernneq2  14266  expnbnd  14268  expnlbnd  14269  expmulnbnd  14271  discr1  14275  discr  14276  faclbnd  14326  faclbnd3  14328  faclbnd6  14335  bcval4  14343  bcval5  14354  bcpasc  14357  hasheq0  14399  hashneq0  14400  hashnn0n0nn  14427  hashgt12el  14459  hashgt12el2  14460  hashge2el2dif  14517  lsw0  14602  swrdccatin2  14766  pfxccatin12lem3  14769  sgnclre  15139  sgnnbi  15141  sgnpbi  15142  reim0  15169  re0  15203  im0  15204  rei  15207  imi  15208  cj0  15209  sqeqd  15217  rennim  15290  cnpart  15291  sqrt0  15292  01sqrexlem4  15296  resqrex  15301  sqrtgt0  15309  sqrt00  15314  sqrtneglem  15317  sqrt9  15324  sqrt2gt1lt2  15325  leabs  15350  absor  15351  max0add  15361  eqsqrt2d  15420  sqrtpclii  15434  rlimconst  15595  rlimrege0  15630  lo1mul  15679  iserge0  15712  fsum00  15850  isumless  15899  arisum2  15915  georeclim  15926  geo2sum  15927  geoisumr  15932  0.999...  15935  cvgrat  15937  fprodge0  16047  bpoly4  16113  cos0  16206  ef01bndlem  16240  sin01bnd  16241  cos01bnd  16242  cos2bnd  16244  sin01gt0  16246  cos01gt0  16247  sincos2sgn  16250  sin4lt0  16251  absef  16253  absefib  16254  efieq1re  16255  epos  16263  rpnnen2lem2  16271  rpnnen2lem3  16272  rpnnen2lem4  16273  rpnnen2lem9  16278  ruclem6  16291  dvdslelem  16367  divalglem1  16452  divalglem5  16455  divalglem6  16456  flodddiv4  16473  sadcadd  16516  gcdn0gt0  16576  nn0seqcvgd  16628  algcvgblem  16635  algcvga  16637  pythagtriplem12  16886  pythagtriplem13  16887  pythagtriplem14  16888  pythagtriplem16  16890  prmreclem4  16979  prmreclem5  16980  prmreclem6  16981  1arith  16987  ramz  17085  chnub  18678  mulgnegnn  19150  subgmulg  19207  srgbinomlem4  20311  isabvd  20893  abvtrivd  20913  rge0srg  21557  xrs1mnd  21559  xrs10  21560  psgnodpmr  21709  re0g  21731  psrbaglesupp  22041  psdmvr  22301  mnfnei  23347  imasdsf1olem  24499  ssblps  24548  ssbl  24549  xmeter  24559  dscmet  24698  dscopn  24699  nmoi  24854  nmoeq0  24862  0nghm  24867  idnghm  24869  cnbl0  24899  xrsxmet  24936  metdseq0  24981  iicmp  25014  iiconn  25015  iihalf1  25059  elii1  25063  icopnfcnv  25070  icopnfhmeo  25071  iccpnfcnv  25072  xrhmeo  25074  xrhmph  25075  htpycc  25108  reparphti  25125  pcoval1  25141  pco0  25142  pcoval2  25144  pcocn  25145  pcohtpylem  25147  pcopt  25150  pcopt2  25151  pcoass  25152  pcorevlem  25154  reust  25509  recusp  25510  rrx0el  25526  minveclem4c  25553  minveclem2  25554  minveclem3b  25556  minveclem4  25560  minveclem7  25563  pjthlem1  25565  cniccbdd  25589  ovolunnul  25628  ovoliunnul  25635  ovolicc1  25644  ovolre  25653  iccvolcl  25695  ovolioo  25696  ioovolcl  25698  ioorcl  25705  vitalilem4  25739  vitalilem5  25740  vitali  25741  ismbf  25756  mbfmulc2lem  25775  mbfpos  25779  mbfposr  25780  i1f0  25815  i1f1  25818  itg1addlem2  25825  itg1addlem4  25827  itg1addlem5  25828  mbfi1fseqlem4  25846  mbfi1fseqlem5  25847  mbfi1flimlem  25850  xrge0f  25859  itg2ge0  25863  itg2const  25868  itg2mulc  25875  itg2splitlem  25876  itg2gt0  25888  itg2cnlem1  25889  ibl0  25915  iblrelem  25919  iblposlem  25920  iblpos  25921  iblre  25922  itgreval  25925  itgneg  25932  iblss  25933  i1fibl  25936  itgitg1  25937  itgle  25938  itgeqa  25942  itgless  25945  iblconst  25946  itgconst  25947  ibladdlem  25948  itgaddlem2  25952  iblabslem  25956  iblabsr  25958  iblmulc2  25959  itgmulc2lem2  25961  itgabs  25963  itgsplit  25964  bddmulibl  25967  dvferm1  26113  dvferm2  26115  dvferm  26116  dvlip  26121  c1lip1  26125  dveq0  26128  dv11cn  26129  dvne0  26139  ftc1lem4  26167  ply1divex  26263  dgrco  26401  plyrecj  26407  plyn0mulidp  26411  vieta1lem2  26441  aalioulem2  26463  aalioulem3  26464  pserulm  26551  psercnlem2  26553  psercnlem1  26554  psercn  26555  abelth  26570  reeff1olem  26575  reeff1o  26576  pilem2  26581  pilem3  26582  pipos  26589  pige0  26590  sinhalfpilem  26594  sincosq1sgn  26629  sincosq2sgn  26630  coseq00topi  26633  coseq0negpitopi  26634  tangtx  26636  tanabsge  26637  sinq12ge0  26639  sinq34lt0t  26640  cosq14ge0  26642  sincos4thpi  26644  sincos6thpi  26647  pige3ALT  26651  sineq0  26655  cosordlem  26661  cosord  26662  cos0pilt1  26663  cos11  26664  sinord  26665  recosf1o  26666  resinf1o  26667  tanord1  26668  tanord  26669  tanregt0  26670  efif1olem4  26676  efifo  26678  relogrn  26692  log1  26716  logi  26718  logneg  26719  argregt0  26741  argrege0  26742  argimgt0  26743  logneg2  26746  logdivlti  26751  logdivlt  26752  ellogdm  26770  logdmn0  26771  logdmnrp  26772  logcnlem3  26775  dvloglem  26779  logdmopn  26780  logf1o2  26781  dvlog2lem  26783  efopnlem1  26787  logtayl  26791  recxpcl  26806  cxpge0  26814  cxple2  26828  cxple2a  26830  cxpsqrtlem  26833  cxpcn3  26879  cxpaddlelem  26882  cxpaddle  26883  loglesqrt  26892  logbrec  26913  ang180lem3  26942  ang180lem4  26943  asinneg  27017  asin1  27025  reasinsin  27027  acosbnd  27031  atan0  27039  atanrecl  27042  atanlogaddlem  27044  atanlogsublem  27046  atanlogsub  27047  atantan  27054  atanbnd  27057  atan1  27059  atans2  27062  ressatans  27065  log2cnv  27075  log2tlbnd  27076  log2ub  27080  log2le1  27081  rlimcnp  27096  rlimcnp2  27097  o1cxp  27105  jensen  27119  amgm  27121  emgt0  27137  harmonicbnd3  27138  harmoniclbnd  27139  harmonicbnd4  27141  zetacvg  27145  eldmgm  27152  lgamgulmlem2  27160  basellem3  27213  basellem8  27218  efnnfsumcl  27233  ppisval  27234  vmage0  27251  chpge0  27256  efchtdvds  27289  ppiltx  27307  ppiub  27334  chpeq0  27338  chteq0  27339  chtleppi  27340  chpchtsum  27349  chpub  27350  dchr1re  27393  bcmono  27407  efexple  27411  bposlem1  27414  bposlem4  27417  bposlem5  27418  bposlem7  27420  bposlem8  27421  bposlem9  27422  lgsval2lem  27437  lgsval4a  27449  lgsneg  27451  lgsdilem  27454  lgsdir2lem1  27455  2lgsoddprmlem3a  27540  2lgsoddprmlem3b  27541  2lgsoddprmlem3c  27542  2lgsoddprmlem3d  27543  rplogsumlem2  27615  rpvmasumlem  27617  dchrisum0flblem1  27638  dchrisum0flblem2  27639  dchrisum0fno1  27641  rplogsum  27657  logdivsum  27663  mulog2sumlem2  27665  selberg2lem  27680  logdivbnd  27686  pntrsumo1  27695  pntrlog2bndlem4  27710  pntrlog2bndlem5  27711  pntpbnd1  27716  pntpbnd2  27717  pntlem3  27739  pntleml  27741  ostth2  27767  trgcgrg  28750  ttgcontlem1  29175  axlowdimlem1  29233  axlowdimlem6  29238  axlowdimlem7  29239  axlowdimlem10  29242  axlowdim1  29250  axlowdim2  29251  axlowdim  29252  elntg2  29276  umgrislfupgrlem  29413  lfgrnloop  29416  lfuhgr1v0e  29545  usgrexmplef  29550  pthdlem2  30058  crctcshwlkn0lem7  30106  rusgrnumwwlks  30267  clwwlkn0  30320  konigsberg  30549  ex-po  30727  ex-sqrt  30746  ex-gcd  30749  nvz0  30961  0blo  31085  nmlno0lem  31086  nmblolbii  31092  siilem2  31145  minvecolem2  31168  minvecolem3  31169  minvecolem4c  31172  minvecolem4  31173  minvecolem5  31174  minvecolem7  31176  htthlem  31210  hiidge0  31391  normlem6  31408  normgt0  31420  norm-i  31422  normpyc  31439  bcsiALT  31472  pjhthlem1  31684  pjneli  32016  nmlnop0iALT  32288  unopbd  32308  nmbdoplbi  32317  nmcoplbi  32321  nmbdfnlbi  32342  nmbdfnlb  32343  nmcfnlbi  32345  cnlnadjlem7  32366  nmopcoi  32388  branmfn  32398  leopmul  32427  nmopleid  32432  pjbdlni  32442  pjnormssi  32461  stle0i  32532  cdj3lem1  32727  xaddeq0  33039  expgt0b  33102  dp20u  33138  dp20h  33139  dp2clq  33141  dp2lt10  33144  dp2lt  33145  dp0u  33161  dplti  33165  dpexpp1  33168  xdiv0  33189  xrge0slmod  33611  evl1deg3  33813  fldext2chn  34063  cos9thpiminplylem1  34117  unitdivcld  34236  sqsscirc1  34243  xrge0iifcnv  34268  xrge0iifiso  34270  rezh  34304  esumcvgsum  34423  voliune  34564  volfiniune  34565  sibfinima  34674  sitmcl  34686  0rrv  34786  coinfliprv  34818  ballotlem2  34824  ballotlem4  34834  ballotlemi1  34838  ballotlemic  34842  signsply0  34883  signswch  34893  signstf  34898  signstf0  34900  signstfveq0  34909  signlem0  34919  signshf  34920  itgexpif  34938  hgt750lemd  34980  hgt750lem  34983  hgt750lem2  34984  hgt750leme  34990  iisconn  35643  iillysconn  35644  cvmliftlem10  35685  fz0n  36122  bcneg1  36127  nn0prpwlem  36722  dnizeq0  36953  dnizphlfeqhlf  36954  knoppndvlem13  37002  cnndvlem1  37015  bj-pinftyccb  37753  bj-minftyccb  37757  bj-pinftynminfty  37759  taupilemrplb  37852  irrdiff  37858  sin2h  38149  tan2h  38151  ptrecube  38159  poimirlem16  38175  poimirlem17  38176  poimirlem20  38179  poimirlem22  38181  poimirlem23  38182  poimirlem29  38188  poimirlem31  38190  poimir  38192  heicant  38194  mblfinlem2  38197  ismblfin  38200  ovoliunnfl  38201  voliunnfl  38203  volsupnfl  38204  mbfposadd  38206  itg2addnclem  38210  itg2addnclem2  38211  ibladdnclem  38215  itgaddnclem2  38218  iblabsnclem  38222  iblmulc2nc  38224  itgmulc2nclem2  38226  itgabsnc  38228  ftc1cnnclem  38230  ftc1anclem5  38236  ftc1anclem8  38239  asindmre  38242  dvasin  38243  areacirclem4  38250  areacirc  38252  isbnd3  38323  ssbnd  38327  prdsbnd  38332  bfplem2  38362  bfp  38363  renegclALT  39627  0cnALT3  42911  sn-1ne2  42922  itrere  42969  oexpreposd  42973  tan3rdpi  43003  asin1half  43008  readvrec2  43012  sn-00idlem2  43050  sn-00idlem3  43051  sn-00id  43052  sn-0tie0  43115  sn-ltaddpos  43117  sn-ltaddneg  43118  relt0neg1  43120  sn-nnne0  43124  reelznn0nn  43125  sn-0lt1  43139  sn-inelr  43151  sn-itrere  43152  sn-retire  43153  pellexlem6  43453  elpell14qr2  43481  oddcomabszz  43563  zindbi  43565  jm2.24  43582  acongeq  43602  arearect  43834  areaquad  43835  reabsifneg  44250  reabsifnpos  44251  reabsifpos  44252  reabsifnneg  44253  imsqrtvalex  44264  relexp01min  44331  imo72b2lem2  44785  imo72b2lem1  44787  imo72b2  44790  dvconstbi  44936  binomcxplemnn0  44951  binomcxplemdvbinom  44955  binomcxplemcvg  44956  binomcxplemnotnn0  44958  sineq0ALT  45537  halffl  45907  ren0  46008  rexanuz2nf  46098  sqrlearg  46161  limsup10ex  46379  dvnmptdivc  46544  dvnmul  46549  itgsin0pilem1  46556  itgsinexplem1  46560  itgsinexp  46561  iblempty  46571  stoweidlem17  46623  stoweidlem36  46642  stoweidlem55  46661  wallispilem1  46671  wallispilem2  46672  wallispilem4  46674  stirlinglem4  46683  stirlinglem13  46692  stirlinglem14  46693  stirlingr  46696  dirker2re  46698  dirkerdenne0  46699  dirkerre  46701  dirkertrigeqlem1  46704  dirkercncflem2  46710  dirkercncflem4  46712  fourierdlem11  46724  fourierdlem16  46729  fourierdlem21  46734  fourierdlem22  46735  fourierdlem41  46754  fourierdlem42  46755  fourierdlem62  46774  fourierdlem66  46778  fourierdlem79  46791  fourierdlem83  46795  fourierdlem94  46806  fourierdlem102  46814  fourierdlem103  46815  fourierdlem104  46816  fourierdlem111  46823  fourierdlem112  46824  fourierdlem113  46825  fourierdlem114  46826  sqwvfoura  46834  sqwvfourb  46835  fourierswlem  46836  fouriersw  46837  etransclem23  46863  etransclem44  46884  etransclem46  46886  salexct3  46948  salgensscntex  46950  sge0rnn0  46974  sge00  46982  0ome  47135  ovn0lem  47171  ovnhoilem1  47207  smfmullem1  47397  smfmullem2  47398  smfmullem3  47399  smfmullem4  47400  squeezedltsq  47496  goldrapos  47509  zm1nn  47928  sqrtnegnre  47933  flmrecm1  47969  m1mod0mod1  47986  muldvdsfacgt  48012  fmtnoprmfac2lem1  48207  31prm  48238  mod42tp1mod8  48243  nfermltl2rev  48397  tgblthelfgott  48469  usgrexmpl1lem  48675  usgrexmpl2lem  48680  usgrexmpl2nb0  48685  usgrexmpl2nb5  48690  usgrexmpl2trifr  48691  gpgusgralem  48710  pgnbgreunbgrlem2lem1  48768  pgnbgreunbgrlem2lem2  48769  pgnbgreunbgrlem2lem3  48770  gpg5edgnedg  48784  altgsumbcALT  49018  expnegico01  49183  dignnld  49268  eenglngeehlnmlem1  49402  line2ylem  49416  line2y  49420  itsclc0yqsollem2  49428  icccldii  49582  i0oii  49583  sepfsepc  49591  ex-gt  50391