Theorem 0re 11235

Description: The number 0 is real. Remark: the first step could also be ax-icn 11184. See also 0reALT 11580. (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 11183	. 2 ⊢ 1 ∈ ℂ
2		cnre 11230	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11196	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11208	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2848	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 248	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3163	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 16	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 486	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3155	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3086  (class class class)co 7414  ℂcc 11123  ℝcr 11124  0cc0 11125  1c1 11126  ici 11127   + caddc 11128   · cmul 11130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-1cn 11183  ax-addrcl 11186  ax-rnegex 11196  ax-cnre 11198

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-rex 3087

This theorem is used by:  0red  11236  pr01ssre  11237  0xr  11281  axmulgt0  11309  ne0gt0  11340  00id  11410  mul02lem1  11411  mul02lem2  11412  mul02  11413  addrid  11415  ltaddneg  11451  addgt0  11725  addgegt0  11726  addgtge0  11727  addge0  11728  ltaddpos  11729  ltneg  11739  leneg  11742  lt0neg1  11745  lt0neg2  11746  le0neg1  11747  le0neg2  11748  addge01  11749  suble0  11753  mulge0  11757  msqge0  11760  0le1  11762  relin01  11763  gt0ne0i  11774  lt0ne0d  11804  elimge0  12079  ltm1  12082  recgt0  12086  prodgt0  12087  lemul1a  12094  ltmul12a  12096  lemul12a  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  12233  crne0  12236  indf  12249  indfval  12250  nnge1  12289  nngt0  12292  nnnle0  12294  nnne0  12295  nnrecgt0  12304  0le0  12367  0le2  12368  halfge0  12485  nn0ssre  12533  nn0ge0  12554  nn0nlt0  12555  nn0le0eq0  12557  0mnnnnn0  12561  elnnnn0b  12573  elnnnn0c  12574  nn0sub  12579  elnnz  12626  0z  12627  elnn0z  12629  elnnz1  12645  recnz  12697  gtndiv  12699  fnn0ind  12721  10re  12760  rpge0  13057  rpneg  13077  0nrp  13080  0ltpnf  13174  mnflt0  13177  qsqueeze  13254  xneg0  13265  xaddrid  13294  xnn0xadd0  13300  xmulpnf1  13327  xlemul1a  13341  xadddi  13348  xrsupsslem  13360  xrinfmsslem  13361  elrege0  13508  0e0icopnf  13512  elicc01  13520  0elunit  13523  unitssre  13553  nnge2recico01  13561  0nelfz1  13598  fzpreddisj  13629  fz0to4untppr  13686  fz0to5un2tp  13687  nn0p1elfzo  13759  ico01fl0  13881  rpsup  13928  modelico  13943  0mod  13964  1mod  13965  le2sq2  14200  expubnd  14243  sqlecan  14274  bernneq2  14295  expnbnd  14297  expnlbnd  14298  expmulnbnd  14300  discr1  14304  discr  14305  faclbnd  14355  faclbnd3  14357  faclbnd6  14364  bcval4  14372  bcval5  14383  bcpasc  14386  hasheq0  14428  hashneq0  14429  hashnn0n0nn  14456  hashgt12el  14488  hashgt12el2  14489  hashge2el2dif  14546  lsw0  14631  swrdccatin2  14799  pfxccatin12lem3  14802  sgnclre  15176  sgnnbi  15178  sgnpbi  15179  reim0  15206  re0  15240  im0  15241  rei  15244  imi  15245  cj0  15246  sqeqd  15254  rennim  15327  cnpart  15328  sqrt0  15329  01sqrexlem4  15333  resqrex  15338  sqrtgt0  15346  sqrt00  15351  sqrtneglem  15354  sqrt9  15361  sqrt2gt1lt2  15362  leabs  15387  absor  15388  max0add  15398  eqsqrt2d  15457  sqrtpclii  15471  rlimconst  15632  rlimrege0  15667  lo1mul  15716  iserge0  15749  fsum00  15886  isumless  15935  arisum2  15951  georeclim  15962  geo2sum  15963  geoisumr  15968  0.999...  15971  cvgrat  15973  fprodge0  16081  bpoly4  16146  cos0  16239  ef01bndlem  16273  sin01bnd  16274  cos01bnd  16275  cos2bnd  16277  sin01gt0  16279  cos01gt0  16280  sincos2sgn  16283  sin4lt0  16284  absef  16286  absefib  16287  efieq1re  16288  epos  16296  rpnnen2lem2  16304  rpnnen2lem3  16305  rpnnen2lem4  16306  rpnnen2lem9  16311  ruclem6  16324  dvdslelem  16400  divalglem1  16485  divalglem5  16488  divalglem6  16489  flodddiv4  16506  sadcadd  16549  gcdn0gt0  16609  nn0seqcvgd  16661  algcvgblem  16668  algcvga  16670  pythagtriplem12  16919  pythagtriplem13  16920  pythagtriplem14  16921  pythagtriplem16  16923  prmreclem4  17012  prmreclem5  17013  prmreclem6  17014  1arith  17020  ramz  17118  chnub  18711  mulgnegnn  19208  subgmulg  19265  srgbinomlem4  20369  isabvd  20979  abvtrivd  20999  rge0srg  21652  xrs1mnd  21654  xrs10  21655  psgnodpmr  21804  re0g  21826  psrbaglesupp  22138  psdmvr  22398  mnfnei  23447  imasdsf1olem  24600  ssblps  24649  ssbl  24650  xmeter  24660  dscmet  24799  dscopn  24800  nmoi  24955  nmoeq0  24963  0nghm  24968  idnghm  24970  cnbl0  25000  xrsxmet  25037  metdseq0  25082  iicmp  25115  iiconn  25116  iihalf1  25160  elii1  25164  icopnfcnv  25171  icopnfhmeo  25172  iccpnfcnv  25173  xrhmeo  25175  xrhmph  25176  htpycc  25209  reparphti  25226  pcoval1  25242  pco0  25243  pcoval2  25245  pcocn  25246  pcohtpylem  25248  pcopt  25251  pcopt2  25252  pcoass  25253  pcorevlem  25255  reust  25610  recusp  25611  rrx0el  25627  minveclem4c  25654  minveclem2  25655  minveclem3b  25657  minveclem4  25661  minveclem7  25664  pjthlem1  25666  cniccbdd  25690  ovolunnul  25729  ovoliunnul  25736  ovolicc1  25745  ovolre  25754  iccvolcl  25796  ovolioo  25797  ioovolcl  25799  ioorcl  25806  vitalilem4  25840  vitalilem5  25841  vitali  25842  ismbf  25857  mbfmulc2lem  25876  mbfpos  25880  mbfposr  25881  i1f0  25916  i1f1  25919  itg1addlem2  25926  itg1addlem4  25928  itg1addlem5  25929  mbfi1fseqlem4  25947  mbfi1fseqlem5  25948  mbfi1flimlem  25951  xrge0f  25960  itg2ge0  25964  itg2const  25969  itg2mulc  25976  itg2splitlem  25977  itg2gt0  25989  itg2cnlem1  25990  ibl0  26015  iblrelem  26019  iblposlem  26020  iblpos  26021  iblre  26022  itgreval  26025  itgneg  26032  iblss  26033  i1fibl  26036  itgitg1  26037  itgle  26038  itgeqa  26042  itgless  26045  iblconst  26046  itgconst  26047  ibladdlem  26048  itgaddlem2  26052  iblabslem  26056  iblabsr  26058  iblmulc2  26059  itgmulc2lem2  26061  itgabs  26063  itgsplit  26064  bddmulibl  26067  dvferm1  26213  dvferm2  26215  dvferm  26216  dvlip  26221  c1lip1  26225  dveq0  26228  dv11cn  26229  dvne0  26239  ftc1lem4  26267  ply1divex  26363  dgrco  26502  plyrecj  26508  plyn0mulidp  26512  vieta1lem2  26544  aalioulem2  26570  aalioulem3  26571  pserulm  26659  psercnlem2  26661  psercnlem1  26662  psercn  26663  abelth  26678  reeff1olem  26683  reeff1o  26684  pilem2  26689  pilem3  26690  pipos  26697  pige0  26698  sinhalfpilem  26702  sincosq1sgn  26737  sincosq2sgn  26738  coseq00topi  26741  coseq0negpitopi  26742  tangtx  26744  tanabsge  26745  sinq12ge0  26747  sinq34lt0t  26748  cosq14ge0  26750  sincos4thpi  26752  sincos6thpi  26754  pige3ALT  26758  sineq0  26762  cosordlem  26768  cosord  26769  cos0pilt1  26770  cos11  26771  sinord  26772  recosf1o  26773  resinf1o  26774  tanord1  26775  tanord  26776  tanregt0  26777  efif1olem4  26783  efifo  26785  relogrn  26799  log1  26823  logi  26825  logneg  26826  argregt0  26848  argrege0  26849  argimgt0  26850  logneg2  26853  logdivlti  26858  logdivlt  26859  ellogdm  26877  logdmn0  26878  logdmnrp  26879  logcnlem3  26882  dvloglem  26886  logdmopn  26887  logf1o2  26888  dvlog2lem  26890  efopnlem1  26894  logtayl  26898  recxpcl  26913  cxpge0  26921  cxple2  26935  cxple2a  26937  cxpsqrtlem  26940  cxpcn3  26986  cxpaddlelem  26989  cxpaddle  26990  loglesqrt  26999  logbrec  27020  ang180lem3  27049  ang180lem4  27050  asinneg  27124  asin1  27132  reasinsin  27134  acosbnd  27138  atan0  27146  atanrecl  27149  atanlogaddlem  27151  atanlogsublem  27153  atanlogsub  27154  atantan  27161  atanbnd  27164  atan1  27166  atans2  27169  ressatans  27172  log2cnv  27182  log2tlbnd  27183  log2ub  27187  log2le1  27188  rlimcnp  27203  rlimcnp2  27204  o1cxp  27212  jensen  27226  amgm  27228  emgt0  27244  harmonicbnd3  27245  harmoniclbnd  27246  harmonicbnd4  27248  zetacvg  27252  eldmgm  27259  lgamgulmlem2  27267  basellem3  27320  basellem8  27325  efnnfsumcl  27340  ppisval  27341  vmage0  27358  chpge0  27363  efchtdvds  27396  ppiltx  27414  ppiub  27441  chpeq0  27445  chteq0  27446  chtleppi  27447  chpchtsum  27456  chpub  27457  dchr1re  27500  bcmono  27514  efexple  27518  bposlem1  27521  bposlem4  27524  bposlem5  27525  bposlem7  27527  bposlem8  27528  bposlem9  27529  lgsval2lem  27544  lgsval4a  27556  lgsneg  27558  lgsdilem  27561  lgsdir2lem1  27562  2lgsoddprmlem3a  27647  2lgsoddprmlem3b  27648  2lgsoddprmlem3c  27649  2lgsoddprmlem3d  27650  rplogsumlem2  27722  rpvmasumlem  27724  dchrisum0flblem1  27745  dchrisum0flblem2  27746  dchrisum0fno1  27748  rplogsum  27764  logdivsum  27770  mulog2sumlem2  27772  selberg2lem  27787  logdivbnd  27793  pntrsumo1  27802  pntrlog2bndlem4  27817  pntrlog2bndlem5  27818  pntpbnd1  27823  pntpbnd2  27824  pntlem3  27846  pntleml  27848  ostth2  27874  trgcgrg  28858  ttgcontlem1  29342  axlowdimlem1  29400  axlowdimlem6  29405  axlowdimlem7  29406  axlowdimlem10  29409  axlowdim1  29417  axlowdim2  29418  axlowdim  29419  elntg2  29443  umgrislfupgrlem  29580  lfgrnloop  29583  lfuhgr1v0e  29715  usgrexmplef  29720  pthdlem2  30234  crctcshwlkn0lem7  30285  rusgrnumwwlks  30446  clwwlkn0  30499  konigsberg  30738  ex-po  30916  ex-sqrt  30935  ex-gcd  30938  nvz0  31150  0blo  31274  nmlno0lem  31275  nmblolbii  31281  siilem2  31334  minvecolem2  31357  minvecolem3  31358  minvecolem4c  31361  minvecolem4  31362  minvecolem5  31363  minvecolem7  31365  htthlem  31399  hiidge0  31580  normlem6  31597  normgt0  31609  norm-i  31611  normpyc  31628  bcsiALT  31661  pjhthlem1  31873  pjneli  32205  nmlnop0iALT  32477  unopbd  32497  nmbdoplbi  32506  nmcoplbi  32510  nmbdfnlbi  32531  nmbdfnlb  32532  nmcfnlbi  32534  cnlnadjlem7  32555  nmopcoi  32577  branmfn  32587  leopmul  32616  nmopleid  32621  pjbdlni  32631  pjnormssi  32650  stle0i  32721  cdj3lem1  32916  xaddeq0  33225  expgt0b  33288  dp20u  33324  dp20h  33325  dp2clq  33327  dp2lt10  33330  dp2lt  33331  dp0u  33347  dplti  33351  dpexpp1  33354  xdiv0  33375  xrge0slmod  33789  evl1deg3  33989  fldext2chn  34239  cos9thpiminplylem1  34293  unitdivcld  34412  sqsscirc1  34419  xrge0iifcnv  34444  xrge0iifiso  34446  rezh  34480  esumcvgsum  34599  voliune  34741  volfiniune  34742  sibfinima  34851  sitmcl  34863  0rrv  34963  coinfliprv  34995  ballotlem2  35001  ballotlem4  35011  ballotlemi1  35015  ballotlemic  35019  signsply0  35060  signswch  35070  signstf  35075  signstf0  35077  signstfveq0  35086  signlem0  35096  signshf  35097  itgexpif  35115  hgt750lemd  35157  hgt750lem  35160  hgt750lem2  35161  hgt750leme  35167  iisconn  35832  iillysconn  35833  cvmliftlem10  35874  fz0n  36311  bcneg1  36316  nn0prpwlem  36942  dnizeq0  37173  dnizphlfeqhlf  37174  knoppndvlem13  37222  cnndvlem1  37235  bj-pinftyccb  37974  bj-minftyccb  37978  bj-pinftynminfty  37980  taupilemrplb  38073  irrdiff  38079  sin2h  38365  tan2h  38367  ptrecube  38370  poimirlem16  38386  poimirlem17  38387  poimirlem20  38390  poimirlem22  38392  poimirlem23  38393  poimirlem29  38399  poimirlem31  38401  poimir  38403  heicant  38405  mblfinlem2  38408  ismblfin  38411  ovoliunnfl  38412  voliunnfl  38414  volsupnfl  38415  mbfposadd  38417  itg2addnclem  38421  itg2addnclem2  38422  ibladdnclem  38426  itgaddnclem2  38429  iblabsnclem  38433  iblmulc2nc  38435  itgmulc2nclem2  38437  itgabsnc  38439  ftc1cnnclem  38441  ftc1anclem5  38447  ftc1anclem8  38450  asindmre  38453  dvasin  38454  areacirclem4  38461  areacirc  38463  isbnd3  38535  ssbnd  38539  prdsbnd  38544  bfplem2  38574  bfp  38575  renegclALT  39837  0cnALT3  43121  sn-1ne2  43147  itrere  43194  oexpreposd  43198  tan3rdpi  43228  asin1half  43233  readvrec2  43237  sn-00idlem2  43275  sn-00idlem3  43276  sn-00id  43277  sn-0tie0  43340  sn-ltaddpos  43342  sn-ltaddneg  43343  relt0neg1  43345  sn-nnne0  43349  reelznn0nn  43350  sn-0lt1  43364  sn-inelr  43376  sn-itrere  43377  sn-retire  43378  pellexlem6  43676  elpell14qr2  43704  oddcomabszz  43786  zindbi  43788  jm2.24  43805  acongeq  43825  arearect  44057  areaquad  44058  reabsifneg  44473  reabsifnpos  44474  reabsifpos  44475  reabsifnneg  44476  imsqrtvalex  44487  relexp01min  44554  imo72b2lem2  45008  imo72b2lem1  45010  imo72b2  45013  dvconstbi  45159  binomcxplemnn0  45174  binomcxplemdvbinom  45178  binomcxplemcvg  45179  binomcxplemnotnn0  45181  sineq0ALT  45760  halffl  46130  ren0  46231  rexanuz2nf  46321  sqrlearg  46384  limsup10ex  46602  dvnmptdivc  46767  dvnmul  46772  itgsin0pilem1  46779  itgsinexplem1  46783  itgsinexp  46784  iblempty  46794  stoweidlem17  46846  stoweidlem36  46865  stoweidlem55  46884  wallispilem1  46894  wallispilem2  46895  wallispilem4  46897  stirlinglem4  46906  stirlinglem13  46915  stirlinglem14  46916  stirlingr  46919  dirker2re  46921  dirkerdenne0  46922  dirkerre  46924  dirkertrigeqlem1  46927  dirkercncflem2  46933  dirkercncflem4  46935  fourierdlem11  46947  fourierdlem16  46952  fourierdlem21  46957  fourierdlem22  46958  fourierdlem41  46977  fourierdlem42  46978  fourierdlem62  46997  fourierdlem66  47001  fourierdlem79  47014  fourierdlem83  47018  fourierdlem94  47029  fourierdlem102  47037  fourierdlem103  47038  fourierdlem104  47039  fourierdlem111  47046  fourierdlem112  47047  fourierdlem113  47048  fourierdlem114  47049  sqwvfoura  47057  sqwvfourb  47058  fourierswlem  47059  fouriersw  47060  etransclem23  47086  etransclem44  47107  etransclem46  47109  salexct3  47171  salgensscntex  47173  sge0rnn0  47197  sge00  47205  0ome  47358  ovn0lem  47394  ovnhoilem1  47430  smfmullem1  47620  smfmullem2  47621  smfmullem3  47622  smfmullem4  47623  squeezedltsq  47731  goldrapos  47749  goldratval  47755  zm1nn  48191  sqrtnegnre  48196  flmrecm1  48232  m1mod0mod1  48249  muldvdsfacgt  48275  fmtnoprmfac2lem1  48470  31prm  48501  mod42tp1mod8  48506  nfermltl2rev  48660  tgblthelfgott  48732  usgrexmpl1lem  48938  usgrexmpl2lem  48943  usgrexmpl2nb0  48948  usgrexmpl2nb5  48953  usgrexmpl2trifr  48954  gpgusgralem  48973  pgnbgreunbgrlem2lem1  49031  pgnbgreunbgrlem2lem2  49032  pgnbgreunbgrlem2lem3  49033  gpg5edgnedg  49047  altgsumbcALT  49284  expnegico01  49449  dignnld  49534  eenglngeehlnmlem1  49668  line2ylem  49682  line2y  49686  itsclc0yqsollem2  49694  icccldii  49846  i0oii  49847  sepfsepc  49855  ex-gt  50655