Theorem 0re 11114

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∃wrex 3056  (class class class)co 7346  ℂcc 11004  ℝcr 11005  0cc0 11006  1c1 11007  ici 11008   + caddc 11009   · cmul 11011

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 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-addrcl 11067  ax-rnegex 11077  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-rex 3057

This theorem is referenced by:  0red  11115  0xr  11159  axmulgt0  11187  ne0gt0  11218  00id  11288  mul02lem1  11289  mul02lem2  11290  mul02  11291  addrid  11293  ltaddneg  11329  addgt0  11603  addgegt0  11604  addgtge0  11605  addge0  11606  ltaddpos  11607  ltneg  11617  leneg  11620  lt0neg1  11623  lt0neg2  11624  le0neg1  11625  le0neg2  11626  addge01  11627  suble0  11631  mulge0  11635  msqge0  11638  0le1  11640  relin01  11641  gt0ne0i  11652  lt0ne0d  11682  elimge0  11960  ltm1  11963  recgt0  11967  prodgt0  11968  lemul1a  11975  ltmul12a  11977  lemul12a  11979  mulgt1OLD  11980  gt0div  11988  ge0div  11989  mulge0b  11992  lediv12a  12015  recgt1i  12019  recreclt  12021  ledivp1  12024  squeeze0  12025  recgt0ii  12028  ledivp1i  12047  ltdivp1i  12048  fimaxre2  12067  inelr  12115  crne0  12118  nnge1  12153  nngt0  12156  nnnle0  12158  nnne0  12159  nnrecgt0  12168  0le0  12226  halfge0  12337  nn0ssre  12385  nn0ge0  12406  nn0nlt0  12407  nn0le0eq0  12409  0mnnnnn0  12413  elnnnn0b  12425  elnnnn0c  12426  nn0sub  12431  elnnz  12478  0z  12479  elnn0z  12481  elnnz1  12498  recnz  12548  gtndiv  12550  fnn0ind  12572  10re  12607  rpge0  12904  rpneg  12924  0nrp  12927  0ltpnf  13021  mnflt0  13024  qsqueeze  13100  xneg0  13111  xaddrid  13140  xnn0xadd0  13146  xmulpnf1  13173  xlemul1a  13187  xadddi  13194  xrsupsslem  13206  xrinfmsslem  13207  elrege0  13354  0e0icopnf  13358  elicc01  13366  0elunit  13369  unitssre  13399  0nelfz1  13443  fzpreddisj  13473  fz0to4untppr  13530  fz0to5un2tp  13531  nn0p1elfzo  13602  ico01fl0  13723  rpsup  13770  modelico  13785  0mod  13806  1mod  13807  le2sq2  14042  expubnd  14085  sqlecan  14116  bernneq2  14137  expnbnd  14139  expnlbnd  14140  expmulnbnd  14142  discr1  14146  discr  14147  faclbnd  14197  faclbnd3  14199  faclbnd6  14206  bcval4  14214  bcval5  14225  bcpasc  14228  hasheq0  14270  hashneq0  14271  hashnn0n0nn  14298  hashgt12el  14329  hashgt12el2  14330  hashge2el2dif  14387  lsw0  14472  swrdccatin2  14636  pfxccatin12lem3  14639  reim0  15025  re0  15059  im0  15060  rei  15063  imi  15064  cj0  15065  sqeqd  15073  rennim  15146  cnpart  15147  sqrt0  15148  01sqrexlem4  15152  resqrex  15157  sqrtgt0  15165  sqrt00  15170  sqrtneglem  15173  sqrt9  15180  sqrt2gt1lt2  15181  leabs  15206  absor  15207  max0add  15217  eqsqrt2d  15276  sqrtpclii  15290  rlimconst  15451  rlimrege0  15486  lo1mul  15535  iserge0  15568  fsum00  15705  isumless  15752  arisum2  15768  georeclim  15779  geo2sum  15780  geoisumr  15785  0.999...  15788  cvgrat  15790  fprodge0  15900  bpoly4  15966  cos0  16059  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  cos2bnd  16097  sin01gt0  16099  cos01gt0  16100  sincos2sgn  16103  sin4lt0  16104  absef  16106  absefib  16107  efieq1re  16108  epos  16116  rpnnen2lem2  16124  rpnnen2lem3  16125  rpnnen2lem4  16126  rpnnen2lem9  16131  ruclem6  16144  dvdslelem  16220  divalglem1  16305  divalglem5  16308  divalglem6  16309  flodddiv4  16326  sadcadd  16369  gcdn0gt0  16429  nn0seqcvgd  16481  algcvgblem  16488  algcvga  16490  pythagtriplem12  16738  pythagtriplem13  16739  pythagtriplem14  16740  pythagtriplem16  16742  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  1arith  16839  ramz  16937  chnub  18528  mulgnegnn  18997  subgmulg  19053  srgbinomlem4  20147  isabvd  20727  abvtrivd  20747  rge0srg  21375  xrs1mnd  21377  xrs10  21378  psgnodpmr  21527  re0g  21549  psrbaglesupp  21859  psdmvr  22084  mnfnei  23136  imasdsf1olem  24288  ssblps  24337  ssbl  24338  xmeter  24348  dscmet  24487  dscopn  24488  nmoi  24643  nmoeq0  24651  0nghm  24656  idnghm  24658  cnbl0  24688  xrsxmet  24725  metdseq0  24770  iicmp  24806  iiconn  24807  iihalf1  24852  iihalf1cnOLD  24854  elii1  24858  icopnfcnv  24867  icopnfhmeo  24868  iccpnfcnv  24869  xrhmeo  24871  xrhmph  24872  htpycc  24906  reparphti  24923  reparphtiOLD  24924  pcoval1  24940  pco0  24941  pcoval2  24943  pcocn  24944  pcohtpylem  24946  pcopt  24949  pcopt2  24950  pcoass  24951  pcorevlem  24953  reust  25308  recusp  25309  rrx0el  25325  minveclem4c  25352  minveclem2  25353  minveclem3b  25355  minveclem4  25359  minveclem7  25362  pjthlem1  25364  cniccbdd  25389  ovolunnul  25428  ovoliunnul  25435  ovolicc1  25444  ovolre  25453  iccvolcl  25495  ovolioo  25496  ioovolcl  25498  ioorcl  25505  vitalilem4  25539  vitalilem5  25540  vitali  25541  ismbf  25556  mbfmulc2lem  25575  mbfpos  25579  mbfposr  25580  i1f0  25615  i1f1  25618  itg1addlem2  25625  itg1addlem4  25627  itg1addlem5  25628  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  mbfi1flimlem  25650  xrge0f  25659  itg2ge0  25663  itg2const  25668  itg2mulc  25675  itg2splitlem  25676  itg2gt0  25688  itg2cnlem1  25689  ibl0  25715  iblrelem  25719  iblposlem  25720  iblpos  25721  iblre  25722  itgreval  25725  itgneg  25732  iblss  25733  i1fibl  25736  itgitg1  25737  itgle  25738  itgeqa  25742  itgless  25745  iblconst  25746  itgconst  25747  ibladdlem  25748  itgaddlem2  25752  iblabslem  25756  iblabsr  25758  iblmulc2  25759  itgmulc2lem2  25761  itgabs  25763  itgsplit  25764  bddmulibl  25767  dvferm1  25916  dvferm2  25918  dvferm  25919  dvlip  25925  c1lip1  25929  dveq0  25932  dv11cn  25933  dvne0  25943  ftc1lem4  25973  ply1divex  26069  dgrco  26208  plyrecj  26214  vieta1lem2  26246  aalioulem2  26268  aalioulem3  26269  pserulm  26358  psercnlem2  26361  psercnlem1  26362  psercn  26363  abelth  26378  reeff1olem  26383  reeff1o  26384  pilem2  26389  pilem3  26390  pipos  26395  sinhalfpilem  26399  sincosq1sgn  26434  sincosq2sgn  26435  coseq00topi  26438  coseq0negpitopi  26439  tangtx  26441  tanabsge  26442  sinq12ge0  26444  sinq34lt0t  26445  cosq14ge0  26447  sincos4thpi  26449  sincos6thpi  26452  pige3ALT  26456  sineq0  26460  cosordlem  26466  cosord  26467  cos0pilt1  26468  cos11  26469  sinord  26470  recosf1o  26471  resinf1o  26472  tanord1  26473  tanord  26474  tanregt0  26475  efif1olem4  26481  efifo  26483  relogrn  26497  log1  26521  logi  26523  logneg  26524  argregt0  26546  argrege0  26547  argimgt0  26548  logneg2  26551  logdivlti  26556  logdivlt  26557  ellogdm  26575  logdmn0  26576  logdmnrp  26577  logcnlem3  26580  dvloglem  26584  logdmopn  26585  logf1o2  26586  dvlog2lem  26588  efopnlem1  26592  logtayl  26596  recxpcl  26611  cxpge0  26619  cxple2  26633  cxple2a  26635  cxpsqrtlem  26638  cxpcn3  26685  cxpaddlelem  26688  cxpaddle  26689  loglesqrt  26698  logbrec  26719  ang180lem3  26748  ang180lem4  26749  asinneg  26823  asin1  26831  reasinsin  26833  acosbnd  26837  atan0  26845  atanrecl  26848  atanlogaddlem  26850  atanlogsublem  26852  atanlogsub  26853  atantan  26860  atanbnd  26863  atan1  26865  atans2  26868  ressatans  26871  log2cnv  26881  log2tlbnd  26882  log2ub  26886  log2le1  26887  rlimcnp  26902  rlimcnp2  26903  o1cxp  26912  jensen  26926  amgm  26928  emgt0  26944  harmonicbnd3  26945  harmoniclbnd  26946  harmonicbnd4  26948  zetacvg  26952  eldmgm  26959  lgamgulmlem2  26967  basellem3  27020  basellem8  27025  efnnfsumcl  27040  ppisval  27041  vmage0  27058  chpge0  27063  efchtdvds  27096  ppiltx  27114  ppiub  27142  chpeq0  27146  chteq0  27147  chtleppi  27148  chpchtsum  27157  chpub  27158  dchr1re  27201  bcmono  27215  efexple  27219  bposlem1  27222  bposlem4  27225  bposlem5  27226  bposlem7  27228  bposlem8  27229  bposlem9  27230  lgsval2lem  27245  lgsval4a  27257  lgsneg  27259  lgsdilem  27262  lgsdir2lem1  27263  2lgsoddprmlem3a  27348  2lgsoddprmlem3b  27349  2lgsoddprmlem3c  27350  2lgsoddprmlem3d  27351  rplogsumlem2  27423  rpvmasumlem  27425  dchrisum0flblem1  27446  dchrisum0flblem2  27447  dchrisum0fno1  27449  rplogsum  27465  logdivsum  27471  mulog2sumlem2  27473  selberg2lem  27488  logdivbnd  27494  pntrsumo1  27503  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntpbnd1  27524  pntpbnd2  27525  pntlem3  27547  pntleml  27549  ostth2  27575  trgcgrg  28493  ttgcontlem1  28863  axlowdimlem1  28920  axlowdimlem6  28925  axlowdimlem7  28926  axlowdimlem10  28929  axlowdim1  28937  axlowdim2  28938  axlowdim  28939  elntg2  28963  umgrislfupgrlem  29100  lfgrnloop  29103  lfuhgr1v0e  29232  usgrexmplef  29237  pthdlem2  29746  crctcshwlkn0lem7  29794  rusgrnumwwlks  29955  clwwlkn0  30008  konigsberg  30237  ex-po  30415  ex-sqrt  30434  ex-gcd  30437  nvz0  30648  0blo  30772  nmlno0lem  30773  nmblolbii  30779  siilem2  30832  minvecolem2  30855  minvecolem3  30856  minvecolem4c  30859  minvecolem4  30860  minvecolem5  30861  minvecolem7  30863  htthlem  30897  hiidge0  31078  normlem6  31095  normgt0  31107  norm-i  31109  normpyc  31126  bcsiALT  31159  pjhthlem1  31371  pjneli  31703  nmlnop0iALT  31975  unopbd  31995  nmbdoplbi  32004  nmcoplbi  32008  nmbdfnlbi  32029  nmbdfnlb  32030  nmcfnlbi  32032  cnlnadjlem7  32053  nmopcoi  32075  branmfn  32085  leopmul  32114  nmopleid  32119  pjbdlni  32129  pjnormssi  32148  stle0i  32219  cdj3lem1  32414  xaddeq0  32736  expgt0b  32799  pr01ssre  32807  sgnclre  32815  sgnnbi  32821  sgnpbi  32822  indf  32836  indfval  32837  dp20u  32858  dp20h  32859  dp2clq  32861  dp2lt10  32864  dp2lt  32865  dp0u  32881  dplti  32885  dpexpp1  32888  xdiv0  32909  xrge0slmod  33313  evl1deg3  33541  fldext2chn  33741  cos9thpiminplylem1  33795  unitdivcld  33914  sqsscirc1  33921  xrge0iifcnv  33946  xrge0iifiso  33948  rezh  33982  esumcvgsum  34101  voliune  34242  volfiniune  34243  sibfinima  34352  sitmcl  34364  0rrv  34464  coinfliprv  34496  ballotlem2  34502  ballotlem4  34512  ballotlemi1  34516  ballotlemic  34520  plymulx0  34560  signsply0  34564  signswch  34574  signstf  34579  signstf0  34581  signstfveq0  34590  signlem0  34600  signshf  34601  itgexpif  34619  hgt750lemd  34661  hgt750lem  34664  hgt750lem2  34665  hgt750leme  34671  iisconn  35296  iillysconn  35297  cvmliftlem10  35338  fz0n  35775  bcneg1  35780  nn0prpwlem  36364  dnizeq0  36517  dnizphlfeqhlf  36518  knoppndvlem13  36566  cnndvlem1  36579  bj-pinftyccb  37263  bj-minftyccb  37267  bj-pinftynminfty  37269  taupilemrplb  37362  irrdiff  37368  sin2h  37658  tan2h  37660  ptrecube  37668  poimirlem16  37684  poimirlem17  37685  poimirlem20  37688  poimirlem22  37690  poimirlem23  37691  poimirlem29  37697  poimirlem31  37699  poimir  37701  heicant  37703  mblfinlem2  37706  ismblfin  37709  ovoliunnfl  37710  voliunnfl  37712  volsupnfl  37713  mbfposadd  37715  itg2addnclem  37719  itg2addnclem2  37720  ibladdnclem  37724  itgaddnclem2  37727  iblabsnclem  37731  iblmulc2nc  37733  itgmulc2nclem2  37735  itgabsnc  37737  ftc1cnnclem  37739  ftc1anclem5  37745  ftc1anclem8  37748  asindmre  37751  dvasin  37752  areacirclem4  37759  areacirc  37761  isbnd3  37832  ssbnd  37836  prdsbnd  37841  bfplem2  37871  bfp  37872  renegclALT  39010  0cnALT3  42294  sn-1ne2  42306  itrere  42359  oexpreposd  42363  tan3rdpi  42393  asin1half  42398  readvrec2  42402  sn-00idlem2  42440  sn-00idlem3  42441  sn-00id  42442  sn-0tie0  42492  sn-ltaddpos  42494  sn-ltaddneg  42495  relt0neg1  42497  sn-nnne0  42501  reelznn0nn  42502  sn-0lt1  42516  sn-inelr  42528  sn-itrere  42529  sn-retire  42530  pellexlem6  42875  elpell14qr2  42903  oddcomabszz  42985  zindbi  42987  jm2.24  43004  acongeq  43024  arearect  43256  areaquad  43257  reabsifneg  43673  reabsifnpos  43674  reabsifpos  43675  reabsifnneg  43676  imsqrtvalex  43687  relexp01min  43754  imo72b2lem2  44208  imo72b2lem1  44210  imo72b2  44213  dvconstbi  44375  binomcxplemnn0  44390  binomcxplemdvbinom  44394  binomcxplemcvg  44395  binomcxplemnotnn0  44397  sineq0ALT  44977  halffl  45345  ren0  45448  rexanuz2nf  45538  sqrlearg  45601  limsup10ex  45819  dvnmptdivc  45984  dvnmul  45989  itgsin0pilem1  45996  itgsinexplem1  46000  itgsinexp  46001  iblempty  46011  stoweidlem17  46063  stoweidlem36  46082  stoweidlem55  46101  wallispilem1  46111  wallispilem2  46112  wallispilem4  46114  stirlinglem4  46123  stirlinglem13  46132  stirlinglem14  46133  stirlinglem15  46134  stirlingr  46136  dirker2re  46138  dirkerdenne0  46139  dirkerre  46141  dirkertrigeqlem1  46144  dirkercncflem2  46150  dirkercncflem4  46152  fourierdlem11  46164  fourierdlem16  46169  fourierdlem21  46174  fourierdlem22  46175  fourierdlem41  46194  fourierdlem42  46195  fourierdlem48  46200  fourierdlem62  46214  fourierdlem66  46218  fourierdlem79  46231  fourierdlem83  46235  fourierdlem94  46246  fourierdlem102  46254  fourierdlem103  46255  fourierdlem104  46256  fourierdlem111  46263  fourierdlem112  46264  fourierdlem113  46265  fourierdlem114  46266  sqwvfoura  46274  sqwvfourb  46275  fourierswlem  46276  fouriersw  46277  etransclem23  46303  etransclem44  46324  etransclem46  46326  salexct3  46388  salgensscntex  46390  sge0rnn0  46414  sge00  46422  0ome  46575  ovn0lem  46611  ovnhoilem1  46647  smfmullem1  46837  smfmullem2  46838  smfmullem3  46839  smfmullem4  46840  squeezedltsq  46925  zm1nn  47341  sqrtnegnre  47346  m1mod0mod1  47393  fmtnoprmfac2lem1  47605  31prm  47636  mod42tp1mod8  47641  nfermltl2rev  47782  tgblthelfgott  47854  usgrexmpl1lem  48060  usgrexmpl2lem  48065  usgrexmpl2nb0  48070  usgrexmpl2nb5  48075  usgrexmpl2trifr  48076  gpgusgralem  48095  pgnbgreunbgrlem2lem1  48153  pgnbgreunbgrlem2lem2  48154  pgnbgreunbgrlem2lem3  48155  gpg5edgnedg  48169  altgsumbcALT  48392  expnegico01  48558  dignnld  48643  eenglngeehlnmlem1  48777  line2ylem  48791  line2y  48795  itsclc0yqsollem2  48803  icccldii  48958  i0oii  48959  sepfsepc  48967  ex-gt  49768