Theorem 0re 11137

Description: The number 0 is real. Remark: the first step could also be ax-icn 11088. See also 0reALT 11482. (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 11087	. 2 ⊢ 1 ∈ ℂ
2		cnre 11132	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11100	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11112	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2827	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 246	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3140	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 481	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3132	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃wrex 3063  (class class class)co 7356  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030  ici 11031   + caddc 11032   · cmul 11034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-rex 3064

This theorem is referenced by:  0red  11138  pr01ssre  11139  0xr  11183  axmulgt0  11211  ne0gt0  11242  00id  11312  mul02lem1  11313  mul02lem2  11314  mul02  11315  addrid  11317  ltaddneg  11353  addgt0  11627  addgegt0  11628  addgtge0  11629  addge0  11630  ltaddpos  11631  ltneg  11641  leneg  11644  lt0neg1  11647  lt0neg2  11648  le0neg1  11649  le0neg2  11650  addge01  11651  suble0  11655  mulge0  11659  msqge0  11662  0le1  11664  relin01  11665  gt0ne0i  11676  lt0ne0d  11706  elimge0  11985  ltm1  11988  recgt0  11992  prodgt0  11993  lemul1a  12000  ltmul12a  12002  lemul12a  12004  mulgt1OLD  12005  gt0div  12013  ge0div  12014  mulge0b  12017  lediv12a  12040  recgt1i  12044  recreclt  12046  ledivp1  12049  squeeze0  12050  recgt0ii  12053  ledivp1i  12072  ltdivp1i  12073  fimaxre2  12092  inelr  12140  crne0  12143  indf  12156  indfval  12157  nnge1  12196  nngt0  12199  nnnle0  12201  nnne0  12202  nnrecgt0  12211  0le0  12273  halfge0  12384  nn0ssre  12432  nn0ge0  12453  nn0nlt0  12454  nn0le0eq0  12456  0mnnnnn0  12460  elnnnn0b  12472  elnnnn0c  12473  nn0sub  12478  elnnz  12525  0z  12526  elnn0z  12528  elnnz1  12544  recnz  12595  gtndiv  12597  fnn0ind  12619  10re  12654  rpge0  12947  rpneg  12967  0nrp  12970  0ltpnf  13064  mnflt0  13067  qsqueeze  13144  xneg0  13155  xaddrid  13184  xnn0xadd0  13190  xmulpnf1  13217  xlemul1a  13231  xadddi  13238  xrsupsslem  13250  xrinfmsslem  13251  elrege0  13398  0e0icopnf  13402  elicc01  13410  0elunit  13413  unitssre  13443  nnge2recico01  13451  0nelfz1  13488  fzpreddisj  13518  fz0to4untppr  13575  fz0to5un2tp  13576  nn0p1elfzo  13648  ico01fl0  13769  rpsup  13816  modelico  13831  0mod  13852  1mod  13853  le2sq2  14088  expubnd  14131  sqlecan  14162  bernneq2  14183  expnbnd  14185  expnlbnd  14186  expmulnbnd  14188  discr1  14192  discr  14193  faclbnd  14243  faclbnd3  14245  faclbnd6  14252  bcval4  14260  bcval5  14271  bcpasc  14274  hasheq0  14316  hashneq0  14317  hashnn0n0nn  14344  hashgt12el  14375  hashgt12el2  14376  hashge2el2dif  14433  lsw0  14518  swrdccatin2  14682  pfxccatin12lem3  14685  reim0  15071  re0  15105  im0  15106  rei  15109  imi  15110  cj0  15111  sqeqd  15119  rennim  15192  cnpart  15193  sqrt0  15194  01sqrexlem4  15198  resqrex  15203  sqrtgt0  15211  sqrt00  15216  sqrtneglem  15219  sqrt9  15226  sqrt2gt1lt2  15227  leabs  15252  absor  15253  max0add  15263  eqsqrt2d  15322  sqrtpclii  15336  rlimconst  15497  rlimrege0  15532  lo1mul  15581  iserge0  15614  fsum00  15752  isumless  15801  arisum2  15817  georeclim  15828  geo2sum  15829  geoisumr  15834  0.999...  15837  cvgrat  15839  fprodge0  15949  bpoly4  16015  cos0  16108  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  cos2bnd  16146  sin01gt0  16148  cos01gt0  16149  sincos2sgn  16152  sin4lt0  16153  absef  16155  absefib  16156  efieq1re  16157  epos  16165  rpnnen2lem2  16173  rpnnen2lem3  16174  rpnnen2lem4  16175  rpnnen2lem9  16180  ruclem6  16193  dvdslelem  16269  divalglem1  16354  divalglem5  16357  divalglem6  16358  flodddiv4  16375  sadcadd  16418  gcdn0gt0  16478  nn0seqcvgd  16530  algcvgblem  16537  algcvga  16539  pythagtriplem12  16788  pythagtriplem13  16789  pythagtriplem14  16790  pythagtriplem16  16792  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  1arith  16889  ramz  16987  chnub  18579  mulgnegnn  19051  subgmulg  19107  srgbinomlem4  20201  isabvd  20784  abvtrivd  20804  rge0srg  21413  xrs1mnd  21415  xrs10  21416  psgnodpmr  21565  re0g  21587  psrbaglesupp  21897  psdmvr  22157  mnfnei  23204  imasdsf1olem  24356  ssblps  24405  ssbl  24406  xmeter  24416  dscmet  24555  dscopn  24556  nmoi  24711  nmoeq0  24719  0nghm  24724  idnghm  24726  cnbl0  24756  xrsxmet  24793  metdseq0  24838  iicmp  24871  iiconn  24872  iihalf1  24916  elii1  24920  icopnfcnv  24927  icopnfhmeo  24928  iccpnfcnv  24929  xrhmeo  24931  xrhmph  24932  htpycc  24965  reparphti  24982  pcoval1  24998  pco0  24999  pcoval2  25001  pcocn  25002  pcohtpylem  25004  pcopt  25007  pcopt2  25008  pcoass  25009  pcorevlem  25011  reust  25366  recusp  25367  rrx0el  25383  minveclem4c  25410  minveclem2  25411  minveclem3b  25413  minveclem4  25417  minveclem7  25420  pjthlem1  25422  cniccbdd  25446  ovolunnul  25485  ovoliunnul  25492  ovolicc1  25501  ovolre  25510  iccvolcl  25552  ovolioo  25553  ioovolcl  25555  ioorcl  25562  vitalilem4  25596  vitalilem5  25597  vitali  25598  ismbf  25613  mbfmulc2lem  25632  mbfpos  25636  mbfposr  25637  i1f0  25672  i1f1  25675  itg1addlem2  25682  itg1addlem4  25684  itg1addlem5  25685  mbfi1fseqlem4  25703  mbfi1fseqlem5  25704  mbfi1flimlem  25707  xrge0f  25716  itg2ge0  25720  itg2const  25725  itg2mulc  25732  itg2splitlem  25733  itg2gt0  25745  itg2cnlem1  25746  ibl0  25772  iblrelem  25776  iblposlem  25777  iblpos  25778  iblre  25779  itgreval  25782  itgneg  25789  iblss  25790  i1fibl  25793  itgitg1  25794  itgle  25795  itgeqa  25799  itgless  25802  iblconst  25803  itgconst  25804  ibladdlem  25805  itgaddlem2  25809  iblabslem  25813  iblabsr  25815  iblmulc2  25816  itgmulc2lem2  25818  itgabs  25820  itgsplit  25821  bddmulibl  25824  dvferm1  25970  dvferm2  25972  dvferm  25973  dvlip  25978  c1lip1  25982  dveq0  25985  dv11cn  25986  dvne0  25996  ftc1lem4  26024  ply1divex  26120  dgrco  26258  plyrecj  26264  vieta1lem2  26295  aalioulem2  26317  aalioulem3  26318  pserulm  26405  psercnlem2  26407  psercnlem1  26408  psercn  26409  abelth  26424  reeff1olem  26429  reeff1o  26430  pilem2  26435  pilem3  26436  pipos  26441  sinhalfpilem  26445  sincosq1sgn  26480  sincosq2sgn  26481  coseq00topi  26484  coseq0negpitopi  26485  tangtx  26487  tanabsge  26488  sinq12ge0  26490  sinq34lt0t  26491  cosq14ge0  26493  sincos4thpi  26495  sincos6thpi  26498  pige3ALT  26502  sineq0  26506  cosordlem  26512  cosord  26513  cos0pilt1  26514  cos11  26515  sinord  26516  recosf1o  26517  resinf1o  26518  tanord1  26519  tanord  26520  tanregt0  26521  efif1olem4  26527  efifo  26529  relogrn  26543  log1  26567  logi  26569  logneg  26570  argregt0  26592  argrege0  26593  argimgt0  26594  logneg2  26597  logdivlti  26602  logdivlt  26603  ellogdm  26621  logdmn0  26622  logdmnrp  26623  logcnlem3  26626  dvloglem  26630  logdmopn  26631  logf1o2  26632  dvlog2lem  26634  efopnlem1  26638  logtayl  26642  recxpcl  26657  cxpge0  26665  cxple2  26679  cxple2a  26681  cxpsqrtlem  26684  cxpcn3  26730  cxpaddlelem  26733  cxpaddle  26734  loglesqrt  26743  logbrec  26764  ang180lem3  26793  ang180lem4  26794  asinneg  26868  asin1  26876  reasinsin  26878  acosbnd  26882  atan0  26890  atanrecl  26893  atanlogaddlem  26895  atanlogsublem  26897  atanlogsub  26898  atantan  26905  atanbnd  26908  atan1  26910  atans2  26913  ressatans  26916  log2cnv  26926  log2tlbnd  26927  log2ub  26931  log2le1  26932  rlimcnp  26947  rlimcnp2  26948  o1cxp  26956  jensen  26970  amgm  26972  emgt0  26988  harmonicbnd3  26989  harmoniclbnd  26990  harmonicbnd4  26992  zetacvg  26996  eldmgm  27003  lgamgulmlem2  27011  basellem3  27064  basellem8  27069  efnnfsumcl  27084  ppisval  27085  vmage0  27102  chpge0  27107  efchtdvds  27140  ppiltx  27158  ppiub  27185  chpeq0  27189  chteq0  27190  chtleppi  27191  chpchtsum  27200  chpub  27201  dchr1re  27244  bcmono  27258  efexple  27262  bposlem1  27265  bposlem4  27268  bposlem5  27269  bposlem7  27271  bposlem8  27272  bposlem9  27273  lgsval2lem  27288  lgsval4a  27300  lgsneg  27302  lgsdilem  27305  lgsdir2lem1  27306  2lgsoddprmlem3a  27391  2lgsoddprmlem3b  27392  2lgsoddprmlem3c  27393  2lgsoddprmlem3d  27394  rplogsumlem2  27466  rpvmasumlem  27468  dchrisum0flblem1  27489  dchrisum0flblem2  27490  dchrisum0fno1  27492  rplogsum  27508  logdivsum  27514  mulog2sumlem2  27516  selberg2lem  27531  logdivbnd  27537  pntrsumo1  27546  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntpbnd1  27567  pntpbnd2  27568  pntlem3  27590  pntleml  27592  ostth2  27618  trgcgrg  28601  ttgcontlem1  28971  axlowdimlem1  29029  axlowdimlem6  29034  axlowdimlem7  29035  axlowdimlem10  29038  axlowdim1  29046  axlowdim2  29047  axlowdim  29048  elntg2  29072  umgrislfupgrlem  29209  lfgrnloop  29212  lfuhgr1v0e  29341  usgrexmplef  29346  pthdlem2  29854  crctcshwlkn0lem7  29902  rusgrnumwwlks  30063  clwwlkn0  30116  konigsberg  30345  ex-po  30523  ex-sqrt  30542  ex-gcd  30545  nvz0  30757  0blo  30881  nmlno0lem  30882  nmblolbii  30888  siilem2  30941  minvecolem2  30964  minvecolem3  30965  minvecolem4c  30968  minvecolem4  30969  minvecolem5  30970  minvecolem7  30972  htthlem  31006  hiidge0  31187  normlem6  31204  normgt0  31216  norm-i  31218  normpyc  31235  bcsiALT  31268  pjhthlem1  31480  pjneli  31812  nmlnop0iALT  32084  unopbd  32104  nmbdoplbi  32113  nmcoplbi  32117  nmbdfnlbi  32138  nmbdfnlb  32139  nmcfnlbi  32141  cnlnadjlem7  32162  nmopcoi  32184  branmfn  32194  leopmul  32223  nmopleid  32228  pjbdlni  32238  pjnormssi  32257  stle0i  32328  cdj3lem1  32523  xaddeq0  32845  expgt0b  32909  sgnclre  32924  sgnnbi  32930  sgnpbi  32931  dp20u  32956  dp20h  32957  dp2clq  32959  dp2lt10  32962  dp2lt  32963  dp0u  32979  dplti  32983  dpexpp1  32986  xdiv0  33007  xrge0slmod  33431  evl1deg3  33661  fldext2chn  33912  cos9thpiminplylem1  33966  unitdivcld  34085  sqsscirc1  34092  xrge0iifcnv  34117  xrge0iifiso  34119  rezh  34153  esumcvgsum  34272  voliune  34413  volfiniune  34414  sibfinima  34523  sitmcl  34535  0rrv  34635  coinfliprv  34667  ballotlem2  34673  ballotlem4  34683  ballotlemi1  34687  ballotlemic  34691  plymulx0  34731  signsply0  34735  signswch  34745  signstf  34750  signstf0  34752  signstfveq0  34761  signlem0  34771  signshf  34772  itgexpif  34790  hgt750lemd  34832  hgt750lem  34835  hgt750lem2  34836  hgt750leme  34842  iisconn  35480  iillysconn  35481  cvmliftlem10  35522  fz0n  35959  bcneg1  35964  nn0prpwlem  36550  dnizeq0  36781  dnizphlfeqhlf  36782  knoppndvlem13  36830  cnndvlem1  36843  bj-pinftyccb  37581  bj-minftyccb  37585  bj-pinftynminfty  37587  taupilemrplb  37680  irrdiff  37686  sin2h  37977  tan2h  37979  ptrecube  37987  poimirlem16  38003  poimirlem17  38004  poimirlem20  38007  poimirlem22  38009  poimirlem23  38010  poimirlem29  38016  poimirlem31  38018  poimir  38020  heicant  38022  mblfinlem2  38025  ismblfin  38028  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  mbfposadd  38034  itg2addnclem  38038  itg2addnclem2  38039  ibladdnclem  38043  itgaddnclem2  38046  iblabsnclem  38050  iblmulc2nc  38052  itgmulc2nclem2  38054  itgabsnc  38056  ftc1cnnclem  38058  ftc1anclem5  38064  ftc1anclem8  38067  asindmre  38070  dvasin  38071  areacirclem4  38078  areacirc  38080  isbnd3  38151  ssbnd  38155  prdsbnd  38160  bfplem2  38190  bfp  38191  renegclALT  39455  0cnALT3  42737  sn-1ne2  42748  itrere  42795  oexpreposd  42799  tan3rdpi  42829  asin1half  42834  readvrec2  42838  sn-00idlem2  42876  sn-00idlem3  42877  sn-00id  42878  sn-0tie0  42941  sn-ltaddpos  42943  sn-ltaddneg  42944  relt0neg1  42946  sn-nnne0  42950  reelznn0nn  42951  sn-0lt1  42965  sn-inelr  42977  sn-itrere  42978  sn-retire  42979  pellexlem6  43279  elpell14qr2  43307  oddcomabszz  43389  zindbi  43391  jm2.24  43408  acongeq  43428  arearect  43660  areaquad  43661  reabsifneg  44076  reabsifnpos  44077  reabsifpos  44078  reabsifnneg  44079  imsqrtvalex  44090  relexp01min  44157  imo72b2lem2  44611  imo72b2lem1  44613  imo72b2  44616  dvconstbi  44778  binomcxplemnn0  44793  binomcxplemdvbinom  44797  binomcxplemcvg  44798  binomcxplemnotnn0  44800  sineq0ALT  45380  halffl  45744  ren0  45845  rexanuz2nf  45935  sqrlearg  45998  limsup10ex  46216  dvnmptdivc  46381  dvnmul  46386  itgsin0pilem1  46393  itgsinexplem1  46397  itgsinexp  46398  iblempty  46408  stoweidlem17  46460  stoweidlem36  46479  stoweidlem55  46498  wallispilem1  46508  wallispilem2  46509  wallispilem4  46511  stirlinglem4  46520  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  stirlingr  46533  dirker2re  46535  dirkerdenne0  46536  dirkerre  46538  dirkertrigeqlem1  46541  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem11  46561  fourierdlem16  46566  fourierdlem21  46571  fourierdlem22  46572  fourierdlem41  46591  fourierdlem42  46592  fourierdlem48  46597  fourierdlem62  46611  fourierdlem66  46615  fourierdlem79  46628  fourierdlem83  46632  fourierdlem94  46643  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  fourierdlem114  46663  sqwvfoura  46671  sqwvfourb  46672  fourierswlem  46673  fouriersw  46674  etransclem23  46700  etransclem44  46721  etransclem46  46723  salexct3  46785  salgensscntex  46787  sge0rnn0  46811  sge00  46819  0ome  46972  ovn0lem  47008  ovnhoilem1  47044  smfmullem1  47234  smfmullem2  47235  smfmullem3  47236  smfmullem4  47237  squeezedltsq  47333  goldrapos  47346  zm1nn  47765  sqrtnegnre  47770  flmrecm1  47806  m1mod0mod1  47823  muldvdsfacgt  47849  fmtnoprmfac2lem1  48044  31prm  48075  mod42tp1mod8  48080  nfermltl2rev  48234  tgblthelfgott  48306  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb0  48522  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528  gpgusgralem  48547  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  gpg5edgnedg  48621  altgsumbcALT  48844  expnegico01  49009  dignnld  49094  eenglngeehlnmlem1  49228  line2ylem  49242  line2y  49246  itsclc0yqsollem2  49254  icccldii  49409  i0oii  49410  sepfsepc  49418  ex-gt  50218