Theorem 0re 11320

Description: The number 0 is real. Remark: the first step could also be ax-icn 11269. See also 0reALT 11665. (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 11268	. 2 ⊢ 1 ∈ ℂ
2		cnre 11315	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11281	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11293	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2851	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 248	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3166	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 16	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 486	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3158	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∃wrex 3089  (class class class)co 7427  ℂcc 11208  ℝcr 11209  0cc0 11210  1c1 11211  ici 11212   + caddc 11213   · cmul 11215

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-addrcl 11271  ax-rnegex 11281  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-clel 2838  df-rex 3090

This theorem is used by:  0red  11321  pr01ssre  11322  0xr  11366  axmulgt0  11394  ne0gt0  11425  00id  11495  mul02lem1  11496  mul02lem2  11497  mul02  11498  addrid  11500  ltaddneg  11536  addgt0  11812  addgegt0  11813  addgtge0  11814  addge0  11815  ltaddpos  11816  ltneg  11826  leneg  11829  lt0neg1  11832  lt0neg2  11833  le0neg1  11834  le0neg2  11835  addge01  11836  suble0  11840  mulge0  11844  msqge0  11847  0le1  11849  relin01  11850  gt0ne0i  11861  lt0ne0d  11891  elimge0  12166  ltm1  12169  recgt0  12173  prodgt0  12174  lemul1a  12181  ltmul12a  12183  lemul12a  12185  gt0div  12193  ge0div  12194  mulge0b  12197  lediv12a  12220  recgt1i  12224  recreclt  12226  ledivp1  12229  squeeze0  12230  recgt0ii  12233  ledivp1i  12252  ltdivp1i  12253  fimaxre2  12272  inelr  12320  crne0  12323  indf  12336  indfval  12337  nnge1  12376  nngt0  12379  nnnle0  12381  nnne0  12382  nnrecgt0  12391  0le0  12454  0le2  12455  halfge0  12572  nn0ssre  12620  nn0ge0  12641  nn0nlt0  12642  nn0le0eq0  12644  0mnnnnn0  12648  elnnnn0b  12660  elnnnn0c  12661  nn0sub  12666  elnnz  12713  0z  12714  elnn0z  12716  elnnz1  12732  recnz  12784  gtndiv  12786  fnn0ind  12808  10re  12847  rpge0  13144  rpneg  13164  0nrp  13167  0ltpnf  13261  mnflt0  13264  qsqueeze  13341  xneg0  13352  xaddrid  13381  xnn0xadd0  13387  xmulpnf1  13414  xlemul1a  13428  xadddi  13435  xrsupsslem  13447  xrinfmsslem  13448  elrege0  13595  0e0icopnf  13599  elicc01  13607  0elunit  13610  unitssre  13640  nnge2recico01  13648  0nelfz1  13686  fzpreddisj  13717  fz0to4untppr  13774  fz0to5un2tp  13775  nn0p1elfzo  13847  ico01fl0  13969  rpsup  14016  modelico  14031  0mod  14052  1mod  14053  le2sq2  14288  expubnd  14331  sqlecan  14363  bernneq2  14384  expnbnd  14386  expnlbnd  14387  expmulnbnd  14389  discr1  14393  discr  14394  faclbnd  14444  faclbnd3  14446  faclbnd6  14453  bcval4  14461  bcval5  14472  bcpasc  14475  hasheq0  14517  hashneq0  14518  hashnn0n0nn  14545  hashgt12el  14577  hashgt12el2  14578  hashge2el2dif  14635  lsw0  14720  swrdccatin2  14889  pfxccatin12lem3  14892  sgnclre  15267  sgnnbi  15269  sgnpbi  15270  reim0  15297  re0  15331  im0  15332  rei  15335  imi  15336  cj0  15337  sqeqd  15345  rennim  15418  cnpart  15419  sqrt0  15420  01sqrexlem4  15424  resqrex  15429  sqrtgt0  15437  sqrt00  15442  sqrtneglem  15445  sqrt9  15452  sqrt2gt1lt2  15453  leabs  15478  absor  15479  max0add  15489  eqsqrt2d  15548  sqrtpclii  15562  rlimconst  15723  rlimrege0  15758  lo1mul  15807  iserge0  15840  fsum00  15977  isumless  16026  georeclim  16053  geo2sum  16054  geoisumr  16059  0.999...  16062  cvgrat  16064  fprodge0  16172  bpoly4  16237  cos0  16330  ef01bndlem  16364  sin01bnd  16365  cos01bnd  16366  cos2bnd  16368  sin01gt0  16370  cos01gt0  16371  sincos2sgn  16374  sin4lt0  16375  absef  16377  absefib  16378  efieq1re  16379  epos  16387  rpnnen2lem2  16395  rpnnen2lem3  16396  rpnnen2lem4  16397  rpnnen2lem9  16402  ruclem6  16415  dvdslelem  16491  divalglem1  16576  divalglem5  16579  divalglem6  16580  flodddiv4  16597  sadcadd  16640  gcdn0gt0  16702  nn0seqcvgd  16757  algcvgblem  16764  algcvga  16766  pythagtriplem12  17016  pythagtriplem13  17017  pythagtriplem14  17018  pythagtriplem16  17020  prmreclem4  17109  prmreclem5  17110  prmreclem6  17111  1arith  17117  ramz  17215  chnub  18808  mulgnegnn  19306  subgmulg  19363  srgbinomlem4  20467  isabvd  21081  abvtrivd  21101  rge0srg  21756  xrs1mnd  21758  xrs10  21759  psgnodpmr  21908  re0g  21930  psrbaglesupp  22242  psdmvr  22502  mnfnei  23551  imasdsf1olem  24704  ssblps  24753  ssbl  24754  xmeter  24764  dscmet  24903  dscopn  24904  nmoi  25059  nmoeq0  25067  0nghm  25072  idnghm  25074  cnbl0  25104  xrsxmet  25141  metdseq0  25186  iicmp  25219  iiconn  25220  iihalf1  25264  elii1  25268  icopnfcnv  25275  icopnfhmeo  25276  iccpnfcnv  25277  xrhmeo  25279  xrhmph  25280  htpycc  25313  reparphti  25330  pcoval1  25346  pco0  25347  pcoval2  25349  pcocn  25350  pcohtpylem  25352  pcopt  25355  pcopt2  25356  pcoass  25357  pcorevlem  25359  reust  25714  recusp  25715  rrx0el  25731  minveclem4c  25758  minveclem2  25759  minveclem3b  25761  minveclem4  25765  minveclem7  25768  pjthlem1  25770  cniccbdd  25794  ovolunnul  25833  ovoliunnul  25840  ovolicc1  25849  ovolre  25858  iccvolcl  25900  ovolioo  25901  ioovolcl  25903  ioorcl  25910  vitalilem4  25944  vitalilem5  25945  vitali  25946  ismbf  25961  mbfmulc2lem  25980  mbfpos  25984  mbfposr  25985  i1f0  26020  i1f1  26023  itg1addlem2  26030  itg1addlem4  26032  itg1addlem5  26033  mbfi1fseqlem4  26051  mbfi1fseqlem5  26052  mbfi1flimlem  26055  xrge0f  26064  itg2ge0  26068  itg2const  26073  itg2mulc  26080  itg2splitlem  26081  itg2gt0  26093  itg2cnlem1  26094  ibl0  26119  iblrelem  26123  iblposlem  26124  iblpos  26125  iblre  26126  itgreval  26129  itgneg  26136  iblss  26137  i1fibl  26140  itgitg1  26141  itgle  26142  itgeqa  26146  itgless  26149  iblconst  26150  itgconst  26151  ibladdlem  26152  itgaddlem2  26156  iblabslem  26160  iblabsr  26162  iblmulc2  26163  itgmulc2lem2  26165  itgabs  26167  itgsplit  26168  bddmulibl  26171  dvferm1  26317  dvferm2  26319  dvferm  26320  dvlip  26325  c1lip1  26329  dveq0  26332  dv11cn  26333  dvne0  26343  ftc1lem4  26371  ply1divex  26467  dgrco  26606  plyrecj  26610  plyn0mulidp  26614  vieta1lem2  26646  aalioulem2  26672  aalioulem3  26673  pserulm  26761  psercnlem2  26763  psercnlem1  26764  psercn  26765  abelth  26780  reeff1olem  26785  reeff1o  26786  pilem2  26791  pilem3  26792  pipos  26799  pige0  26800  sinhalfpilem  26804  sincosq1sgn  26839  sincosq2sgn  26840  coseq00topi  26843  coseq0negpitopi  26844  tangtx  26846  tanabsge  26847  sinq12ge0  26849  sinq34lt0t  26850  cosq14ge0  26852  sincos4thpi  26854  sincos6thpi  26856  pige3ALT  26860  sineq0  26864  cosordlem  26870  cosord  26871  cos11  26873  sinord  26874  recosf1o  26875  resinf1o  26876  tanord1  26877  tanord  26878  tanregt0  26879  efif1olem4  26885  efifo  26887  relogrn  26901  log1  26925  logi  26927  logneg  26928  argregt0  26950  argrege0  26951  argimgt0  26952  logneg2  26955  logdivlti  26960  logdivlt  26961  ellogdm  26979  logdmn0  26980  logdmnrp  26981  logcnlem3  26984  dvloglem  26988  logdmopn  26989  logf1o2  26990  dvlog2lem  26992  efopnlem1  26996  logtayl  27000  recxpcl  27015  cxpge0  27023  cxple2  27037  cxple2a  27039  cxpsqrtlem  27042  cxpcn3  27088  cxpaddlelem  27091  cxpaddle  27092  loglesqrt  27101  logbrec  27122  ang180lem3  27151  ang180lem4  27152  asinneg  27226  asin1  27234  reasinsin  27236  acosbnd  27240  atan0  27248  atanrecl  27251  atanlogaddlem  27253  atanlogsublem  27255  atanlogsub  27256  atantan  27263  atanbnd  27266  atan1  27268  atans2  27271  ressatans  27274  log2cnv  27284  log2tlbnd  27285  log2ub  27289  log2le1  27290  rlimcnp  27305  rlimcnp2  27306  o1cxp  27314  jensen  27328  amgm  27330  emgt0  27346  harmonicbnd3  27347  harmoniclbnd  27348  harmonicbnd4  27350  zetacvg  27354  eldmgm  27361  lgamgulmlem2  27369  basellem3  27422  basellem8  27427  efnnfsumcl  27442  ppisval  27443  vmage0  27460  chpge0  27465  efchtdvds  27498  ppiltx  27516  ppiub  27543  chpeq0  27547  chteq0  27548  chtleppi  27549  chpchtsum  27558  chpub  27559  dchr1re  27602  bcmono  27616  efexple  27620  bposlem1  27623  bposlem4  27626  bposlem5  27627  bposlem7  27629  bposlem8  27630  bposlem9  27631  lgsval2lem  27646  lgsval4a  27658  lgsneg  27660  lgsdilem  27663  lgsdir2lem1  27664  2lgsoddprmlem3a  27749  2lgsoddprmlem3b  27750  2lgsoddprmlem3c  27751  2lgsoddprmlem3d  27752  rplogsumlem2  27824  rpvmasumlem  27826  dchrisum0flblem1  27847  dchrisum0flblem2  27848  dchrisum0fno1  27850  rplogsum  27866  logdivsum  27872  mulog2sumlem2  27874  selberg2lem  27889  logdivbnd  27895  pntrsumo1  27904  pntrlog2bndlem4  27919  pntrlog2bndlem5  27920  pntpbnd1  27925  pntpbnd2  27926  pntlem3  27948  pntleml  27950  ostth2  27976  trgcgrg  28990  ttgcontlem1  29474  axlowdimlem1  29532  axlowdimlem6  29537  axlowdimlem7  29538  axlowdimlem10  29541  axlowdim1  29549  axlowdim2  29550  axlowdim  29551  elntg2  29575  umgrislfupgrlem  29712  lfgrnloop  29715  lfuhgr1v0e  29847  usgrexmplef  29852  pthdlem2  30366  crctcshwlkn0lem7  30417  rusgrnumwwlks  30578  clwwlkn0  30631  konigsberg  30870  ex-po  31048  ex-sqrt  31067  ex-gcd  31070  nvz0  31282  0blo  31406  nmlno0lem  31407  nmblolbii  31413  siilem2  31466  minvecolem2  31489  minvecolem3  31490  minvecolem4c  31493  minvecolem4  31494  minvecolem5  31495  minvecolem7  31497  htthlem  31531  hiidge0  31712  normlem6  31729  normgt0  31741  norm-i  31743  normpyc  31760  bcsiALT  31793  pjhthlem1  32005  pjneli  32337  nmlnop0iALT  32609  unopbd  32629  nmbdoplbi  32638  nmcoplbi  32642  nmbdfnlbi  32663  nmbdfnlb  32664  nmcfnlbi  32666  cnlnadjlem7  32687  nmopcoi  32709  branmfn  32719  leopmul  32748  nmopleid  32753  pjbdlni  32763  pjnormssi  32782  stle0i  32853  cdj3lem1  33048  xaddeq0  33398  expgt0b  33461  dp20u  33497  dp20h  33498  dp2clq  33500  dp2lt10  33503  dp2lt  33504  dp0u  33520  dplti  33524  dpexpp1  33527  xdiv0  33548  xrge0slmod  33962  evl1deg3  34163  fldext2chn  34413  cos9thpiminplylem1  34467  unitdivcld  34586  sqsscirc1  34593  xrge0iifcnv  34618  xrge0iifiso  34620  rezh  34654  esumcvgsum  34773  voliune  34915  volfiniune  34916  sibfinima  35024  sitmcl  35036  0rrv  35136  coinfliprv  35168  ballotlem2  35174  ballotlem4  35184  ballotlemi1  35188  ballotlemic  35192  signsply0  35233  signswch  35243  signstf  35248  signstf0  35250  signstfveq0  35259  signlem0  35269  signshf  35270  itgexpif  35288  hgt750lemd  35330  hgt750lem  35333  hgt750lem2  35334  hgt750leme  35340  iisconn  36138  iillysconn  36139  cvmliftlem10  36180  fz0n  36623  bcneg1  36628  nn0prpwlem  37237  dnizeq0  37468  dnizphlfeqhlf  37469  knoppndvlem13  37517  cnndvlem1  37530  bj-pinftyccb  38282  bj-minftyccb  38286  bj-pinftynminfty  38288  taupilemrplb  38381  irrdiff  38387  sin2h  38673  tan2h  38675  ptrecube  38678  poimirlem16  38694  poimirlem17  38695  poimirlem20  38698  poimirlem22  38700  poimirlem23  38701  poimirlem29  38707  poimirlem31  38709  poimir  38711  heicant  38713  mblfinlem2  38716  ismblfin  38719  ovoliunnfl  38720  voliunnfl  38722  volsupnfl  38723  mbfposadd  38725  itg2addnclem  38729  itg2addnclem2  38730  ibladdnclem  38734  itgaddnclem2  38737  iblabsnclem  38741  iblmulc2nc  38743  itgmulc2nclem2  38745  itgabsnc  38747  ftc1cnnclem  38749  ftc1anclem5  38755  ftc1anclem8  38758  asindmre  38761  dvasin  38762  areacirclem4  38769  areacirc  38771  isbnd3  38858  ssbnd  38862  prdsbnd  38867  bfplem2  38897  bfp  38898  renegclALT  40160  0cnALT3  43444  sn-1ne2  43470  itrere  43515  oexpreposd  43519  tan3rdpi  43543  asin1half  43548  readvrec2  43552  sn-00idlem2  43590  sn-00idlem3  43591  sn-00id  43592  sn-0tie0  43655  sn-ltaddpos  43657  sn-ltaddneg  43658  relt0neg1  43660  sn-nnne0  43664  reelznn0nn  43665  sn-0lt1  43679  sn-inelr  43691  sn-itrere  43692  sn-retire  43693  pellexlem6  43981  elpell14qr2  44009  oddcomabszz  44091  zindbi  44093  jm2.24  44110  acongeq  44130  arearect  44357  areaquad  44358  reabsifneg  44772  reabsifnpos  44773  reabsifpos  44774  reabsifnneg  44775  imsqrtvalex  44786  relexp01min  44853  imo72b2lem2  45307  imo72b2lem1  45309  imo72b2  45312  dvconstbi  45458  binomcxplemnn0  45473  binomcxplemdvbinom  45477  binomcxplemcvg  45478  binomcxplemnotnn0  45480  sineq0ALT  46058  halffl  46451  ren0  46551  rexanuz2nf  46641  sqrlearg  46704  limsup10ex  46922  dvnmptdivc  47087  dvnmul  47092  itgsin0pilem1  47099  itgsinexplem1  47103  itgsinexp  47104  iblempty  47114  stoweidlem17  47166  stoweidlem36  47185  stoweidlem55  47204  wallispilem1  47214  wallispilem2  47215  wallispilem4  47217  stirlinglem4  47226  stirlinglem13  47235  stirlinglem14  47236  stirlingr  47239  dirker2re  47241  dirkerdenne0  47242  dirkerre  47244  dirkertrigeqlem1  47247  dirkercncflem2  47253  dirkercncflem4  47255  fourierdlem11  47267  fourierdlem16  47272  fourierdlem21  47277  fourierdlem22  47278  fourierdlem41  47297  fourierdlem42  47298  fourierdlem62  47317  fourierdlem66  47321  fourierdlem79  47334  fourierdlem83  47338  fourierdlem94  47349  fourierdlem102  47357  fourierdlem103  47358  fourierdlem104  47359  fourierdlem111  47366  fourierdlem112  47367  fourierdlem113  47368  fourierdlem114  47369  sqwvfoura  47377  sqwvfourb  47378  fourierswlem  47379  fouriersw  47380  etransclem23  47406  etransclem44  47427  etransclem46  47429  salexct3  47491  salgensscntex  47493  sge0rnn0  47517  sge00  47525  0ome  47678  ovn0lem  47714  ovnhoilem1  47750  smfmullem1  47940  smfmullem2  47941  smfmullem3  47942  smfmullem4  47943  squeezedltsq  48051  goldrapos  48069  goldratval  48075  zm1nn  48511  sqrtnegnre  48516  flmrecm1  48552  m1mod0mod1  48569  muldvdsfacgt  48595  fmtnoprmfac2lem1  48790  31prm  48821  mod42tp1mod8  48826  nfermltl2rev  48980  tgblthelfgott  49052  usgrexmpl1lem  49258  usgrexmpl2lem  49263  usgrexmpl2nb0  49268  usgrexmpl2nb5  49273  usgrexmpl2trifr  49274  gpgusgralem  49293  pgnbgreunbgrlem2lem1  49351  pgnbgreunbgrlem2lem2  49352  pgnbgreunbgrlem2lem3  49353  gpg5edgnedg  49367  altgsumbcALT  49604  expnegico01  49769  dignnld  49854  eenglngeehlnmlem1  49989  line2ylem  50002  line2  50003  line2x  50005  line2y  50006  itsclc0yqsollem2  50014  icccldii  50172  i0oii  50173  sepfsepc  50181  ex-gt  51035