Theorem 0re 11134

Description: The number 0 is real. Remark: the first step could also be ax-icn 11085. See also 0reALT 11478. (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 11084	. 2 ⊢ 1 ∈ ℂ
2		cnre 11129	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11097	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11109	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2824	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3137	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3129	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∃wrex 3060  (class class class)co 7358  ℂcc 11024  ℝcr 11025  0cc0 11026  1c1 11027  ici 11028   + caddc 11029   · cmul 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addrcl 11087  ax-rnegex 11097  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-rex 3061

This theorem is referenced by:  0red  11135  0xr  11179  axmulgt0  11207  ne0gt0  11238  00id  11308  mul02lem1  11309  mul02lem2  11310  mul02  11311  addrid  11313  ltaddneg  11349  addgt0  11623  addgegt0  11624  addgtge0  11625  addge0  11626  ltaddpos  11627  ltneg  11637  leneg  11640  lt0neg1  11643  lt0neg2  11644  le0neg1  11645  le0neg2  11646  addge01  11647  suble0  11651  mulge0  11655  msqge0  11658  0le1  11660  relin01  11661  gt0ne0i  11672  lt0ne0d  11702  elimge0  11980  ltm1  11983  recgt0  11987  prodgt0  11988  lemul1a  11995  ltmul12a  11997  lemul12a  11999  mulgt1OLD  12000  gt0div  12008  ge0div  12009  mulge0b  12012  lediv12a  12035  recgt1i  12039  recreclt  12041  ledivp1  12044  squeeze0  12045  recgt0ii  12048  ledivp1i  12067  ltdivp1i  12068  fimaxre2  12087  inelr  12135  crne0  12138  nnge1  12173  nngt0  12176  nnnle0  12178  nnne0  12179  nnrecgt0  12188  0le0  12246  halfge0  12357  nn0ssre  12405  nn0ge0  12426  nn0nlt0  12427  nn0le0eq0  12429  0mnnnnn0  12433  elnnnn0b  12445  elnnnn0c  12446  nn0sub  12451  elnnz  12498  0z  12499  elnn0z  12501  elnnz1  12517  recnz  12567  gtndiv  12569  fnn0ind  12591  10re  12626  rpge0  12919  rpneg  12939  0nrp  12942  0ltpnf  13036  mnflt0  13039  qsqueeze  13116  xneg0  13127  xaddrid  13156  xnn0xadd0  13162  xmulpnf1  13189  xlemul1a  13203  xadddi  13210  xrsupsslem  13222  xrinfmsslem  13223  elrege0  13370  0e0icopnf  13374  elicc01  13382  0elunit  13385  unitssre  13415  0nelfz1  13459  fzpreddisj  13489  fz0to4untppr  13546  fz0to5un2tp  13547  nn0p1elfzo  13618  ico01fl0  13739  rpsup  13786  modelico  13801  0mod  13822  1mod  13823  le2sq2  14058  expubnd  14101  sqlecan  14132  bernneq2  14153  expnbnd  14155  expnlbnd  14156  expmulnbnd  14158  discr1  14162  discr  14163  faclbnd  14213  faclbnd3  14215  faclbnd6  14222  bcval4  14230  bcval5  14241  bcpasc  14244  hasheq0  14286  hashneq0  14287  hashnn0n0nn  14314  hashgt12el  14345  hashgt12el2  14346  hashge2el2dif  14403  lsw0  14488  swrdccatin2  14652  pfxccatin12lem3  14655  reim0  15041  re0  15075  im0  15076  rei  15079  imi  15080  cj0  15081  sqeqd  15089  rennim  15162  cnpart  15163  sqrt0  15164  01sqrexlem4  15168  resqrex  15173  sqrtgt0  15181  sqrt00  15186  sqrtneglem  15189  sqrt9  15196  sqrt2gt1lt2  15197  leabs  15222  absor  15223  max0add  15233  eqsqrt2d  15292  sqrtpclii  15306  rlimconst  15467  rlimrege0  15502  lo1mul  15551  iserge0  15584  fsum00  15721  isumless  15768  arisum2  15784  georeclim  15795  geo2sum  15796  geoisumr  15801  0.999...  15804  cvgrat  15806  fprodge0  15916  bpoly4  15982  cos0  16075  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  cos2bnd  16113  sin01gt0  16115  cos01gt0  16116  sincos2sgn  16119  sin4lt0  16120  absef  16122  absefib  16123  efieq1re  16124  epos  16132  rpnnen2lem2  16140  rpnnen2lem3  16141  rpnnen2lem4  16142  rpnnen2lem9  16147  ruclem6  16160  dvdslelem  16236  divalglem1  16321  divalglem5  16324  divalglem6  16325  flodddiv4  16342  sadcadd  16385  gcdn0gt0  16445  nn0seqcvgd  16497  algcvgblem  16504  algcvga  16506  pythagtriplem12  16754  pythagtriplem13  16755  pythagtriplem14  16756  pythagtriplem16  16758  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  1arith  16855  ramz  16953  chnub  18545  mulgnegnn  19014  subgmulg  19070  srgbinomlem4  20164  isabvd  20745  abvtrivd  20765  rge0srg  21393  xrs1mnd  21395  xrs10  21396  psgnodpmr  21545  re0g  21567  psrbaglesupp  21878  psdmvr  22112  mnfnei  23165  imasdsf1olem  24317  ssblps  24366  ssbl  24367  xmeter  24377  dscmet  24516  dscopn  24517  nmoi  24672  nmoeq0  24680  0nghm  24685  idnghm  24687  cnbl0  24717  xrsxmet  24754  metdseq0  24799  iicmp  24835  iiconn  24836  iihalf1  24881  iihalf1cnOLD  24883  elii1  24887  icopnfcnv  24896  icopnfhmeo  24897  iccpnfcnv  24898  xrhmeo  24900  xrhmph  24901  htpycc  24935  reparphti  24952  reparphtiOLD  24953  pcoval1  24969  pco0  24970  pcoval2  24972  pcocn  24973  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  reust  25337  recusp  25338  rrx0el  25354  minveclem4c  25381  minveclem2  25382  minveclem3b  25384  minveclem4  25388  minveclem7  25391  pjthlem1  25393  cniccbdd  25418  ovolunnul  25457  ovoliunnul  25464  ovolicc1  25473  ovolre  25482  iccvolcl  25524  ovolioo  25525  ioovolcl  25527  ioorcl  25534  vitalilem4  25568  vitalilem5  25569  vitali  25570  ismbf  25585  mbfmulc2lem  25604  mbfpos  25608  mbfposr  25609  i1f0  25644  i1f1  25647  itg1addlem2  25654  itg1addlem4  25656  itg1addlem5  25657  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfi1flimlem  25679  xrge0f  25688  itg2ge0  25692  itg2const  25697  itg2mulc  25704  itg2splitlem  25705  itg2gt0  25717  itg2cnlem1  25718  ibl0  25744  iblrelem  25748  iblposlem  25749  iblpos  25750  iblre  25751  itgreval  25754  itgneg  25761  iblss  25762  i1fibl  25765  itgitg1  25766  itgle  25767  itgeqa  25771  itgless  25774  iblconst  25775  itgconst  25776  ibladdlem  25777  itgaddlem2  25781  iblabslem  25785  iblabsr  25787  iblmulc2  25788  itgmulc2lem2  25790  itgabs  25792  itgsplit  25793  bddmulibl  25796  dvferm1  25945  dvferm2  25947  dvferm  25948  dvlip  25954  c1lip1  25958  dveq0  25961  dv11cn  25962  dvne0  25972  ftc1lem4  26002  ply1divex  26098  dgrco  26237  plyrecj  26243  vieta1lem2  26275  aalioulem2  26297  aalioulem3  26298  pserulm  26387  psercnlem2  26390  psercnlem1  26391  psercn  26392  abelth  26407  reeff1olem  26412  reeff1o  26413  pilem2  26418  pilem3  26419  pipos  26424  sinhalfpilem  26428  sincosq1sgn  26463  sincosq2sgn  26464  coseq00topi  26467  coseq0negpitopi  26468  tangtx  26470  tanabsge  26471  sinq12ge0  26473  sinq34lt0t  26474  cosq14ge0  26476  sincos4thpi  26478  sincos6thpi  26481  pige3ALT  26485  sineq0  26489  cosordlem  26495  cosord  26496  cos0pilt1  26497  cos11  26498  sinord  26499  recosf1o  26500  resinf1o  26501  tanord1  26502  tanord  26503  tanregt0  26504  efif1olem4  26510  efifo  26512  relogrn  26526  log1  26550  logi  26552  logneg  26553  argregt0  26575  argrege0  26576  argimgt0  26577  logneg2  26580  logdivlti  26585  logdivlt  26586  ellogdm  26604  logdmn0  26605  logdmnrp  26606  logcnlem3  26609  dvloglem  26613  logdmopn  26614  logf1o2  26615  dvlog2lem  26617  efopnlem1  26621  logtayl  26625  recxpcl  26640  cxpge0  26648  cxple2  26662  cxple2a  26664  cxpsqrtlem  26667  cxpcn3  26714  cxpaddlelem  26717  cxpaddle  26718  loglesqrt  26727  logbrec  26748  ang180lem3  26777  ang180lem4  26778  asinneg  26852  asin1  26860  reasinsin  26862  acosbnd  26866  atan0  26874  atanrecl  26877  atanlogaddlem  26879  atanlogsublem  26881  atanlogsub  26882  atantan  26889  atanbnd  26892  atan1  26894  atans2  26897  ressatans  26900  log2cnv  26910  log2tlbnd  26911  log2ub  26915  log2le1  26916  rlimcnp  26931  rlimcnp2  26932  o1cxp  26941  jensen  26955  amgm  26957  emgt0  26973  harmonicbnd3  26974  harmoniclbnd  26975  harmonicbnd4  26977  zetacvg  26981  eldmgm  26988  lgamgulmlem2  26996  basellem3  27049  basellem8  27054  efnnfsumcl  27069  ppisval  27070  vmage0  27087  chpge0  27092  efchtdvds  27125  ppiltx  27143  ppiub  27171  chpeq0  27175  chteq0  27176  chtleppi  27177  chpchtsum  27186  chpub  27187  dchr1re  27230  bcmono  27244  efexple  27248  bposlem1  27251  bposlem4  27254  bposlem5  27255  bposlem7  27257  bposlem8  27258  bposlem9  27259  lgsval2lem  27274  lgsval4a  27286  lgsneg  27288  lgsdilem  27291  lgsdir2lem1  27292  2lgsoddprmlem3a  27377  2lgsoddprmlem3b  27378  2lgsoddprmlem3c  27379  2lgsoddprmlem3d  27380  rplogsumlem2  27452  rpvmasumlem  27454  dchrisum0flblem1  27475  dchrisum0flblem2  27476  dchrisum0fno1  27478  rplogsum  27494  logdivsum  27500  mulog2sumlem2  27502  selberg2lem  27517  logdivbnd  27523  pntrsumo1  27532  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntpbnd1  27553  pntpbnd2  27554  pntlem3  27576  pntleml  27578  ostth2  27604  trgcgrg  28587  ttgcontlem1  28957  axlowdimlem1  29015  axlowdimlem6  29020  axlowdimlem7  29021  axlowdimlem10  29024  axlowdim1  29032  axlowdim2  29033  axlowdim  29034  elntg2  29058  umgrislfupgrlem  29195  lfgrnloop  29198  lfuhgr1v0e  29327  usgrexmplef  29332  pthdlem2  29841  crctcshwlkn0lem7  29889  rusgrnumwwlks  30050  clwwlkn0  30103  konigsberg  30332  ex-po  30510  ex-sqrt  30529  ex-gcd  30532  nvz0  30743  0blo  30867  nmlno0lem  30868  nmblolbii  30874  siilem2  30927  minvecolem2  30950  minvecolem3  30951  minvecolem4c  30954  minvecolem4  30955  minvecolem5  30956  minvecolem7  30958  htthlem  30992  hiidge0  31173  normlem6  31190  normgt0  31202  norm-i  31204  normpyc  31221  bcsiALT  31254  pjhthlem1  31466  pjneli  31798  nmlnop0iALT  32070  unopbd  32090  nmbdoplbi  32099  nmcoplbi  32103  nmbdfnlbi  32124  nmbdfnlb  32125  nmcfnlbi  32127  cnlnadjlem7  32148  nmopcoi  32170  branmfn  32180  leopmul  32209  nmopleid  32214  pjbdlni  32224  pjnormssi  32243  stle0i  32314  cdj3lem1  32509  xaddeq0  32833  expgt0b  32897  pr01ssre  32905  sgnclre  32913  sgnnbi  32919  sgnpbi  32920  indf  32934  indfval  32935  dp20u  32959  dp20h  32960  dp2clq  32962  dp2lt10  32965  dp2lt  32966  dp0u  32982  dplti  32986  dpexpp1  32989  xdiv0  33010  xrge0slmod  33429  evl1deg3  33659  fldext2chn  33885  cos9thpiminplylem1  33939  unitdivcld  34058  sqsscirc1  34065  xrge0iifcnv  34090  xrge0iifiso  34092  rezh  34126  esumcvgsum  34245  voliune  34386  volfiniune  34387  sibfinima  34496  sitmcl  34508  0rrv  34608  coinfliprv  34640  ballotlem2  34646  ballotlem4  34656  ballotlemi1  34660  ballotlemic  34664  plymulx0  34704  signsply0  34708  signswch  34718  signstf  34723  signstf0  34725  signstfveq0  34734  signlem0  34744  signshf  34745  itgexpif  34763  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  iisconn  35446  iillysconn  35447  cvmliftlem10  35488  fz0n  35925  bcneg1  35930  nn0prpwlem  36516  dnizeq0  36675  dnizphlfeqhlf  36676  knoppndvlem13  36724  cnndvlem1  36737  bj-pinftyccb  37426  bj-minftyccb  37430  bj-pinftynminfty  37432  taupilemrplb  37525  irrdiff  37531  sin2h  37811  tan2h  37813  ptrecube  37821  poimirlem16  37837  poimirlem17  37838  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem29  37850  poimirlem31  37852  poimir  37854  heicant  37856  mblfinlem2  37859  ismblfin  37862  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  mbfposadd  37868  itg2addnclem  37872  itg2addnclem2  37873  ibladdnclem  37877  itgaddnclem2  37880  iblabsnclem  37884  iblmulc2nc  37886  itgmulc2nclem2  37888  itgabsnc  37890  ftc1cnnclem  37892  ftc1anclem5  37898  ftc1anclem8  37901  asindmre  37904  dvasin  37905  areacirclem4  37912  areacirc  37914  isbnd3  37985  ssbnd  37989  prdsbnd  37994  bfplem2  38024  bfp  38025  renegclALT  39223  0cnALT3  42508  sn-1ne2  42520  itrere  42573  oexpreposd  42577  tan3rdpi  42607  asin1half  42612  readvrec2  42616  sn-00idlem2  42654  sn-00idlem3  42655  sn-00id  42656  sn-0tie0  42706  sn-ltaddpos  42708  sn-ltaddneg  42709  relt0neg1  42711  sn-nnne0  42715  reelznn0nn  42716  sn-0lt1  42730  sn-inelr  42742  sn-itrere  42743  sn-retire  42744  pellexlem6  43076  elpell14qr2  43104  oddcomabszz  43186  zindbi  43188  jm2.24  43205  acongeq  43225  arearect  43457  areaquad  43458  reabsifneg  43873  reabsifnpos  43874  reabsifpos  43875  reabsifnneg  43876  imsqrtvalex  43887  relexp01min  43954  imo72b2lem2  44408  imo72b2lem1  44410  imo72b2  44413  dvconstbi  44575  binomcxplemnn0  44590  binomcxplemdvbinom  44594  binomcxplemcvg  44595  binomcxplemnotnn0  44597  sineq0ALT  45177  halffl  45544  ren0  45646  rexanuz2nf  45736  sqrlearg  45799  limsup10ex  46017  dvnmptdivc  46182  dvnmul  46187  itgsin0pilem1  46194  itgsinexplem1  46198  itgsinexp  46199  iblempty  46209  stoweidlem17  46261  stoweidlem36  46280  stoweidlem55  46299  wallispilem1  46309  wallispilem2  46310  wallispilem4  46312  stirlinglem4  46321  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  stirlingr  46334  dirker2re  46336  dirkerdenne0  46337  dirkerre  46339  dirkertrigeqlem1  46342  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem11  46362  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem41  46392  fourierdlem42  46393  fourierdlem48  46398  fourierdlem62  46412  fourierdlem66  46416  fourierdlem79  46429  fourierdlem83  46433  fourierdlem94  46444  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  fourierdlem113  46463  fourierdlem114  46464  sqwvfoura  46472  sqwvfourb  46473  fourierswlem  46474  fouriersw  46475  etransclem23  46501  etransclem44  46522  etransclem46  46524  salexct3  46586  salgensscntex  46588  sge0rnn0  46612  sge00  46620  0ome  46773  ovn0lem  46809  ovnhoilem1  46845  smfmullem1  47035  smfmullem2  47036  smfmullem3  47037  smfmullem4  47038  squeezedltsq  47132  zm1nn  47548  sqrtnegnre  47553  m1mod0mod1  47600  fmtnoprmfac2lem1  47812  31prm  47843  mod42tp1mod8  47848  nfermltl2rev  47989  tgblthelfgott  48061  usgrexmpl1lem  48267  usgrexmpl2lem  48272  usgrexmpl2nb0  48277  usgrexmpl2nb5  48282  usgrexmpl2trifr  48283  gpgusgralem  48302  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  gpg5edgnedg  48376  altgsumbcALT  48599  expnegico01  48764  dignnld  48849  eenglngeehlnmlem1  48983  line2ylem  48997  line2y  49001  itsclc0yqsollem2  49009  icccldii  49164  i0oii  49165  sepfsepc  49173  ex-gt  49973