Theorem 0re 11205

Description: The number 0 is real. Remark: the first step could also be ax-icn 11154. See also 0reALT 11550. (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 11153	. 2 ⊢ 1 ∈ ℂ
2		cnre 11200	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11166	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11178	. . . . . . 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 485	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3158	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∃wrex 3089  (class class class)co 7410  ℂcc 11093  ℝcr 11094  0cc0 11095  1c1 11096  ici 11097   + caddc 11098   · cmul 11100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-addrcl 11156  ax-rnegex 11166  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-rex 3090

This theorem is referenced by:  0red  11206  pr01ssre  11207  0xr  11251  axmulgt0  11279  ne0gt0  11310  00id  11380  mul02lem1  11381  mul02lem2  11382  mul02  11383  addrid  11385  ltaddneg  11421  addgt0  11695  addgegt0  11696  addgtge0  11697  addge0  11698  ltaddpos  11699  ltneg  11709  leneg  11712  lt0neg1  11715  lt0neg2  11716  le0neg1  11717  le0neg2  11718  addge01  11719  suble0  11723  mulge0  11727  msqge0  11730  0le1  11732  relin01  11733  gt0ne0i  11744  lt0ne0d  11774  elimge0  12049  ltm1  12052  recgt0  12056  prodgt0  12057  lemul1a  12064  ltmul12a  12066  lemul12a  12068  gt0div  12076  ge0div  12077  mulge0b  12080  lediv12a  12103  recgt1i  12107  recreclt  12109  ledivp1  12112  squeeze0  12113  recgt0ii  12116  ledivp1i  12135  ltdivp1i  12136  fimaxre2  12155  inelr  12203  crne0  12206  indf  12219  indfval  12220  nnge1  12259  nngt0  12262  nnnle0  12264  nnne0  12265  nnrecgt0  12274  0le0  12337  0le2  12338  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  12615  recnz  12666  gtndiv  12668  fnn0ind  12690  10re  12729  rpge0  13025  rpneg  13045  0nrp  13048  0ltpnf  13142  mnflt0  13145  qsqueeze  13222  xneg0  13233  xaddrid  13262  xnn0xadd0  13268  xmulpnf1  13295  xlemul1a  13309  xadddi  13316  xrsupsslem  13328  xrinfmsslem  13329  elrege0  13476  0e0icopnf  13480  elicc01  13488  0elunit  13491  unitssre  13521  nnge2recico01  13529  0nelfz1  13566  fzpreddisj  13597  fz0to4untppr  13654  fz0to5un2tp  13655  nn0p1elfzo  13727  ico01fl0  13848  rpsup  13895  modelico  13910  0mod  13931  1mod  13932  le2sq2  14167  expubnd  14210  sqlecan  14241  bernneq2  14262  expnbnd  14264  expnlbnd  14265  expmulnbnd  14267  discr1  14271  discr  14272  faclbnd  14322  faclbnd3  14324  faclbnd6  14331  bcval4  14339  bcval5  14350  bcpasc  14353  hasheq0  14395  hashneq0  14396  hashnn0n0nn  14423  hashgt12el  14455  hashgt12el2  14456  hashge2el2dif  14513  lsw0  14598  swrdccatin2  14762  pfxccatin12lem3  14765  sgnclre  15135  sgnnbi  15137  sgnpbi  15138  reim0  15165  re0  15199  im0  15200  rei  15203  imi  15204  cj0  15205  sqeqd  15213  rennim  15286  cnpart  15287  sqrt0  15288  01sqrexlem4  15292  resqrex  15297  sqrtgt0  15305  sqrt00  15310  sqrtneglem  15313  sqrt9  15320  sqrt2gt1lt2  15321  leabs  15346  absor  15347  max0add  15357  eqsqrt2d  15416  sqrtpclii  15430  rlimconst  15591  rlimrege0  15626  lo1mul  15675  iserge0  15708  fsum00  15846  isumless  15895  arisum2  15911  georeclim  15922  geo2sum  15923  geoisumr  15928  0.999...  15931  cvgrat  15933  fprodge0  16043  bpoly4  16108  cos0  16201  ef01bndlem  16235  sin01bnd  16236  cos01bnd  16237  cos2bnd  16239  sin01gt0  16241  cos01gt0  16242  sincos2sgn  16245  sin4lt0  16246  absef  16248  absefib  16249  efieq1re  16250  epos  16258  rpnnen2lem2  16266  rpnnen2lem3  16267  rpnnen2lem4  16268  rpnnen2lem9  16273  ruclem6  16286  dvdslelem  16362  divalglem1  16447  divalglem5  16450  divalglem6  16451  flodddiv4  16468  sadcadd  16511  gcdn0gt0  16571  nn0seqcvgd  16623  algcvgblem  16630  algcvga  16632  pythagtriplem12  16881  pythagtriplem13  16882  pythagtriplem14  16883  pythagtriplem16  16885  prmreclem4  16974  prmreclem5  16975  prmreclem6  16976  1arith  16982  ramz  17080  chnub  18673  mulgnegnn  19145  subgmulg  19202  srgbinomlem4  20306  isabvd  20915  abvtrivd  20935  rge0srg  21588  xrs1mnd  21590  xrs10  21591  psgnodpmr  21740  re0g  21762  psrbaglesupp  22072  psdmvr  22332  mnfnei  23378  imasdsf1olem  24530  ssblps  24579  ssbl  24580  xmeter  24590  dscmet  24729  dscopn  24730  nmoi  24885  nmoeq0  24893  0nghm  24898  idnghm  24900  cnbl0  24930  xrsxmet  24967  metdseq0  25012  iicmp  25045  iiconn  25046  iihalf1  25090  elii1  25094  icopnfcnv  25101  icopnfhmeo  25102  iccpnfcnv  25103  xrhmeo  25105  xrhmph  25106  htpycc  25139  reparphti  25156  pcoval1  25172  pco0  25173  pcoval2  25175  pcocn  25176  pcohtpylem  25178  pcopt  25181  pcopt2  25182  pcoass  25183  pcorevlem  25185  reust  25540  recusp  25541  rrx0el  25557  minveclem4c  25584  minveclem2  25585  minveclem3b  25587  minveclem4  25591  minveclem7  25594  pjthlem1  25596  cniccbdd  25620  ovolunnul  25659  ovoliunnul  25666  ovolicc1  25675  ovolre  25684  iccvolcl  25726  ovolioo  25727  ioovolcl  25729  ioorcl  25736  vitalilem4  25770  vitalilem5  25771  vitali  25772  ismbf  25787  mbfmulc2lem  25806  mbfpos  25810  mbfposr  25811  i1f0  25846  i1f1  25849  itg1addlem2  25856  itg1addlem4  25858  itg1addlem5  25859  mbfi1fseqlem4  25877  mbfi1fseqlem5  25878  mbfi1flimlem  25881  xrge0f  25890  itg2ge0  25894  itg2const  25899  itg2mulc  25906  itg2splitlem  25907  itg2gt0  25919  itg2cnlem1  25920  ibl0  25946  iblrelem  25950  iblposlem  25951  iblpos  25952  iblre  25953  itgreval  25956  itgneg  25963  iblss  25964  i1fibl  25967  itgitg1  25968  itgle  25969  itgeqa  25973  itgless  25976  iblconst  25977  itgconst  25978  ibladdlem  25979  itgaddlem2  25983  iblabslem  25987  iblabsr  25989  iblmulc2  25990  itgmulc2lem2  25992  itgabs  25994  itgsplit  25995  bddmulibl  25998  dvferm1  26144  dvferm2  26146  dvferm  26147  dvlip  26152  c1lip1  26156  dveq0  26159  dv11cn  26160  dvne0  26170  ftc1lem4  26198  ply1divex  26294  dgrco  26432  plyrecj  26438  plyn0mulidp  26442  vieta1lem2  26472  aalioulem2  26496  aalioulem3  26497  pserulm  26585  psercnlem2  26587  psercnlem1  26588  psercn  26589  abelth  26604  reeff1olem  26609  reeff1o  26610  pilem2  26615  pilem3  26616  pipos  26623  pige0  26624  sinhalfpilem  26628  sincosq1sgn  26663  sincosq2sgn  26664  coseq00topi  26667  coseq0negpitopi  26668  tangtx  26670  tanabsge  26671  sinq12ge0  26673  sinq34lt0t  26674  cosq14ge0  26676  sincos4thpi  26678  sincos6thpi  26681  pige3ALT  26685  sineq0  26689  cosordlem  26695  cosord  26696  cos0pilt1  26697  cos11  26698  sinord  26699  recosf1o  26700  resinf1o  26701  tanord1  26702  tanord  26703  tanregt0  26704  efif1olem4  26710  efifo  26712  relogrn  26726  log1  26750  logi  26752  logneg  26753  argregt0  26775  argrege0  26776  argimgt0  26777  logneg2  26780  logdivlti  26785  logdivlt  26786  ellogdm  26804  logdmn0  26805  logdmnrp  26806  logcnlem3  26809  dvloglem  26813  logdmopn  26814  logf1o2  26815  dvlog2lem  26817  efopnlem1  26821  logtayl  26825  recxpcl  26840  cxpge0  26848  cxple2  26862  cxple2a  26864  cxpsqrtlem  26867  cxpcn3  26913  cxpaddlelem  26916  cxpaddle  26917  loglesqrt  26926  logbrec  26947  ang180lem3  26976  ang180lem4  26977  asinneg  27051  asin1  27059  reasinsin  27061  acosbnd  27065  atan0  27073  atanrecl  27076  atanlogaddlem  27078  atanlogsublem  27080  atanlogsub  27081  atantan  27088  atanbnd  27091  atan1  27093  atans2  27096  ressatans  27099  log2cnv  27109  log2tlbnd  27110  log2ub  27114  log2le1  27115  rlimcnp  27130  rlimcnp2  27131  o1cxp  27139  jensen  27153  amgm  27155  emgt0  27171  harmonicbnd3  27172  harmoniclbnd  27173  harmonicbnd4  27175  zetacvg  27179  eldmgm  27186  lgamgulmlem2  27194  basellem3  27247  basellem8  27252  efnnfsumcl  27267  ppisval  27268  vmage0  27285  chpge0  27290  efchtdvds  27323  ppiltx  27341  ppiub  27368  chpeq0  27372  chteq0  27373  chtleppi  27374  chpchtsum  27383  chpub  27384  dchr1re  27427  bcmono  27441  efexple  27445  bposlem1  27448  bposlem4  27451  bposlem5  27452  bposlem7  27454  bposlem8  27455  bposlem9  27456  lgsval2lem  27471  lgsval4a  27483  lgsneg  27485  lgsdilem  27488  lgsdir2lem1  27489  2lgsoddprmlem3a  27574  2lgsoddprmlem3b  27575  2lgsoddprmlem3c  27576  2lgsoddprmlem3d  27577  rplogsumlem2  27649  rpvmasumlem  27651  dchrisum0flblem1  27672  dchrisum0flblem2  27673  dchrisum0fno1  27675  rplogsum  27691  logdivsum  27697  mulog2sumlem2  27699  selberg2lem  27714  logdivbnd  27720  pntrsumo1  27729  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntpbnd1  27750  pntpbnd2  27751  pntlem3  27773  pntleml  27775  ostth2  27801  trgcgrg  28784  ttgcontlem1  29234  axlowdimlem1  29292  axlowdimlem6  29297  axlowdimlem7  29298  axlowdimlem10  29301  axlowdim1  29309  axlowdim2  29310  axlowdim  29311  elntg2  29335  umgrislfupgrlem  29472  lfgrnloop  29475  lfuhgr1v0e  29604  usgrexmplef  29609  pthdlem2  30117  crctcshwlkn0lem7  30165  rusgrnumwwlks  30326  clwwlkn0  30379  konigsberg  30608  ex-po  30786  ex-sqrt  30805  ex-gcd  30808  nvz0  31020  0blo  31144  nmlno0lem  31145  nmblolbii  31151  siilem2  31204  minvecolem2  31227  minvecolem3  31228  minvecolem4c  31231  minvecolem4  31232  minvecolem5  31233  minvecolem7  31235  htthlem  31269  hiidge0  31450  normlem6  31467  normgt0  31479  norm-i  31481  normpyc  31498  bcsiALT  31531  pjhthlem1  31743  pjneli  32075  nmlnop0iALT  32347  unopbd  32367  nmbdoplbi  32376  nmcoplbi  32380  nmbdfnlbi  32401  nmbdfnlb  32402  nmcfnlbi  32404  cnlnadjlem7  32425  nmopcoi  32447  branmfn  32457  leopmul  32486  nmopleid  32491  pjbdlni  32501  pjnormssi  32520  stle0i  32591  cdj3lem1  32786  xaddeq0  33098  expgt0b  33161  dp20u  33197  dp20h  33198  dp2clq  33200  dp2lt10  33203  dp2lt  33204  dp0u  33220  dplti  33224  dpexpp1  33227  xdiv0  33248  xrge0slmod  33668  evl1deg3  33868  fldext2chn  34118  cos9thpiminplylem1  34172  unitdivcld  34291  sqsscirc1  34298  xrge0iifcnv  34323  xrge0iifiso  34325  rezh  34359  esumcvgsum  34478  voliune  34619  volfiniune  34620  sibfinima  34729  sitmcl  34741  0rrv  34841  coinfliprv  34873  ballotlem2  34879  ballotlem4  34889  ballotlemi1  34893  ballotlemic  34897  signsply0  34938  signswch  34948  signstf  34953  signstf0  34955  signstfveq0  34964  signlem0  34974  signshf  34975  itgexpif  34993  hgt750lemd  35035  hgt750lem  35038  hgt750lem2  35039  hgt750leme  35045  iisconn  35744  iillysconn  35745  cvmliftlem10  35786  fz0n  36223  bcneg1  36228  nn0prpwlem  36853  dnizeq0  37084  dnizphlfeqhlf  37085  knoppndvlem13  37133  cnndvlem1  37146  bj-pinftyccb  37885  bj-minftyccb  37889  bj-pinftynminfty  37891  taupilemrplb  37984  irrdiff  37990  sin2h  38281  tan2h  38283  ptrecube  38291  poimirlem16  38307  poimirlem17  38308  poimirlem20  38311  poimirlem22  38313  poimirlem23  38314  poimirlem29  38320  poimirlem31  38322  poimir  38324  heicant  38326  mblfinlem2  38329  ismblfin  38332  ovoliunnfl  38333  voliunnfl  38335  volsupnfl  38336  mbfposadd  38338  itg2addnclem  38342  itg2addnclem2  38343  ibladdnclem  38347  itgaddnclem2  38350  iblabsnclem  38354  iblmulc2nc  38356  itgmulc2nclem2  38358  itgabsnc  38360  ftc1cnnclem  38362  ftc1anclem5  38368  ftc1anclem8  38371  asindmre  38374  dvasin  38375  areacirclem4  38382  areacirc  38384  isbnd3  38455  ssbnd  38459  prdsbnd  38464  bfplem2  38494  bfp  38495  renegclALT  39757  0cnALT3  43041  sn-1ne2  43052  itrere  43099  oexpreposd  43103  tan3rdpi  43133  asin1half  43138  readvrec2  43142  sn-00idlem2  43180  sn-00idlem3  43181  sn-00id  43182  sn-0tie0  43245  sn-ltaddpos  43247  sn-ltaddneg  43248  relt0neg1  43250  sn-nnne0  43254  reelznn0nn  43255  sn-0lt1  43269  sn-inelr  43281  sn-itrere  43282  sn-retire  43283  pellexlem6  43581  elpell14qr2  43609  oddcomabszz  43691  zindbi  43693  jm2.24  43710  acongeq  43730  arearect  43962  areaquad  43963  reabsifneg  44378  reabsifnpos  44379  reabsifpos  44380  reabsifnneg  44381  imsqrtvalex  44392  relexp01min  44459  imo72b2lem2  44913  imo72b2lem1  44915  imo72b2  44918  dvconstbi  45064  binomcxplemnn0  45079  binomcxplemdvbinom  45083  binomcxplemcvg  45084  binomcxplemnotnn0  45086  sineq0ALT  45665  halffl  46035  ren0  46136  rexanuz2nf  46226  sqrlearg  46289  limsup10ex  46507  dvnmptdivc  46672  dvnmul  46677  itgsin0pilem1  46684  itgsinexplem1  46688  itgsinexp  46689  iblempty  46699  stoweidlem17  46751  stoweidlem36  46770  stoweidlem55  46789  wallispilem1  46799  wallispilem2  46800  wallispilem4  46802  stirlinglem4  46811  stirlinglem13  46820  stirlinglem14  46821  stirlingr  46824  dirker2re  46826  dirkerdenne0  46827  dirkerre  46829  dirkertrigeqlem1  46832  dirkercncflem2  46838  dirkercncflem4  46840  fourierdlem11  46852  fourierdlem16  46857  fourierdlem21  46862  fourierdlem22  46863  fourierdlem41  46882  fourierdlem42  46883  fourierdlem62  46902  fourierdlem66  46906  fourierdlem79  46919  fourierdlem83  46923  fourierdlem94  46934  fourierdlem102  46942  fourierdlem103  46943  fourierdlem104  46944  fourierdlem111  46951  fourierdlem112  46952  fourierdlem113  46953  fourierdlem114  46954  sqwvfoura  46962  sqwvfourb  46963  fourierswlem  46964  fouriersw  46965  etransclem23  46991  etransclem44  47012  etransclem46  47014  salexct3  47076  salgensscntex  47078  sge0rnn0  47102  sge00  47110  0ome  47263  ovn0lem  47299  ovnhoilem1  47335  smfmullem1  47525  smfmullem2  47526  smfmullem3  47527  smfmullem4  47528  squeezedltsq  47623  goldrapos  47640  zm1nn  48059  sqrtnegnre  48064  flmrecm1  48100  m1mod0mod1  48117  muldvdsfacgt  48143  fmtnoprmfac2lem1  48338  31prm  48369  mod42tp1mod8  48374  nfermltl2rev  48528  tgblthelfgott  48600  usgrexmpl1lem  48806  usgrexmpl2lem  48811  usgrexmpl2nb0  48816  usgrexmpl2nb5  48821  usgrexmpl2trifr  48822  gpgusgralem  48841  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  pgnbgreunbgrlem2lem3  48901  gpg5edgnedg  48915  altgsumbcALT  49153  expnegico01  49318  dignnld  49403  eenglngeehlnmlem1  49537  line2ylem  49551  line2y  49555  itsclc0yqsollem2  49563  icccldii  49717  i0oii  49718  sepfsepc  49726  ex-gt  50526