Theorem 0re 11235

Description: The number 0 is real. Remark: the first step could also be ax-icn 11186. See also 0reALT 11578. (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 11185	. 2 ⊢ 1 ∈ ℂ
2		cnre 11230	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11198	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11210	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2822	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3141	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3133	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∃wrex 3060  (class class class)co 7403  ℂcc 11125  ℝcr 11126  0cc0 11127  1c1 11128  ici 11129   + caddc 11130   · cmul 11132

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addrcl 11188  ax-rnegex 11198  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809  df-rex 3061

This theorem is referenced by:  0red  11236  0xr  11280  axmulgt0  11307  ne0gt0  11338  00id  11408  mul02lem1  11409  mul02lem2  11410  mul02  11411  addrid  11413  ltaddneg  11449  addgt0  11721  addgegt0  11722  addgtge0  11723  addge0  11724  ltaddpos  11725  ltneg  11735  leneg  11738  lt0neg1  11741  lt0neg2  11742  le0neg1  11743  le0neg2  11744  addge01  11745  suble0  11749  mulge0  11753  msqge0  11756  0le1  11758  relin01  11759  gt0ne0i  11770  gt0ne0d  11799  lt0ne0d  11800  elimge0  12078  ltm1  12081  recgt0  12085  prodgt0  12086  lemul1a  12093  ltmul12a  12095  lemul12a  12097  mulgt1OLD  12098  gt0div  12106  ge0div  12107  mulge0b  12110  lediv12a  12133  recgt1i  12137  recreclt  12139  ledivp1  12142  squeeze0  12143  recgt0ii  12146  ledivp1i  12165  ltdivp1i  12166  fimaxre2  12185  inelr  12228  crne0  12231  nnge1  12266  nngt0  12269  nnnle0  12271  nnne0  12272  nnrecgt0  12281  0le0  12339  neg1lt0  12355  halfge0  12455  nn0ssre  12503  nn0ge0  12524  nn0nlt0  12525  nn0le0eq0  12527  0mnnnnn0  12531  elnnnn0b  12543  elnnnn0c  12544  nn0sub  12549  elnnz  12596  0z  12597  elnn0z  12599  elnnz1  12616  recnz  12666  gtndiv  12668  fnn0ind  12690  10re  12725  rpge0  13020  rpneg  13039  0nrp  13042  0ltpnf  13136  mnflt0  13139  qsqueeze  13215  xneg0  13226  xaddrid  13255  xnn0xadd0  13261  xmulpnf1  13288  xlemul1a  13302  xadddi  13309  xrsupsslem  13321  xrinfmsslem  13322  elrege0  13469  0e0icopnf  13473  elicc01  13481  0elunit  13484  unitssre  13514  0nelfz1  13558  fzpreddisj  13588  fz0to4untppr  13645  fz0to5un2tp  13646  nn0p1elfzo  13717  ico01fl0  13834  rpsup  13881  modelico  13896  0mod  13917  1mod  13918  le2sq2  14151  expubnd  14194  sqlecan  14225  bernneq2  14246  expnbnd  14248  expnlbnd  14249  expmulnbnd  14251  discr1  14255  discr  14256  faclbnd  14306  faclbnd3  14308  faclbnd6  14315  bcval4  14323  bcval5  14334  bcpasc  14337  hasheq0  14379  hashneq0  14380  hashnn0n0nn  14407  hashgt12el  14438  hashgt12el2  14439  hashge2el2dif  14496  lsw0  14581  swrdccatin2  14745  pfxccatin12lem3  14748  reim0  15135  re0  15169  im0  15170  rei  15173  imi  15174  cj0  15175  sqeqd  15183  rennim  15256  cnpart  15257  sqrt0  15258  01sqrexlem4  15262  resqrex  15267  sqrtgt0  15275  sqrt00  15280  sqrtneglem  15283  sqrt9  15290  sqrt2gt1lt2  15291  leabs  15316  absor  15317  max0add  15327  eqsqrt2d  15385  sqrtpclii  15399  rlimconst  15558  rlimrege0  15593  lo1mul  15642  iserge0  15675  fsum00  15812  isumless  15859  arisum2  15875  georeclim  15886  geo2sum  15887  geoisumr  15892  0.999...  15895  cvgrat  15897  fprodge0  16007  bpoly4  16073  cos0  16166  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  cos2bnd  16204  sin01gt0  16206  cos01gt0  16207  sincos2sgn  16210  sin4lt0  16211  absef  16213  absefib  16214  efieq1re  16215  epos  16223  rpnnen2lem2  16231  rpnnen2lem3  16232  rpnnen2lem4  16233  rpnnen2lem9  16238  ruclem6  16251  dvdslelem  16326  divalglem1  16411  divalglem5  16414  divalglem6  16415  flodddiv4  16432  sadcadd  16475  gcdn0gt0  16535  nn0seqcvgd  16587  algcvgblem  16594  algcvga  16596  pythagtriplem12  16844  pythagtriplem13  16845  pythagtriplem14  16846  pythagtriplem16  16848  prmreclem4  16937  prmreclem5  16938  prmreclem6  16939  1arith  16945  ramz  17043  mulgnegnn  19065  subgmulg  19121  srgbinomlem4  20187  isabvd  20770  abvtrivd  20790  xrs1mnd  21370  xrs10  21371  rge0srg  21404  psgnodpmr  21548  re0g  21570  psrbaglesupp  21880  psdmvr  22105  mnfnei  23157  imasdsf1olem  24310  ssblps  24359  ssbl  24360  xmeter  24370  dscmet  24509  dscopn  24510  nmoi  24665  nmoeq0  24673  0nghm  24678  idnghm  24680  cnbl0  24710  xrsxmet  24747  metdseq0  24792  iicmp  24828  iiconn  24829  iihalf1  24874  iihalf1cnOLD  24876  elii1  24880  icopnfcnv  24889  icopnfhmeo  24890  iccpnfcnv  24891  xrhmeo  24893  xrhmph  24894  htpycc  24928  reparphti  24945  reparphtiOLD  24946  pcoval1  24962  pco0  24963  pcoval2  24965  pcocn  24966  pcohtpylem  24968  pcopt  24971  pcopt2  24972  pcoass  24973  pcorevlem  24975  reust  25331  recusp  25332  rrx0el  25348  minveclem4c  25375  minveclem2  25376  minveclem3b  25378  minveclem4  25382  minveclem7  25385  pjthlem1  25387  cniccbdd  25412  ovolunnul  25451  ovoliunnul  25458  ovolicc1  25467  ovolre  25476  iccvolcl  25518  ovolioo  25519  ioovolcl  25521  ioorcl  25528  vitalilem4  25562  vitalilem5  25563  vitali  25564  ismbf  25579  mbfmulc2lem  25598  mbfpos  25602  mbfposr  25603  i1f0  25638  i1f1  25641  itg1addlem2  25648  itg1addlem4  25650  itg1addlem5  25651  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1flimlem  25673  xrge0f  25682  itg2ge0  25686  itg2const  25691  itg2mulc  25698  itg2splitlem  25699  itg2gt0  25711  itg2cnlem1  25712  ibl0  25738  iblrelem  25742  iblposlem  25743  iblpos  25744  iblre  25745  itgreval  25748  itgneg  25755  iblss  25756  i1fibl  25759  itgitg1  25760  itgle  25761  itgeqa  25765  itgless  25768  iblconst  25769  itgconst  25770  ibladdlem  25771  itgaddlem2  25775  iblabslem  25779  iblabsr  25781  iblmulc2  25782  itgmulc2lem2  25784  itgabs  25786  itgsplit  25787  bddmulibl  25790  dvferm1  25939  dvferm2  25941  dvferm  25942  dvlip  25948  c1lip1  25952  dveq0  25955  dv11cn  25956  dvne0  25966  ftc1lem4  25996  ply1divex  26092  dgrco  26231  plyrecj  26237  vieta1lem2  26269  aalioulem2  26291  aalioulem3  26292  pserulm  26381  psercnlem2  26384  psercnlem1  26385  psercn  26386  abelth  26401  reeff1olem  26406  reeff1o  26407  pilem2  26412  pilem3  26413  pipos  26418  sinhalfpilem  26422  sincosq1sgn  26457  sincosq2sgn  26458  coseq00topi  26461  coseq0negpitopi  26462  tangtx  26464  tanabsge  26465  sinq12ge0  26467  sinq34lt0t  26468  cosq14ge0  26470  sincos4thpi  26472  sincos6thpi  26475  pige3ALT  26479  sineq0  26483  cosordlem  26489  cosord  26490  cos0pilt1  26491  cos11  26492  sinord  26493  recosf1o  26494  resinf1o  26495  tanord1  26496  tanord  26497  tanregt0  26498  efif1olem4  26504  efifo  26506  relogrn  26520  log1  26544  logi  26546  logneg  26547  argregt0  26569  argrege0  26570  argimgt0  26571  logneg2  26574  logdivlti  26579  logdivlt  26580  ellogdm  26598  logdmn0  26599  logdmnrp  26600  logcnlem3  26603  dvloglem  26607  logdmopn  26608  logf1o2  26609  dvlog2lem  26611  efopnlem1  26615  logtayl  26619  recxpcl  26634  cxpge0  26642  cxple2  26656  cxple2a  26658  cxpsqrtlem  26661  cxpcn3  26708  cxpaddlelem  26711  cxpaddle  26712  loglesqrt  26721  logbrec  26742  ang180lem3  26771  ang180lem4  26772  asinneg  26846  asin1  26854  reasinsin  26856  acosbnd  26860  atan0  26868  atanrecl  26871  atanlogaddlem  26873  atanlogsublem  26875  atanlogsub  26876  atantan  26883  atanbnd  26886  atan1  26888  atans2  26891  ressatans  26894  log2cnv  26904  log2tlbnd  26905  log2ub  26909  log2le1  26910  rlimcnp  26925  rlimcnp2  26926  o1cxp  26935  jensen  26949  amgm  26951  emgt0  26967  harmonicbnd3  26968  harmoniclbnd  26969  harmonicbnd4  26971  zetacvg  26975  eldmgm  26982  lgamgulmlem2  26990  basellem3  27043  basellem8  27048  efnnfsumcl  27063  ppisval  27064  vmage0  27081  chpge0  27086  efchtdvds  27119  ppiltx  27137  ppiub  27165  chpeq0  27169  chteq0  27170  chtleppi  27171  chpchtsum  27180  chpub  27181  dchr1re  27224  bcmono  27238  efexple  27242  bposlem1  27245  bposlem4  27248  bposlem5  27249  bposlem7  27251  bposlem8  27252  bposlem9  27253  lgsval2lem  27268  lgsval4a  27280  lgsneg  27282  lgsdilem  27285  lgsdir2lem1  27286  2lgsoddprmlem3a  27371  2lgsoddprmlem3b  27372  2lgsoddprmlem3c  27373  2lgsoddprmlem3d  27374  rplogsumlem2  27446  rpvmasumlem  27448  dchrisum0flblem1  27469  dchrisum0flblem2  27470  dchrisum0fno1  27472  rplogsum  27488  logdivsum  27494  mulog2sumlem2  27496  selberg2lem  27511  logdivbnd  27517  pntrsumo1  27526  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntpbnd1  27547  pntpbnd2  27548  pntlem3  27570  pntleml  27572  ostth2  27598  trgcgrg  28440  ttgcontlem1  28810  axlowdimlem1  28867  axlowdimlem6  28872  axlowdimlem7  28873  axlowdimlem10  28876  axlowdim1  28884  axlowdim2  28885  axlowdim  28886  elntg2  28910  umgrislfupgrlem  29047  lfgrnloop  29050  lfuhgr1v0e  29179  usgrexmplef  29184  pthdlem2  29696  crctcshwlkn0lem7  29744  rusgrnumwwlks  29902  clwwlkn0  29955  konigsberg  30184  ex-po  30362  ex-sqrt  30381  ex-gcd  30384  nvz0  30595  0blo  30719  nmlno0lem  30720  nmblolbii  30726  siilem2  30779  minvecolem2  30802  minvecolem3  30803  minvecolem4c  30806  minvecolem4  30807  minvecolem5  30808  minvecolem7  30810  htthlem  30844  hiidge0  31025  normlem6  31042  normgt0  31054  norm-i  31056  normpyc  31073  bcsiALT  31106  pjhthlem1  31318  pjneli  31650  nmlnop0iALT  31922  unopbd  31942  nmbdoplbi  31951  nmcoplbi  31955  nmbdfnlbi  31976  nmbdfnlb  31977  nmcfnlbi  31979  cnlnadjlem7  32000  nmopcoi  32022  branmfn  32032  leopmul  32061  nmopleid  32066  pjbdlni  32076  pjnormssi  32095  stle0i  32166  cdj3lem1  32361  xaddeq0  32676  expgt0b  32741  pr01ssre  32749  sgnclre  32757  sgnnbi  32763  sgnpbi  32764  indf  32778  indfval  32779  dp20u  32798  dp20h  32799  dp2clq  32801  dp2lt10  32804  dp2lt  32805  dp0u  32821  dplti  32825  dpexpp1  32828  xdiv0  32849  chnub  32938  xrge0slmod  33309  evl1deg3  33537  fldext2chn  33708  cos9thpiminplylem1  33762  unitdivcld  33878  sqsscirc1  33885  xrge0iifcnv  33910  xrge0iifiso  33912  rezh  33946  esumcvgsum  34065  voliune  34206  volfiniune  34207  sibfinima  34317  sitmcl  34329  0rrv  34429  coinfliprv  34461  ballotlem2  34467  ballotlem4  34477  ballotlemi1  34481  ballotlemic  34485  plymulx0  34525  signsply0  34529  signswch  34539  signstf  34544  signstf0  34546  signstfveq0  34555  signlem0  34565  signshf  34566  itgexpif  34584  hgt750lemd  34626  hgt750lem  34629  hgt750lem2  34630  hgt750leme  34636  iisconn  35220  iillysconn  35221  cvmliftlem10  35262  fz0n  35694  bcneg1  35699  nn0prpwlem  36286  dnizeq0  36439  dnizphlfeqhlf  36440  knoppndvlem13  36488  cnndvlem1  36501  bj-pinftyccb  37185  bj-minftyccb  37189  bj-pinftynminfty  37191  taupilemrplb  37284  irrdiff  37290  sin2h  37580  tan2h  37582  ptrecube  37590  poimirlem16  37606  poimirlem17  37607  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem29  37619  poimirlem31  37621  poimir  37623  heicant  37625  mblfinlem2  37628  ismblfin  37631  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  mbfposadd  37637  itg2addnclem  37641  itg2addnclem2  37642  ibladdnclem  37646  itgaddnclem2  37649  iblabsnclem  37653  iblmulc2nc  37655  itgmulc2nclem2  37657  itgabsnc  37659  ftc1cnnclem  37661  ftc1anclem5  37667  ftc1anclem8  37670  asindmre  37673  dvasin  37674  areacirclem4  37681  areacirc  37683  isbnd3  37754  ssbnd  37758  prdsbnd  37763  bfplem2  37793  bfp  37794  renegclALT  38927  2xp3dxp2ge1d  42200  factwoffsmonot  42201  0cnALT3  42251  sn-1ne2  42262  itrere  42314  oexpreposd  42318  tan3rdpi  42346  asin1half  42347  readvrec2  42351  sn-00idlem2  42389  sn-00idlem3  42390  sn-00id  42391  sn-0tie0  42429  sn-ltaddpos  42431  sn-ltaddneg  42432  relt0neg1  42434  sn-nnne0  42438  reelznn0nn  42439  sn-0lt1  42453  sn-inelr  42457  sn-itrere  42458  sn-retire  42459  pellexlem6  42804  elpell14qr2  42832  oddcomabszz  42915  zindbi  42917  jm2.24  42934  acongeq  42954  arearect  43186  areaquad  43187  reabsifneg  43603  reabsifnpos  43604  reabsifpos  43605  reabsifnneg  43606  imsqrtvalex  43617  relexp01min  43684  imo72b2lem2  44138  imo72b2lem1  44140  imo72b2  44143  dvconstbi  44306  binomcxplemnn0  44321  binomcxplemdvbinom  44325  binomcxplemcvg  44326  binomcxplemnotnn0  44328  sineq0ALT  44909  halffl  45273  ren0  45377  rexanuz2nf  45467  sqrlearg  45530  limsup10ex  45750  dvnmptdivc  45915  dvnmul  45920  itgsin0pilem1  45927  itgsinexplem1  45931  itgsinexp  45932  iblempty  45942  stoweidlem17  45994  stoweidlem36  46013  stoweidlem55  46032  wallispilem1  46042  wallispilem2  46043  wallispilem4  46045  stirlinglem4  46054  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  stirlingr  46067  dirker2re  46069  dirkerdenne0  46070  dirkerre  46072  dirkertrigeqlem1  46075  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem11  46095  fourierdlem16  46100  fourierdlem21  46105  fourierdlem22  46106  fourierdlem41  46125  fourierdlem42  46126  fourierdlem48  46131  fourierdlem62  46145  fourierdlem66  46149  fourierdlem79  46162  fourierdlem83  46166  fourierdlem94  46177  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  fourierdlem114  46197  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  etransclem23  46234  etransclem44  46255  etransclem46  46257  salexct3  46319  salgensscntex  46321  sge0rnn0  46345  sge00  46353  0ome  46506  ovn0lem  46542  ovnhoilem1  46578  smfmullem1  46768  smfmullem2  46769  smfmullem3  46770  smfmullem4  46771  squeezedltsq  46866  zm1nn  47279  sqrtnegnre  47284  m1mod0mod1  47331  fmtnoprmfac2lem1  47528  31prm  47559  mod42tp1mod8  47564  nfermltl2rev  47705  tgblthelfgott  47777  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2nb0  47983  usgrexmpl2nb5  47988  usgrexmpl2trifr  47989  gpgusgralem  48008  altgsumbcALT  48276  expnegico01  48442  dignnld  48531  eenglngeehlnmlem1  48665  line2ylem  48679  line2y  48683  itsclc0yqsollem2  48691  icccldii  48841  i0oii  48842  sepfsepc  48850  ex-gt  49540