Theorem 0re 11140

Description: The number 0 is real. Remark: the first step could also be ax-icn 11091. See also 0reALT 11485. (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 11090	. 2 ⊢ 1 ∈ ℂ
2		cnre 11135	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11103	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11115	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2825	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3139	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3131	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  (class class class)co 7361  ℂcc 11030  ℝcr 11031  0cc0 11032  1c1 11033  ici 11034   + caddc 11035   · cmul 11037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-addrcl 11093  ax-rnegex 11103  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-rex 3063

This theorem is referenced by:  0red  11141  pr01ssre  11142  0xr  11186  axmulgt0  11214  ne0gt0  11245  00id  11315  mul02lem1  11316  mul02lem2  11317  mul02  11318  addrid  11320  ltaddneg  11356  addgt0  11630  addgegt0  11631  addgtge0  11632  addge0  11633  ltaddpos  11634  ltneg  11644  leneg  11647  lt0neg1  11650  lt0neg2  11651  le0neg1  11652  le0neg2  11653  addge01  11654  suble0  11658  mulge0  11662  msqge0  11665  0le1  11667  relin01  11668  gt0ne0i  11679  lt0ne0d  11709  elimge0  11988  ltm1  11991  recgt0  11995  prodgt0  11996  lemul1a  12003  ltmul12a  12005  lemul12a  12007  mulgt1OLD  12008  gt0div  12016  ge0div  12017  mulge0b  12020  lediv12a  12043  recgt1i  12047  recreclt  12049  ledivp1  12052  squeeze0  12053  recgt0ii  12056  ledivp1i  12075  ltdivp1i  12076  fimaxre2  12095  inelr  12143  crne0  12146  indf  12159  indfval  12160  nnge1  12199  nngt0  12202  nnnle0  12204  nnne0  12205  nnrecgt0  12214  0le0  12276  halfge0  12387  nn0ssre  12435  nn0ge0  12456  nn0nlt0  12457  nn0le0eq0  12459  0mnnnnn0  12463  elnnnn0b  12475  elnnnn0c  12476  nn0sub  12481  elnnz  12528  0z  12529  elnn0z  12531  elnnz1  12547  recnz  12598  gtndiv  12600  fnn0ind  12622  10re  12657  rpge0  12950  rpneg  12970  0nrp  12973  0ltpnf  13067  mnflt0  13070  qsqueeze  13147  xneg0  13158  xaddrid  13187  xnn0xadd0  13193  xmulpnf1  13220  xlemul1a  13234  xadddi  13241  xrsupsslem  13253  xrinfmsslem  13254  elrege0  13401  0e0icopnf  13405  elicc01  13413  0elunit  13416  unitssre  13446  nnge2recico01  13454  0nelfz1  13491  fzpreddisj  13521  fz0to4untppr  13578  fz0to5un2tp  13579  nn0p1elfzo  13651  ico01fl0  13772  rpsup  13819  modelico  13834  0mod  13855  1mod  13856  le2sq2  14091  expubnd  14134  sqlecan  14165  bernneq2  14186  expnbnd  14188  expnlbnd  14189  expmulnbnd  14191  discr1  14195  discr  14196  faclbnd  14246  faclbnd3  14248  faclbnd6  14255  bcval4  14263  bcval5  14274  bcpasc  14277  hasheq0  14319  hashneq0  14320  hashnn0n0nn  14347  hashgt12el  14378  hashgt12el2  14379  hashge2el2dif  14436  lsw0  14521  swrdccatin2  14685  pfxccatin12lem3  14688  reim0  15074  re0  15108  im0  15109  rei  15112  imi  15113  cj0  15114  sqeqd  15122  rennim  15195  cnpart  15196  sqrt0  15197  01sqrexlem4  15201  resqrex  15206  sqrtgt0  15214  sqrt00  15219  sqrtneglem  15222  sqrt9  15229  sqrt2gt1lt2  15230  leabs  15255  absor  15256  max0add  15266  eqsqrt2d  15325  sqrtpclii  15339  rlimconst  15500  rlimrege0  15535  lo1mul  15584  iserge0  15617  fsum00  15755  isumless  15804  arisum2  15820  georeclim  15831  geo2sum  15832  geoisumr  15837  0.999...  15840  cvgrat  15842  fprodge0  15952  bpoly4  16018  cos0  16111  ef01bndlem  16145  sin01bnd  16146  cos01bnd  16147  cos2bnd  16149  sin01gt0  16151  cos01gt0  16152  sincos2sgn  16155  sin4lt0  16156  absef  16158  absefib  16159  efieq1re  16160  epos  16168  rpnnen2lem2  16176  rpnnen2lem3  16177  rpnnen2lem4  16178  rpnnen2lem9  16183  ruclem6  16196  dvdslelem  16272  divalglem1  16357  divalglem5  16360  divalglem6  16361  flodddiv4  16378  sadcadd  16421  gcdn0gt0  16481  nn0seqcvgd  16533  algcvgblem  16540  algcvga  16542  pythagtriplem12  16791  pythagtriplem13  16792  pythagtriplem14  16793  pythagtriplem16  16795  prmreclem4  16884  prmreclem5  16885  prmreclem6  16886  1arith  16892  ramz  16990  chnub  18582  mulgnegnn  19054  subgmulg  19110  srgbinomlem4  20204  isabvd  20783  abvtrivd  20803  rge0srg  21431  xrs1mnd  21433  xrs10  21434  psgnodpmr  21583  re0g  21605  psrbaglesupp  21915  psdmvr  22148  mnfnei  23199  imasdsf1olem  24351  ssblps  24400  ssbl  24401  xmeter  24411  dscmet  24550  dscopn  24551  nmoi  24706  nmoeq0  24714  0nghm  24719  idnghm  24721  cnbl0  24751  xrsxmet  24788  metdseq0  24833  iicmp  24866  iiconn  24867  iihalf1  24911  elii1  24915  icopnfcnv  24922  icopnfhmeo  24923  iccpnfcnv  24924  xrhmeo  24926  xrhmph  24927  htpycc  24960  reparphti  24977  pcoval1  24993  pco0  24994  pcoval2  24996  pcocn  24997  pcohtpylem  24999  pcopt  25002  pcopt2  25003  pcoass  25004  pcorevlem  25006  reust  25361  recusp  25362  rrx0el  25378  minveclem4c  25405  minveclem2  25406  minveclem3b  25408  minveclem4  25412  minveclem7  25415  pjthlem1  25417  cniccbdd  25441  ovolunnul  25480  ovoliunnul  25487  ovolicc1  25496  ovolre  25505  iccvolcl  25547  ovolioo  25548  ioovolcl  25550  ioorcl  25557  vitalilem4  25591  vitalilem5  25592  vitali  25593  ismbf  25608  mbfmulc2lem  25627  mbfpos  25631  mbfposr  25632  i1f0  25667  i1f1  25670  itg1addlem2  25677  itg1addlem4  25679  itg1addlem5  25680  mbfi1fseqlem4  25698  mbfi1fseqlem5  25699  mbfi1flimlem  25702  xrge0f  25711  itg2ge0  25715  itg2const  25720  itg2mulc  25727  itg2splitlem  25728  itg2gt0  25740  itg2cnlem1  25741  ibl0  25767  iblrelem  25771  iblposlem  25772  iblpos  25773  iblre  25774  itgreval  25777  itgneg  25784  iblss  25785  i1fibl  25788  itgitg1  25789  itgle  25790  itgeqa  25794  itgless  25797  iblconst  25798  itgconst  25799  ibladdlem  25800  itgaddlem2  25804  iblabslem  25808  iblabsr  25810  iblmulc2  25811  itgmulc2lem2  25813  itgabs  25815  itgsplit  25816  bddmulibl  25819  dvferm1  25965  dvferm2  25967  dvferm  25968  dvlip  25973  c1lip1  25977  dveq0  25980  dv11cn  25981  dvne0  25991  ftc1lem4  26019  ply1divex  26115  dgrco  26253  plyrecj  26259  vieta1lem2  26291  aalioulem2  26313  aalioulem3  26314  pserulm  26403  psercnlem2  26405  psercnlem1  26406  psercn  26407  abelth  26422  reeff1olem  26427  reeff1o  26428  pilem2  26433  pilem3  26434  pipos  26439  sinhalfpilem  26443  sincosq1sgn  26478  sincosq2sgn  26479  coseq00topi  26482  coseq0negpitopi  26483  tangtx  26485  tanabsge  26486  sinq12ge0  26488  sinq34lt0t  26489  cosq14ge0  26491  sincos4thpi  26493  sincos6thpi  26496  pige3ALT  26500  sineq0  26504  cosordlem  26510  cosord  26511  cos0pilt1  26512  cos11  26513  sinord  26514  recosf1o  26515  resinf1o  26516  tanord1  26517  tanord  26518  tanregt0  26519  efif1olem4  26525  efifo  26527  relogrn  26541  log1  26565  logi  26567  logneg  26568  argregt0  26590  argrege0  26591  argimgt0  26592  logneg2  26595  logdivlti  26600  logdivlt  26601  ellogdm  26619  logdmn0  26620  logdmnrp  26621  logcnlem3  26624  dvloglem  26628  logdmopn  26629  logf1o2  26630  dvlog2lem  26632  efopnlem1  26636  logtayl  26640  recxpcl  26655  cxpge0  26663  cxple2  26677  cxple2a  26679  cxpsqrtlem  26682  cxpcn3  26728  cxpaddlelem  26731  cxpaddle  26732  loglesqrt  26741  logbrec  26762  ang180lem3  26791  ang180lem4  26792  asinneg  26866  asin1  26874  reasinsin  26876  acosbnd  26880  atan0  26888  atanrecl  26891  atanlogaddlem  26893  atanlogsublem  26895  atanlogsub  26896  atantan  26903  atanbnd  26906  atan1  26908  atans2  26911  ressatans  26914  log2cnv  26924  log2tlbnd  26925  log2ub  26929  log2le1  26930  rlimcnp  26945  rlimcnp2  26946  o1cxp  26955  jensen  26969  amgm  26971  emgt0  26987  harmonicbnd3  26988  harmoniclbnd  26989  harmonicbnd4  26991  zetacvg  26995  eldmgm  27002  lgamgulmlem2  27010  basellem3  27063  basellem8  27068  efnnfsumcl  27083  ppisval  27084  vmage0  27101  chpge0  27106  efchtdvds  27139  ppiltx  27157  ppiub  27184  chpeq0  27188  chteq0  27189  chtleppi  27190  chpchtsum  27199  chpub  27200  dchr1re  27243  bcmono  27257  efexple  27261  bposlem1  27264  bposlem4  27267  bposlem5  27268  bposlem7  27270  bposlem8  27271  bposlem9  27272  lgsval2lem  27287  lgsval4a  27299  lgsneg  27301  lgsdilem  27304  lgsdir2lem1  27305  2lgsoddprmlem3a  27390  2lgsoddprmlem3b  27391  2lgsoddprmlem3c  27392  2lgsoddprmlem3d  27393  rplogsumlem2  27465  rpvmasumlem  27467  dchrisum0flblem1  27488  dchrisum0flblem2  27489  dchrisum0fno1  27491  rplogsum  27507  logdivsum  27513  mulog2sumlem2  27515  selberg2lem  27530  logdivbnd  27536  pntrsumo1  27545  pntrlog2bndlem4  27560  pntrlog2bndlem5  27561  pntpbnd1  27566  pntpbnd2  27567  pntlem3  27589  pntleml  27591  ostth2  27617  trgcgrg  28600  ttgcontlem1  28970  axlowdimlem1  29028  axlowdimlem6  29033  axlowdimlem7  29034  axlowdimlem10  29037  axlowdim1  29045  axlowdim2  29046  axlowdim  29047  elntg2  29071  umgrislfupgrlem  29208  lfgrnloop  29211  lfuhgr1v0e  29340  usgrexmplef  29345  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  32844  expgt0b  32908  sgnclre  32923  sgnnbi  32929  sgnpbi  32930  dp20u  32955  dp20h  32956  dp2clq  32958  dp2lt10  32961  dp2lt  32962  dp0u  32978  dplti  32982  dpexpp1  32985  xdiv0  33006  xrge0slmod  33426  evl1deg3  33656  fldext2chn  33891  cos9thpiminplylem1  33945  unitdivcld  34064  sqsscirc1  34071  xrge0iifcnv  34096  xrge0iifiso  34098  rezh  34132  esumcvgsum  34251  voliune  34392  volfiniune  34393  sibfinima  34502  sitmcl  34514  0rrv  34614  coinfliprv  34646  ballotlem2  34652  ballotlem4  34662  ballotlemi1  34666  ballotlemic  34670  plymulx0  34710  signsply0  34714  signswch  34724  signstf  34729  signstf0  34731  signstfveq0  34740  signlem0  34750  signshf  34751  itgexpif  34769  hgt750lemd  34811  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  iisconn  35453  iillysconn  35454  cvmliftlem10  35495  fz0n  35932  bcneg1  35937  nn0prpwlem  36523  dnizeq0  36754  dnizphlfeqhlf  36755  knoppndvlem13  36803  cnndvlem1  36816  bj-pinftyccb  37554  bj-minftyccb  37558  bj-pinftynminfty  37560  taupilemrplb  37653  irrdiff  37659  sin2h  37948  tan2h  37950  ptrecube  37958  poimirlem16  37974  poimirlem17  37975  poimirlem20  37978  poimirlem22  37980  poimirlem23  37981  poimirlem29  37987  poimirlem31  37989  poimir  37991  heicant  37993  mblfinlem2  37996  ismblfin  37999  ovoliunnfl  38000  voliunnfl  38002  volsupnfl  38003  mbfposadd  38005  itg2addnclem  38009  itg2addnclem2  38010  ibladdnclem  38014  itgaddnclem2  38017  iblabsnclem  38021  iblmulc2nc  38023  itgmulc2nclem2  38025  itgabsnc  38027  ftc1cnnclem  38029  ftc1anclem5  38035  ftc1anclem8  38038  asindmre  38041  dvasin  38042  areacirclem4  38049  areacirc  38051  isbnd3  38122  ssbnd  38126  prdsbnd  38131  bfplem2  38161  bfp  38162  renegclALT  39426  0cnALT3  42709  sn-1ne2  42720  itrere  42767  oexpreposd  42771  tan3rdpi  42801  asin1half  42806  readvrec2  42810  sn-00idlem2  42848  sn-00idlem3  42849  sn-00id  42850  sn-0tie0  42913  sn-ltaddpos  42915  sn-ltaddneg  42916  relt0neg1  42918  sn-nnne0  42922  reelznn0nn  42923  sn-0lt1  42937  sn-inelr  42949  sn-itrere  42950  sn-retire  42951  pellexlem6  43283  elpell14qr2  43311  oddcomabszz  43393  zindbi  43395  jm2.24  43412  acongeq  43432  arearect  43664  areaquad  43665  reabsifneg  44080  reabsifnpos  44081  reabsifpos  44082  reabsifnneg  44083  imsqrtvalex  44094  relexp01min  44161  imo72b2lem2  44615  imo72b2lem1  44617  imo72b2  44620  dvconstbi  44782  binomcxplemnn0  44797  binomcxplemdvbinom  44801  binomcxplemcvg  44802  binomcxplemnotnn0  44804  sineq0ALT  45384  halffl  45750  ren0  45851  rexanuz2nf  45941  sqrlearg  46004  limsup10ex  46222  dvnmptdivc  46387  dvnmul  46392  itgsin0pilem1  46399  itgsinexplem1  46403  itgsinexp  46404  iblempty  46414  stoweidlem17  46466  stoweidlem36  46485  stoweidlem55  46504  wallispilem1  46514  wallispilem2  46515  wallispilem4  46517  stirlinglem4  46526  stirlinglem13  46535  stirlinglem14  46536  stirlinglem15  46537  stirlingr  46539  dirker2re  46541  dirkerdenne0  46542  dirkerre  46544  dirkertrigeqlem1  46547  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem11  46567  fourierdlem16  46572  fourierdlem21  46577  fourierdlem22  46578  fourierdlem41  46597  fourierdlem42  46598  fourierdlem48  46603  fourierdlem62  46617  fourierdlem66  46621  fourierdlem79  46634  fourierdlem83  46638  fourierdlem94  46649  fourierdlem102  46657  fourierdlem103  46658  fourierdlem104  46659  fourierdlem111  46666  fourierdlem112  46667  fourierdlem113  46668  fourierdlem114  46669  sqwvfoura  46677  sqwvfourb  46678  fourierswlem  46679  fouriersw  46680  etransclem23  46706  etransclem44  46727  etransclem46  46729  salexct3  46791  salgensscntex  46793  sge0rnn0  46817  sge00  46825  0ome  46978  ovn0lem  47014  ovnhoilem1  47050  smfmullem1  47240  smfmullem2  47241  smfmullem3  47242  smfmullem4  47243  squeezedltsq  47337  goldrapos  47348  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