Theorem 0re 11183

Description: The number 0 is real. Remark: the first step could also be ax-icn 11132. See also 0reALT 11528. (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 11131	. 2 ⊢ 1 ∈ ℂ
2		cnre 11178	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11144	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11156	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2850	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 247	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3163	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 484	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3155	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∃wrex 3086  (class class class)co 7396  ℂcc 11071  ℝcr 11072  0cc0 11073  1c1 11074  ici 11075   + caddc 11076   · cmul 11078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-addrcl 11134  ax-rnegex 11144  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837  df-rex 3087

This theorem is referenced by:  0red  11184  pr01ssre  11185  0xr  11229  axmulgt0  11257  ne0gt0  11288  00id  11358  mul02lem1  11359  mul02lem2  11360  mul02  11361  addrid  11363  ltaddneg  11399  addgt0  11673  addgegt0  11674  addgtge0  11675  addge0  11676  ltaddpos  11677  ltneg  11687  leneg  11690  lt0neg1  11693  lt0neg2  11694  le0neg1  11695  le0neg2  11696  addge01  11697  suble0  11701  mulge0  11705  msqge0  11708  0le1  11710  relin01  11711  gt0ne0i  11722  lt0ne0d  11752  elimge0  12030  ltm1  12033  recgt0  12037  prodgt0  12038  lemul1a  12045  ltmul12a  12047  lemul12a  12049  mulgt1OLD  12050  gt0div  12058  ge0div  12059  mulge0b  12062  lediv12a  12085  recgt1i  12089  recreclt  12091  ledivp1  12094  squeeze0  12095  recgt0ii  12098  ledivp1i  12117  ltdivp1i  12118  fimaxre2  12137  inelr  12185  crne0  12188  indf  12201  indfval  12202  nnge1  12241  nngt0  12244  nnnle0  12246  nnne0  12247  nnrecgt0  12256  0le0  12319  0le2  12320  halfge0  12437  nn0ssre  12485  nn0ge0  12506  nn0nlt0  12507  nn0le0eq0  12509  0mnnnnn0  12513  elnnnn0b  12525  elnnnn0c  12526  nn0sub  12531  elnnz  12578  0z  12579  elnn0z  12581  elnnz1  12597  recnz  12648  gtndiv  12650  fnn0ind  12672  10re  12711  rpge0  13007  rpneg  13027  0nrp  13030  0ltpnf  13124  mnflt0  13127  qsqueeze  13204  xneg0  13215  xaddrid  13244  xnn0xadd0  13250  xmulpnf1  13277  xlemul1a  13291  xadddi  13298  xrsupsslem  13310  xrinfmsslem  13311  elrege0  13458  0e0icopnf  13462  elicc01  13470  0elunit  13473  unitssre  13503  nnge2recico01  13511  0nelfz1  13548  fzpreddisj  13578  fz0to4untppr  13635  fz0to5un2tp  13636  nn0p1elfzo  13708  ico01fl0  13829  rpsup  13876  modelico  13891  0mod  13912  1mod  13913  le2sq2  14148  expubnd  14191  sqlecan  14222  bernneq2  14243  expnbnd  14245  expnlbnd  14246  expmulnbnd  14248  discr1  14252  discr  14253  faclbnd  14303  faclbnd3  14305  faclbnd6  14312  bcval4  14320  bcval5  14331  bcpasc  14334  hasheq0  14376  hashneq0  14377  hashnn0n0nn  14404  hashgt12el  14435  hashgt12el2  14436  hashge2el2dif  14493  lsw0  14578  swrdccatin2  14742  pfxccatin12lem3  14745  sgnclre  15115  sgnnbi  15117  sgnpbi  15118  reim0  15145  re0  15179  im0  15180  rei  15183  imi  15184  cj0  15185  sqeqd  15193  rennim  15266  cnpart  15267  sqrt0  15268  01sqrexlem4  15272  resqrex  15277  sqrtgt0  15285  sqrt00  15290  sqrtneglem  15293  sqrt9  15300  sqrt2gt1lt2  15301  leabs  15326  absor  15327  max0add  15337  eqsqrt2d  15396  sqrtpclii  15410  rlimconst  15571  rlimrege0  15606  lo1mul  15655  iserge0  15688  fsum00  15826  isumless  15875  arisum2  15891  georeclim  15902  geo2sum  15903  geoisumr  15908  0.999...  15911  cvgrat  15913  fprodge0  16023  bpoly4  16089  cos0  16182  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  cos2bnd  16220  sin01gt0  16222  cos01gt0  16223  sincos2sgn  16226  sin4lt0  16227  absef  16229  absefib  16230  efieq1re  16231  epos  16239  rpnnen2lem2  16247  rpnnen2lem3  16248  rpnnen2lem4  16249  rpnnen2lem9  16254  ruclem6  16267  dvdslelem  16343  divalglem1  16428  divalglem5  16431  divalglem6  16432  flodddiv4  16449  sadcadd  16492  gcdn0gt0  16552  nn0seqcvgd  16604  algcvgblem  16611  algcvga  16613  pythagtriplem12  16862  pythagtriplem13  16863  pythagtriplem14  16864  pythagtriplem16  16866  prmreclem4  16955  prmreclem5  16956  prmreclem6  16957  1arith  16963  ramz  17061  chnub  18654  mulgnegnn  19126  subgmulg  19182  srgbinomlem4  20279  isabvd  20861  abvtrivd  20881  rge0srg  21490  xrs1mnd  21492  xrs10  21493  psgnodpmr  21642  re0g  21664  psrbaglesupp  21974  psdmvr  22234  mnfnei  23281  imasdsf1olem  24433  ssblps  24482  ssbl  24483  xmeter  24493  dscmet  24632  dscopn  24633  nmoi  24788  nmoeq0  24796  0nghm  24801  idnghm  24803  cnbl0  24833  xrsxmet  24870  metdseq0  24915  iicmp  24948  iiconn  24949  iihalf1  24993  elii1  24997  icopnfcnv  25004  icopnfhmeo  25005  iccpnfcnv  25006  xrhmeo  25008  xrhmph  25009  htpycc  25042  reparphti  25059  pcoval1  25075  pco0  25076  pcoval2  25078  pcocn  25079  pcohtpylem  25081  pcopt  25084  pcopt2  25085  pcoass  25086  pcorevlem  25088  reust  25443  recusp  25444  rrx0el  25460  minveclem4c  25487  minveclem2  25488  minveclem3b  25490  minveclem4  25494  minveclem7  25497  pjthlem1  25499  cniccbdd  25523  ovolunnul  25562  ovoliunnul  25569  ovolicc1  25578  ovolre  25587  iccvolcl  25629  ovolioo  25630  ioovolcl  25632  ioorcl  25639  vitalilem4  25673  vitalilem5  25674  vitali  25675  ismbf  25690  mbfmulc2lem  25709  mbfpos  25713  mbfposr  25714  i1f0  25749  i1f1  25752  itg1addlem2  25759  itg1addlem4  25761  itg1addlem5  25762  mbfi1fseqlem4  25780  mbfi1fseqlem5  25781  mbfi1flimlem  25784  xrge0f  25793  itg2ge0  25797  itg2const  25802  itg2mulc  25809  itg2splitlem  25810  itg2gt0  25822  itg2cnlem1  25823  ibl0  25849  iblrelem  25853  iblposlem  25854  iblpos  25855  iblre  25856  itgreval  25859  itgneg  25866  iblss  25867  i1fibl  25870  itgitg1  25871  itgle  25872  itgeqa  25876  itgless  25879  iblconst  25880  itgconst  25881  ibladdlem  25882  itgaddlem2  25886  iblabslem  25890  iblabsr  25892  iblmulc2  25893  itgmulc2lem2  25895  itgabs  25897  itgsplit  25898  bddmulibl  25901  dvferm1  26047  dvferm2  26049  dvferm  26050  dvlip  26055  c1lip1  26059  dveq0  26062  dv11cn  26063  dvne0  26073  ftc1lem4  26101  ply1divex  26197  dgrco  26335  plyrecj  26341  plyn0mulidp  26345  vieta1lem2  26375  aalioulem2  26397  aalioulem3  26398  pserulm  26485  psercnlem2  26487  psercnlem1  26488  psercn  26489  abelth  26504  reeff1olem  26509  reeff1o  26510  pilem2  26515  pilem3  26516  pipos  26523  pige0  26524  sinhalfpilem  26528  sincosq1sgn  26563  sincosq2sgn  26564  coseq00topi  26567  coseq0negpitopi  26568  tangtx  26570  tanabsge  26571  sinq12ge0  26573  sinq34lt0t  26574  cosq14ge0  26576  sincos4thpi  26578  sincos6thpi  26581  pige3ALT  26585  sineq0  26589  cosordlem  26595  cosord  26596  cos0pilt1  26597  cos11  26598  sinord  26599  recosf1o  26600  resinf1o  26601  tanord1  26602  tanord  26603  tanregt0  26604  efif1olem4  26610  efifo  26612  relogrn  26626  log1  26650  logi  26652  logneg  26653  argregt0  26675  argrege0  26676  argimgt0  26677  logneg2  26680  logdivlti  26685  logdivlt  26686  ellogdm  26704  logdmn0  26705  logdmnrp  26706  logcnlem3  26709  dvloglem  26713  logdmopn  26714  logf1o2  26715  dvlog2lem  26717  efopnlem1  26721  logtayl  26725  recxpcl  26740  cxpge0  26748  cxple2  26762  cxple2a  26764  cxpsqrtlem  26767  cxpcn3  26813  cxpaddlelem  26816  cxpaddle  26817  loglesqrt  26826  logbrec  26847  ang180lem3  26876  ang180lem4  26877  asinneg  26951  asin1  26959  reasinsin  26961  acosbnd  26965  atan0  26973  atanrecl  26976  atanlogaddlem  26978  atanlogsublem  26980  atanlogsub  26981  atantan  26988  atanbnd  26991  atan1  26993  atans2  26996  ressatans  26999  log2cnv  27009  log2tlbnd  27010  log2ub  27014  log2le1  27015  rlimcnp  27030  rlimcnp2  27031  o1cxp  27039  jensen  27053  amgm  27055  emgt0  27071  harmonicbnd3  27072  harmoniclbnd  27073  harmonicbnd4  27075  zetacvg  27079  eldmgm  27086  lgamgulmlem2  27094  basellem3  27147  basellem8  27152  efnnfsumcl  27167  ppisval  27168  vmage0  27185  chpge0  27190  efchtdvds  27223  ppiltx  27241  ppiub  27268  chpeq0  27272  chteq0  27273  chtleppi  27274  chpchtsum  27283  chpub  27284  dchr1re  27327  bcmono  27341  efexple  27345  bposlem1  27348  bposlem4  27351  bposlem5  27352  bposlem7  27354  bposlem8  27355  bposlem9  27356  lgsval2lem  27371  lgsval4a  27383  lgsneg  27385  lgsdilem  27388  lgsdir2lem1  27389  2lgsoddprmlem3a  27474  2lgsoddprmlem3b  27475  2lgsoddprmlem3c  27476  2lgsoddprmlem3d  27477  rplogsumlem2  27549  rpvmasumlem  27551  dchrisum0flblem1  27572  dchrisum0flblem2  27573  dchrisum0fno1  27575  rplogsum  27591  logdivsum  27597  mulog2sumlem2  27599  selberg2lem  27614  logdivbnd  27620  pntrsumo1  27629  pntrlog2bndlem4  27644  pntrlog2bndlem5  27645  pntpbnd1  27650  pntpbnd2  27651  pntlem3  27673  pntleml  27675  ostth2  27701  trgcgrg  28684  ttgcontlem1  29085  axlowdimlem1  29143  axlowdimlem6  29148  axlowdimlem7  29149  axlowdimlem10  29152  axlowdim1  29160  axlowdim2  29161  axlowdim  29162  elntg2  29186  umgrislfupgrlem  29323  lfgrnloop  29326  lfuhgr1v0e  29455  usgrexmplef  29460  pthdlem2  29968  crctcshwlkn0lem7  30016  rusgrnumwwlks  30177  clwwlkn0  30230  konigsberg  30459  ex-po  30637  ex-sqrt  30656  ex-gcd  30659  nvz0  30871  0blo  30995  nmlno0lem  30996  nmblolbii  31002  siilem2  31055  minvecolem2  31078  minvecolem3  31079  minvecolem4c  31082  minvecolem4  31083  minvecolem5  31084  minvecolem7  31086  htthlem  31120  hiidge0  31301  normlem6  31318  normgt0  31330  norm-i  31332  normpyc  31349  bcsiALT  31382  pjhthlem1  31594  pjneli  31926  nmlnop0iALT  32198  unopbd  32218  nmbdoplbi  32227  nmcoplbi  32231  nmbdfnlbi  32252  nmbdfnlb  32253  nmcfnlbi  32255  cnlnadjlem7  32276  nmopcoi  32298  branmfn  32308  leopmul  32337  nmopleid  32342  pjbdlni  32352  pjnormssi  32371  stle0i  32442  cdj3lem1  32637  xaddeq0  32955  expgt0b  33019  dp20u  33055  dp20h  33056  dp2clq  33058  dp2lt10  33061  dp2lt  33062  dp0u  33078  dplti  33082  dpexpp1  33085  xdiv0  33106  xrge0slmod  33534  evl1deg3  33774  fldext2chn  34025  cos9thpiminplylem1  34079  unitdivcld  34198  sqsscirc1  34205  xrge0iifcnv  34230  xrge0iifiso  34232  rezh  34266  esumcvgsum  34385  voliune  34526  volfiniune  34527  sibfinima  34636  sitmcl  34648  0rrv  34748  coinfliprv  34780  ballotlem2  34786  ballotlem4  34796  ballotlemi1  34800  ballotlemic  34804  signsply0  34845  signswch  34855  signstf  34860  signstf0  34862  signstfveq0  34871  signlem0  34881  signshf  34882  itgexpif  34900  hgt750lemd  34942  hgt750lem  34945  hgt750lem2  34946  hgt750leme  34952  iisconn  35602  iillysconn  35603  cvmliftlem10  35644  fz0n  36081  bcneg1  36086  nn0prpwlem  36682  dnizeq0  36913  dnizphlfeqhlf  36914  knoppndvlem13  36962  cnndvlem1  36975  bj-pinftyccb  37713  bj-minftyccb  37717  bj-pinftynminfty  37719  taupilemrplb  37812  irrdiff  37818  sin2h  38109  tan2h  38111  ptrecube  38119  poimirlem16  38135  poimirlem17  38136  poimirlem20  38139  poimirlem22  38141  poimirlem23  38142  poimirlem29  38148  poimirlem31  38150  poimir  38152  heicant  38154  mblfinlem2  38157  ismblfin  38160  ovoliunnfl  38161  voliunnfl  38163  volsupnfl  38164  mbfposadd  38166  itg2addnclem  38170  itg2addnclem2  38171  ibladdnclem  38175  itgaddnclem2  38178  iblabsnclem  38182  iblmulc2nc  38184  itgmulc2nclem2  38186  itgabsnc  38188  ftc1cnnclem  38190  ftc1anclem5  38196  ftc1anclem8  38199  asindmre  38202  dvasin  38203  areacirclem4  38210  areacirc  38212  isbnd3  38283  ssbnd  38287  prdsbnd  38292  bfplem2  38322  bfp  38323  renegclALT  39587  0cnALT3  42869  sn-1ne2  42880  itrere  42927  oexpreposd  42931  tan3rdpi  42961  asin1half  42966  readvrec2  42970  sn-00idlem2  43008  sn-00idlem3  43009  sn-00id  43010  sn-0tie0  43073  sn-ltaddpos  43075  sn-ltaddneg  43076  relt0neg1  43078  sn-nnne0  43082  reelznn0nn  43083  sn-0lt1  43097  sn-inelr  43109  sn-itrere  43110  sn-retire  43111  pellexlem6  43411  elpell14qr2  43439  oddcomabszz  43521  zindbi  43523  jm2.24  43540  acongeq  43560  arearect  43792  areaquad  43793  reabsifneg  44208  reabsifnpos  44209  reabsifpos  44210  reabsifnneg  44211  imsqrtvalex  44222  relexp01min  44289  imo72b2lem2  44743  imo72b2lem1  44745  imo72b2  44748  dvconstbi  44910  binomcxplemnn0  44925  binomcxplemdvbinom  44929  binomcxplemcvg  44930  binomcxplemnotnn0  44932  sineq0ALT  45512  halffl  45875  ren0  45976  rexanuz2nf  46066  sqrlearg  46129  limsup10ex  46347  dvnmptdivc  46512  dvnmul  46517  itgsin0pilem1  46524  itgsinexplem1  46528  itgsinexp  46529  iblempty  46539  stoweidlem17  46591  stoweidlem36  46610  stoweidlem55  46629  wallispilem1  46639  wallispilem2  46640  wallispilem4  46642  stirlinglem4  46651  stirlinglem13  46660  stirlinglem14  46661  stirlingr  46664  dirker2re  46666  dirkerdenne0  46667  dirkerre  46669  dirkertrigeqlem1  46672  dirkercncflem2  46678  dirkercncflem4  46680  fourierdlem11  46692  fourierdlem16  46697  fourierdlem21  46702  fourierdlem22  46703  fourierdlem41  46722  fourierdlem42  46723  fourierdlem62  46742  fourierdlem66  46746  fourierdlem79  46759  fourierdlem83  46763  fourierdlem94  46774  fourierdlem102  46782  fourierdlem103  46783  fourierdlem104  46784  fourierdlem111  46791  fourierdlem112  46792  fourierdlem113  46793  fourierdlem114  46794  sqwvfoura  46802  sqwvfourb  46803  fourierswlem  46804  fouriersw  46805  etransclem23  46831  etransclem44  46852  etransclem46  46854  salexct3  46916  salgensscntex  46918  sge0rnn0  46942  sge00  46950  0ome  47103  ovn0lem  47139  ovnhoilem1  47175  smfmullem1  47365  smfmullem2  47366  smfmullem3  47367  smfmullem4  47368  squeezedltsq  47464  goldrapos  47477  zm1nn  47896  sqrtnegnre  47901  flmrecm1  47937  m1mod0mod1  47954  muldvdsfacgt  47980  fmtnoprmfac2lem1  48175  31prm  48206  mod42tp1mod8  48211  nfermltl2rev  48365  tgblthelfgott  48437  usgrexmpl1lem  48643  usgrexmpl2lem  48648  usgrexmpl2nb0  48653  usgrexmpl2nb5  48658  usgrexmpl2trifr  48659  gpgusgralem  48678  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  pgnbgreunbgrlem2lem3  48738  gpg5edgnedg  48752  altgsumbcALT  48975  expnegico01  49140  dignnld  49225  eenglngeehlnmlem1  49359  line2ylem  49373  line2y  49377  itsclc0yqsollem2  49385  icccldii  49540  i0oii  49541  sepfsepc  49549  ex-gt  50349