Theorem 0re 11183

Description: The number 0 is real. Remark: the first step could also be ax-icn 11134. See also 0reALT 11526. (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 11133	. 2 ⊢ 1 ∈ ℂ
2		cnre 11178	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11146	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11158	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2817	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3135	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3127	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3054  (class class class)co 7390  ℂcc 11073  ℝcr 11074  0cc0 11075  1c1 11076  ici 11077   + caddc 11078   · cmul 11080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-addrcl 11136  ax-rnegex 11146  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-rex 3055

This theorem is referenced by:  0red  11184  0xr  11228  axmulgt0  11255  ne0gt0  11286  00id  11356  mul02lem1  11357  mul02lem2  11358  mul02  11359  addrid  11361  ltaddneg  11397  addgt0  11671  addgegt0  11672  addgtge0  11673  addge0  11674  ltaddpos  11675  ltneg  11685  leneg  11688  lt0neg1  11691  lt0neg2  11692  le0neg1  11693  le0neg2  11694  addge01  11695  suble0  11699  mulge0  11703  msqge0  11706  0le1  11708  relin01  11709  gt0ne0i  11720  lt0ne0d  11750  elimge0  12028  ltm1  12031  recgt0  12035  prodgt0  12036  lemul1a  12043  ltmul12a  12045  lemul12a  12047  mulgt1OLD  12048  gt0div  12056  ge0div  12057  mulge0b  12060  lediv12a  12083  recgt1i  12087  recreclt  12089  ledivp1  12092  squeeze0  12093  recgt0ii  12096  ledivp1i  12115  ltdivp1i  12116  fimaxre2  12135  inelr  12183  crne0  12186  nnge1  12221  nngt0  12224  nnnle0  12226  nnne0  12227  nnrecgt0  12236  0le0  12294  halfge0  12405  nn0ssre  12453  nn0ge0  12474  nn0nlt0  12475  nn0le0eq0  12477  0mnnnnn0  12481  elnnnn0b  12493  elnnnn0c  12494  nn0sub  12499  elnnz  12546  0z  12547  elnn0z  12549  elnnz1  12566  recnz  12616  gtndiv  12618  fnn0ind  12640  10re  12675  rpge0  12972  rpneg  12992  0nrp  12995  0ltpnf  13089  mnflt0  13092  qsqueeze  13168  xneg0  13179  xaddrid  13208  xnn0xadd0  13214  xmulpnf1  13241  xlemul1a  13255  xadddi  13262  xrsupsslem  13274  xrinfmsslem  13275  elrege0  13422  0e0icopnf  13426  elicc01  13434  0elunit  13437  unitssre  13467  0nelfz1  13511  fzpreddisj  13541  fz0to4untppr  13598  fz0to5un2tp  13599  nn0p1elfzo  13670  ico01fl0  13788  rpsup  13835  modelico  13850  0mod  13871  1mod  13872  le2sq2  14107  expubnd  14150  sqlecan  14181  bernneq2  14202  expnbnd  14204  expnlbnd  14205  expmulnbnd  14207  discr1  14211  discr  14212  faclbnd  14262  faclbnd3  14264  faclbnd6  14271  bcval4  14279  bcval5  14290  bcpasc  14293  hasheq0  14335  hashneq0  14336  hashnn0n0nn  14363  hashgt12el  14394  hashgt12el2  14395  hashge2el2dif  14452  lsw0  14537  swrdccatin2  14701  pfxccatin12lem3  14704  reim0  15091  re0  15125  im0  15126  rei  15129  imi  15130  cj0  15131  sqeqd  15139  rennim  15212  cnpart  15213  sqrt0  15214  01sqrexlem4  15218  resqrex  15223  sqrtgt0  15231  sqrt00  15236  sqrtneglem  15239  sqrt9  15246  sqrt2gt1lt2  15247  leabs  15272  absor  15273  max0add  15283  eqsqrt2d  15342  sqrtpclii  15356  rlimconst  15517  rlimrege0  15552  lo1mul  15601  iserge0  15634  fsum00  15771  isumless  15818  arisum2  15834  georeclim  15845  geo2sum  15846  geoisumr  15851  0.999...  15854  cvgrat  15856  fprodge0  15966  bpoly4  16032  cos0  16125  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  cos2bnd  16163  sin01gt0  16165  cos01gt0  16166  sincos2sgn  16169  sin4lt0  16170  absef  16172  absefib  16173  efieq1re  16174  epos  16182  rpnnen2lem2  16190  rpnnen2lem3  16191  rpnnen2lem4  16192  rpnnen2lem9  16197  ruclem6  16210  dvdslelem  16286  divalglem1  16371  divalglem5  16374  divalglem6  16375  flodddiv4  16392  sadcadd  16435  gcdn0gt0  16495  nn0seqcvgd  16547  algcvgblem  16554  algcvga  16556  pythagtriplem12  16804  pythagtriplem13  16805  pythagtriplem14  16806  pythagtriplem16  16808  prmreclem4  16897  prmreclem5  16898  prmreclem6  16899  1arith  16905  ramz  17003  mulgnegnn  19023  subgmulg  19079  srgbinomlem4  20145  isabvd  20728  abvtrivd  20748  xrs1mnd  21328  xrs10  21329  rge0srg  21362  psgnodpmr  21506  re0g  21528  psrbaglesupp  21838  psdmvr  22063  mnfnei  23115  imasdsf1olem  24268  ssblps  24317  ssbl  24318  xmeter  24328  dscmet  24467  dscopn  24468  nmoi  24623  nmoeq0  24631  0nghm  24636  idnghm  24638  cnbl0  24668  xrsxmet  24705  metdseq0  24750  iicmp  24786  iiconn  24787  iihalf1  24832  iihalf1cnOLD  24834  elii1  24838  icopnfcnv  24847  icopnfhmeo  24848  iccpnfcnv  24849  xrhmeo  24851  xrhmph  24852  htpycc  24886  reparphti  24903  reparphtiOLD  24904  pcoval1  24920  pco0  24921  pcoval2  24923  pcocn  24924  pcohtpylem  24926  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  reust  25288  recusp  25289  rrx0el  25305  minveclem4c  25332  minveclem2  25333  minveclem3b  25335  minveclem4  25339  minveclem7  25342  pjthlem1  25344  cniccbdd  25369  ovolunnul  25408  ovoliunnul  25415  ovolicc1  25424  ovolre  25433  iccvolcl  25475  ovolioo  25476  ioovolcl  25478  ioorcl  25485  vitalilem4  25519  vitalilem5  25520  vitali  25521  ismbf  25536  mbfmulc2lem  25555  mbfpos  25559  mbfposr  25560  i1f0  25595  i1f1  25598  itg1addlem2  25605  itg1addlem4  25607  itg1addlem5  25608  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1flimlem  25630  xrge0f  25639  itg2ge0  25643  itg2const  25648  itg2mulc  25655  itg2splitlem  25656  itg2gt0  25668  itg2cnlem1  25669  ibl0  25695  iblrelem  25699  iblposlem  25700  iblpos  25701  iblre  25702  itgreval  25705  itgneg  25712  iblss  25713  i1fibl  25716  itgitg1  25717  itgle  25718  itgeqa  25722  itgless  25725  iblconst  25726  itgconst  25727  ibladdlem  25728  itgaddlem2  25732  iblabslem  25736  iblabsr  25738  iblmulc2  25739  itgmulc2lem2  25741  itgabs  25743  itgsplit  25744  bddmulibl  25747  dvferm1  25896  dvferm2  25898  dvferm  25899  dvlip  25905  c1lip1  25909  dveq0  25912  dv11cn  25913  dvne0  25923  ftc1lem4  25953  ply1divex  26049  dgrco  26188  plyrecj  26194  vieta1lem2  26226  aalioulem2  26248  aalioulem3  26249  pserulm  26338  psercnlem2  26341  psercnlem1  26342  psercn  26343  abelth  26358  reeff1olem  26363  reeff1o  26364  pilem2  26369  pilem3  26370  pipos  26375  sinhalfpilem  26379  sincosq1sgn  26414  sincosq2sgn  26415  coseq00topi  26418  coseq0negpitopi  26419  tangtx  26421  tanabsge  26422  sinq12ge0  26424  sinq34lt0t  26425  cosq14ge0  26427  sincos4thpi  26429  sincos6thpi  26432  pige3ALT  26436  sineq0  26440  cosordlem  26446  cosord  26447  cos0pilt1  26448  cos11  26449  sinord  26450  recosf1o  26451  resinf1o  26452  tanord1  26453  tanord  26454  tanregt0  26455  efif1olem4  26461  efifo  26463  relogrn  26477  log1  26501  logi  26503  logneg  26504  argregt0  26526  argrege0  26527  argimgt0  26528  logneg2  26531  logdivlti  26536  logdivlt  26537  ellogdm  26555  logdmn0  26556  logdmnrp  26557  logcnlem3  26560  dvloglem  26564  logdmopn  26565  logf1o2  26566  dvlog2lem  26568  efopnlem1  26572  logtayl  26576  recxpcl  26591  cxpge0  26599  cxple2  26613  cxple2a  26615  cxpsqrtlem  26618  cxpcn3  26665  cxpaddlelem  26668  cxpaddle  26669  loglesqrt  26678  logbrec  26699  ang180lem3  26728  ang180lem4  26729  asinneg  26803  asin1  26811  reasinsin  26813  acosbnd  26817  atan0  26825  atanrecl  26828  atanlogaddlem  26830  atanlogsublem  26832  atanlogsub  26833  atantan  26840  atanbnd  26843  atan1  26845  atans2  26848  ressatans  26851  log2cnv  26861  log2tlbnd  26862  log2ub  26866  log2le1  26867  rlimcnp  26882  rlimcnp2  26883  o1cxp  26892  jensen  26906  amgm  26908  emgt0  26924  harmonicbnd3  26925  harmoniclbnd  26926  harmonicbnd4  26928  zetacvg  26932  eldmgm  26939  lgamgulmlem2  26947  basellem3  27000  basellem8  27005  efnnfsumcl  27020  ppisval  27021  vmage0  27038  chpge0  27043  efchtdvds  27076  ppiltx  27094  ppiub  27122  chpeq0  27126  chteq0  27127  chtleppi  27128  chpchtsum  27137  chpub  27138  dchr1re  27181  bcmono  27195  efexple  27199  bposlem1  27202  bposlem4  27205  bposlem5  27206  bposlem7  27208  bposlem8  27209  bposlem9  27210  lgsval2lem  27225  lgsval4a  27237  lgsneg  27239  lgsdilem  27242  lgsdir2lem1  27243  2lgsoddprmlem3a  27328  2lgsoddprmlem3b  27329  2lgsoddprmlem3c  27330  2lgsoddprmlem3d  27331  rplogsumlem2  27403  rpvmasumlem  27405  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0fno1  27429  rplogsum  27445  logdivsum  27451  mulog2sumlem2  27453  selberg2lem  27468  logdivbnd  27474  pntrsumo1  27483  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntpbnd1  27504  pntpbnd2  27505  pntlem3  27527  pntleml  27529  ostth2  27555  trgcgrg  28449  ttgcontlem1  28819  axlowdimlem1  28876  axlowdimlem6  28881  axlowdimlem7  28882  axlowdimlem10  28885  axlowdim1  28893  axlowdim2  28894  axlowdim  28895  elntg2  28919  umgrislfupgrlem  29056  lfgrnloop  29059  lfuhgr1v0e  29188  usgrexmplef  29193  pthdlem2  29705  crctcshwlkn0lem7  29753  rusgrnumwwlks  29911  clwwlkn0  29964  konigsberg  30193  ex-po  30371  ex-sqrt  30390  ex-gcd  30393  nvz0  30604  0blo  30728  nmlno0lem  30729  nmblolbii  30735  siilem2  30788  minvecolem2  30811  minvecolem3  30812  minvecolem4c  30815  minvecolem4  30816  minvecolem5  30817  minvecolem7  30819  htthlem  30853  hiidge0  31034  normlem6  31051  normgt0  31063  norm-i  31065  normpyc  31082  bcsiALT  31115  pjhthlem1  31327  pjneli  31659  nmlnop0iALT  31931  unopbd  31951  nmbdoplbi  31960  nmcoplbi  31964  nmbdfnlbi  31985  nmbdfnlb  31986  nmcfnlbi  31988  cnlnadjlem7  32009  nmopcoi  32031  branmfn  32041  leopmul  32070  nmopleid  32075  pjbdlni  32085  pjnormssi  32104  stle0i  32175  cdj3lem1  32370  xaddeq0  32683  expgt0b  32748  pr01ssre  32756  sgnclre  32764  sgnnbi  32770  sgnpbi  32771  indf  32785  indfval  32786  dp20u  32805  dp20h  32806  dp2clq  32808  dp2lt10  32811  dp2lt  32812  dp0u  32828  dplti  32832  dpexpp1  32835  xdiv0  32856  chnub  32945  xrge0slmod  33326  evl1deg3  33554  fldext2chn  33725  cos9thpiminplylem1  33779  unitdivcld  33898  sqsscirc1  33905  xrge0iifcnv  33930  xrge0iifiso  33932  rezh  33966  esumcvgsum  34085  voliune  34226  volfiniune  34227  sibfinima  34337  sitmcl  34349  0rrv  34449  coinfliprv  34481  ballotlem2  34487  ballotlem4  34497  ballotlemi1  34501  ballotlemic  34505  plymulx0  34545  signsply0  34549  signswch  34559  signstf  34564  signstf0  34566  signstfveq0  34575  signlem0  34585  signshf  34586  itgexpif  34604  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  iisconn  35246  iillysconn  35247  cvmliftlem10  35288  fz0n  35725  bcneg1  35730  nn0prpwlem  36317  dnizeq0  36470  dnizphlfeqhlf  36471  knoppndvlem13  36519  cnndvlem1  36532  bj-pinftyccb  37216  bj-minftyccb  37220  bj-pinftynminfty  37222  taupilemrplb  37315  irrdiff  37321  sin2h  37611  tan2h  37613  ptrecube  37621  poimirlem16  37637  poimirlem17  37638  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem29  37650  poimirlem31  37652  poimir  37654  heicant  37656  mblfinlem2  37659  ismblfin  37662  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  mbfposadd  37668  itg2addnclem  37672  itg2addnclem2  37673  ibladdnclem  37677  itgaddnclem2  37680  iblabsnclem  37684  iblmulc2nc  37686  itgmulc2nclem2  37688  itgabsnc  37690  ftc1cnnclem  37692  ftc1anclem5  37698  ftc1anclem8  37701  asindmre  37704  dvasin  37705  areacirclem4  37712  areacirc  37714  isbnd3  37785  ssbnd  37789  prdsbnd  37794  bfplem2  37824  bfp  37825  renegclALT  38963  0cnALT3  42248  sn-1ne2  42260  itrere  42313  oexpreposd  42317  tan3rdpi  42347  asin1half  42352  readvrec2  42356  sn-00idlem2  42394  sn-00idlem3  42395  sn-00id  42396  sn-0tie0  42446  sn-ltaddpos  42448  sn-ltaddneg  42449  relt0neg1  42451  sn-nnne0  42455  reelznn0nn  42456  sn-0lt1  42470  sn-inelr  42482  sn-itrere  42483  sn-retire  42484  pellexlem6  42829  elpell14qr2  42857  oddcomabszz  42940  zindbi  42942  jm2.24  42959  acongeq  42979  arearect  43211  areaquad  43212  reabsifneg  43628  reabsifnpos  43629  reabsifpos  43630  reabsifnneg  43631  imsqrtvalex  43642  relexp01min  43709  imo72b2lem2  44163  imo72b2lem1  44165  imo72b2  44168  dvconstbi  44330  binomcxplemnn0  44345  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemnotnn0  44352  sineq0ALT  44933  halffl  45301  ren0  45405  rexanuz2nf  45495  sqrlearg  45558  limsup10ex  45778  dvnmptdivc  45943  dvnmul  45948  itgsin0pilem1  45955  itgsinexplem1  45959  itgsinexp  45960  iblempty  45970  stoweidlem17  46022  stoweidlem36  46041  stoweidlem55  46060  wallispilem1  46070  wallispilem2  46071  wallispilem4  46073  stirlinglem4  46082  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  stirlingr  46095  dirker2re  46097  dirkerdenne0  46098  dirkerre  46100  dirkertrigeqlem1  46103  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem11  46123  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem41  46153  fourierdlem42  46154  fourierdlem48  46159  fourierdlem62  46173  fourierdlem66  46177  fourierdlem79  46190  fourierdlem83  46194  fourierdlem94  46205  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fourierdlem114  46225  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  etransclem23  46262  etransclem44  46283  etransclem46  46285  salexct3  46347  salgensscntex  46349  sge0rnn0  46373  sge00  46381  0ome  46534  ovn0lem  46570  ovnhoilem1  46606  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  smfmullem4  46799  squeezedltsq  46894  zm1nn  47307  sqrtnegnre  47312  m1mod0mod1  47359  fmtnoprmfac2lem1  47571  31prm  47602  mod42tp1mod8  47607  nfermltl2rev  47748  tgblthelfgott  47820  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032  gpgusgralem  48051  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  altgsumbcALT  48345  expnegico01  48511  dignnld  48596  eenglngeehlnmlem1  48730  line2ylem  48744  line2y  48748  itsclc0yqsollem2  48756  icccldii  48911  i0oii  48912  sepfsepc  48920  ex-gt  49721