Theorem 0re 11260

Description: The number 0 is real. Remark: the first step could also be ax-icn 11211. See also 0reALT 11603. (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 11210	. 2 ⊢ 1 ∈ ℂ
2		cnre 11255	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11223	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11235	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2826	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3152	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3144	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1536   ∈ wcel 2105  ∃wrex 3067  (class class class)co 7430  ℂcc 11150  ℝcr 11151  0cc0 11152  1c1 11153  ici 11154   + caddc 11155   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addrcl 11213  ax-rnegex 11223  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-rex 3068

This theorem is referenced by:  0red  11261  0xr  11305  axmulgt0  11332  ne0gt0  11363  00id  11433  mul02lem1  11434  mul02lem2  11435  mul02  11436  addrid  11438  ltaddneg  11474  addgt0  11746  addgegt0  11747  addgtge0  11748  addge0  11749  ltaddpos  11750  ltneg  11760  leneg  11763  lt0neg1  11766  lt0neg2  11767  le0neg1  11768  le0neg2  11769  addge01  11770  suble0  11774  mulge0  11778  msqge0  11781  0le1  11783  relin01  11784  gt0ne0i  11795  gt0ne0d  11824  lt0ne0d  11825  elimge0  12103  ltm1  12106  recgt0  12110  prodgt0  12111  lemul1a  12118  ltmul12a  12120  lemul12a  12122  mulgt1OLD  12123  gt0div  12131  ge0div  12132  mulge0b  12135  lediv12a  12158  recgt1i  12162  recreclt  12164  ledivp1  12167  squeeze0  12168  recgt0ii  12171  ledivp1i  12190  ltdivp1i  12191  fimaxre2  12210  inelr  12253  crne0  12256  nnge1  12291  nngt0  12294  nnnle0  12296  nnne0  12297  nnrecgt0  12306  0le0  12364  neg1lt0  12380  halfge0  12480  nn0ssre  12527  nn0ge0  12548  nn0nlt0  12549  nn0le0eq0  12551  0mnnnnn0  12555  elnnnn0b  12567  elnnnn0c  12568  nn0sub  12573  elnnz  12620  0z  12621  elnn0z  12623  elnnz1  12640  recnz  12690  gtndiv  12692  fnn0ind  12714  10re  12749  rpge0  13045  rpneg  13064  0nrp  13067  0ltpnf  13161  mnflt0  13164  qsqueeze  13239  xneg0  13250  xaddrid  13279  xnn0xadd0  13285  xmulpnf1  13312  xlemul1a  13326  xadddi  13333  xrsupsslem  13345  xrinfmsslem  13346  elrege0  13490  0e0icopnf  13494  elicc01  13502  0elunit  13505  unitssre  13535  0nelfz1  13579  fzpreddisj  13609  fz0to4untppr  13666  fz0to5un2tp  13667  nn0p1elfzo  13738  ico01fl0  13855  rpsup  13902  modelico  13917  0mod  13938  1mod  13939  le2sq2  14171  expubnd  14213  sqlecan  14244  bernneq2  14265  expnbnd  14267  expnlbnd  14268  expmulnbnd  14270  discr1  14274  discr  14275  faclbnd  14325  faclbnd3  14327  faclbnd6  14334  bcval4  14342  bcval5  14353  bcpasc  14356  hasheq0  14398  hashneq0  14399  hashnn0n0nn  14426  hashgt12el  14457  hashgt12el2  14458  hashge2el2dif  14515  lsw0  14599  swrdccatin2  14763  pfxccatin12lem3  14766  reim0  15153  re0  15187  im0  15188  rei  15191  imi  15192  cj0  15193  sqeqd  15201  rennim  15274  cnpart  15275  sqrt0  15276  01sqrexlem4  15280  resqrex  15285  sqrtgt0  15293  sqrt00  15298  sqrtneglem  15301  sqrt9  15308  sqrt2gt1lt2  15309  leabs  15334  absor  15335  max0add  15345  eqsqrt2d  15403  sqrtpclii  15417  rlimconst  15576  rlimrege0  15611  lo1mul  15660  iserge0  15693  fsum00  15830  isumless  15877  arisum2  15893  georeclim  15904  geo2sum  15905  geoisumr  15910  0.999...  15913  cvgrat  15915  fprodge0  16025  bpoly4  16091  cos0  16182  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  cos2bnd  16220  sin01gt0  16222  cos01gt0  16223  sincos2sgn  16226  sin4lt0  16227  absef  16229  absefib  16230  efieq1re  16231  epos  16239  rpnnen2lem2  16247  rpnnen2lem3  16248  rpnnen2lem4  16249  rpnnen2lem9  16254  ruclem6  16267  dvdslelem  16342  divalglem1  16427  divalglem5  16430  divalglem6  16431  flodddiv4  16448  sadcadd  16491  gcdn0gt0  16551  nn0seqcvgd  16603  algcvgblem  16610  algcvga  16612  pythagtriplem12  16859  pythagtriplem13  16860  pythagtriplem14  16861  pythagtriplem16  16863  prmreclem4  16952  prmreclem5  16953  prmreclem6  16954  1arith  16960  ramz  17058  mulgnegnn  19114  subgmulg  19170  srgbinomlem4  20246  isabvd  20829  abvtrivd  20849  xrs1mnd  21439  xrs10  21440  rge0srg  21473  psgnodpmr  21625  re0g  21647  psrbaglesupp  21959  mnfnei  23244  imasdsf1olem  24398  ssblps  24447  ssbl  24448  xmeter  24458  dscmet  24600  dscopn  24601  nmoi  24764  nmoeq0  24772  0nghm  24777  idnghm  24779  cnbl0  24809  xrsxmet  24844  metdseq0  24889  iicmp  24925  iiconn  24926  iihalf1  24971  iihalf1cnOLD  24973  elii1  24977  icopnfcnv  24986  icopnfhmeo  24987  iccpnfcnv  24988  xrhmeo  24990  xrhmph  24991  htpycc  25025  reparphti  25042  reparphtiOLD  25043  pcoval1  25059  pco0  25060  pcoval2  25062  pcocn  25063  pcohtpylem  25065  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  reust  25428  recusp  25429  rrx0el  25445  minveclem4c  25472  minveclem2  25473  minveclem3b  25475  minveclem4  25479  minveclem7  25482  pjthlem1  25484  cniccbdd  25509  ovolunnul  25548  ovoliunnul  25555  ovolicc1  25564  ovolre  25573  iccvolcl  25615  ovolioo  25616  ioovolcl  25618  ioorcl  25625  vitalilem4  25659  vitalilem5  25660  vitali  25661  ismbf  25676  mbfmulc2lem  25695  mbfpos  25699  mbfposr  25700  i1f0  25735  i1f1  25738  itg1addlem2  25745  itg1addlem4  25747  itg1addlem4OLD  25748  itg1addlem5  25749  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1flimlem  25771  xrge0f  25780  itg2ge0  25784  itg2const  25789  itg2mulc  25796  itg2splitlem  25797  itg2gt0  25809  itg2cnlem1  25810  ibl0  25836  iblrelem  25840  iblposlem  25841  iblpos  25842  iblre  25843  itgreval  25846  itgneg  25853  iblss  25854  i1fibl  25857  itgitg1  25858  itgle  25859  itgeqa  25863  itgless  25866  iblconst  25867  itgconst  25868  ibladdlem  25869  itgaddlem2  25873  iblabslem  25877  iblabsr  25879  iblmulc2  25880  itgmulc2lem2  25882  itgabs  25884  itgsplit  25885  bddmulibl  25888  dvferm1  26037  dvferm2  26039  dvferm  26040  dvlip  26046  c1lip1  26050  dveq0  26053  dv11cn  26054  dvne0  26064  ftc1lem4  26094  ply1divex  26190  dgrco  26329  plyrecj  26335  vieta1lem2  26367  aalioulem2  26389  aalioulem3  26390  pserulm  26479  psercnlem2  26482  psercnlem1  26483  psercn  26484  abelth  26499  reeff1olem  26504  reeff1o  26505  pilem2  26510  pilem3  26511  pipos  26516  sinhalfpilem  26519  sincosq1sgn  26554  sincosq2sgn  26555  coseq00topi  26558  coseq0negpitopi  26559  tangtx  26561  tanabsge  26562  sinq12ge0  26564  sinq34lt0t  26565  cosq14ge0  26567  sincos4thpi  26569  sincos6thpi  26572  pige3ALT  26576  sineq0  26580  cosordlem  26586  cosord  26587  cos0pilt1  26588  cos11  26589  sinord  26590  recosf1o  26591  resinf1o  26592  tanord1  26593  tanord  26594  tanregt0  26595  efif1olem4  26601  efifo  26603  relogrn  26617  log1  26641  logi  26643  logneg  26644  argregt0  26666  argrege0  26667  argimgt0  26668  logneg2  26671  logdivlti  26676  logdivlt  26677  ellogdm  26695  logdmn0  26696  logdmnrp  26697  logcnlem3  26700  dvloglem  26704  logdmopn  26705  logf1o2  26706  dvlog2lem  26708  efopnlem1  26712  logtayl  26716  recxpcl  26731  cxpge0  26739  cxple2  26753  cxple2a  26755  cxpsqrtlem  26758  cxpcn3  26805  cxpaddlelem  26808  cxpaddle  26809  loglesqrt  26818  logbrec  26839  ang180lem3  26868  ang180lem4  26869  asinneg  26943  asin1  26951  reasinsin  26953  acosbnd  26957  atan0  26965  atanrecl  26968  atanlogaddlem  26970  atanlogsublem  26972  atanlogsub  26973  atantan  26980  atanbnd  26983  atan1  26985  atans2  26988  ressatans  26991  log2cnv  27001  log2tlbnd  27002  log2ub  27006  log2le1  27007  rlimcnp  27022  rlimcnp2  27023  o1cxp  27032  jensen  27046  amgm  27048  emgt0  27064  harmonicbnd3  27065  harmoniclbnd  27066  harmonicbnd4  27068  zetacvg  27072  eldmgm  27079  lgamgulmlem2  27087  basellem3  27140  basellem8  27145  efnnfsumcl  27160  ppisval  27161  vmage0  27178  chpge0  27183  efchtdvds  27216  ppiltx  27234  ppiub  27262  chpeq0  27266  chteq0  27267  chtleppi  27268  chpchtsum  27277  chpub  27278  dchr1re  27321  bcmono  27335  efexple  27339  bposlem1  27342  bposlem4  27345  bposlem5  27346  bposlem7  27348  bposlem8  27349  bposlem9  27350  lgsval2lem  27365  lgsval4a  27377  lgsneg  27379  lgsdilem  27382  lgsdir2lem1  27383  2lgsoddprmlem3a  27468  2lgsoddprmlem3b  27469  2lgsoddprmlem3c  27470  2lgsoddprmlem3d  27471  rplogsumlem2  27543  rpvmasumlem  27545  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0fno1  27569  rplogsum  27585  logdivsum  27591  mulog2sumlem2  27593  selberg2lem  27608  logdivbnd  27614  pntrsumo1  27623  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntpbnd1  27644  pntpbnd2  27645  pntlem3  27667  pntleml  27669  ostth2  27695  trgcgrg  28537  ttgcontlem1  28913  axlowdimlem1  28971  axlowdimlem6  28976  axlowdimlem7  28977  axlowdimlem10  28980  axlowdim1  28988  axlowdim2  28989  axlowdim  28990  elntg2  29014  umgrislfupgrlem  29153  lfgrnloop  29156  lfuhgr1v0e  29285  usgrexmplef  29290  pthdlem2  29800  crctcshwlkn0lem7  29845  rusgrnumwwlks  30003  clwwlkn0  30056  konigsberg  30285  ex-po  30463  ex-sqrt  30482  ex-gcd  30485  nvz0  30696  0blo  30820  nmlno0lem  30821  nmblolbii  30827  siilem2  30880  minvecolem2  30903  minvecolem3  30904  minvecolem4c  30907  minvecolem4  30908  minvecolem5  30909  minvecolem7  30911  htthlem  30945  hiidge0  31126  normlem6  31143  normgt0  31155  norm-i  31157  normpyc  31174  bcsiALT  31207  pjhthlem1  31419  pjneli  31751  nmlnop0iALT  32023  unopbd  32043  nmbdoplbi  32052  nmcoplbi  32056  nmbdfnlbi  32077  nmbdfnlb  32078  nmcfnlbi  32080  cnlnadjlem7  32101  nmopcoi  32123  branmfn  32133  leopmul  32162  nmopleid  32167  pjbdlni  32177  pjnormssi  32196  stle0i  32267  cdj3lem1  32462  xaddeq0  32763  expgt0b  32822  pr01ssre  32830  dp20u  32844  dp20h  32845  dp2clq  32847  dp2lt10  32850  dp2lt  32851  dp0u  32867  dplti  32871  dpexpp1  32874  xdiv0  32895  chnub  32985  xrge0slmod  33355  evl1deg3  33582  fldext2chn  33733  unitdivcld  33861  sqsscirc1  33868  xrge0iifcnv  33893  xrge0iifiso  33895  rezh  33931  indf  33995  indfval  33996  esumcvgsum  34068  voliune  34209  volfiniune  34210  sibfinima  34320  sitmcl  34332  0rrv  34432  coinfliprv  34463  ballotlem2  34469  ballotlem4  34479  ballotlemi1  34483  ballotlemic  34487  sgnclre  34520  sgnnbi  34526  sgnpbi  34527  plymulx0  34540  signsply0  34544  signswch  34554  signstf  34559  signstf0  34561  signstfveq0  34570  signlem0  34580  signshf  34581  itgexpif  34599  hgt750lemd  34641  hgt750lem  34644  hgt750lem2  34645  hgt750leme  34651  iisconn  35236  iillysconn  35237  cvmliftlem10  35278  fz0n  35710  bcneg1  35715  nn0prpwlem  36304  dnizeq0  36457  dnizphlfeqhlf  36458  knoppndvlem13  36506  cnndvlem1  36519  bj-pinftyccb  37203  bj-minftyccb  37207  bj-pinftynminfty  37209  taupilemrplb  37302  irrdiff  37308  sin2h  37596  tan2h  37598  ptrecube  37606  poimirlem16  37622  poimirlem17  37623  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem29  37635  poimirlem31  37637  poimir  37639  heicant  37641  mblfinlem2  37644  ismblfin  37647  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  mbfposadd  37653  itg2addnclem  37657  itg2addnclem2  37658  ibladdnclem  37662  itgaddnclem2  37665  iblabsnclem  37669  iblmulc2nc  37671  itgmulc2nclem2  37673  itgabsnc  37675  ftc1cnnclem  37677  ftc1anclem5  37683  ftc1anclem8  37686  asindmre  37689  dvasin  37690  areacirclem4  37697  areacirc  37699  isbnd3  37770  ssbnd  37774  prdsbnd  37779  bfplem2  37809  bfp  37810  renegclALT  38944  2xp3dxp2ge1d  42222  factwoffsmonot  42223  0cnALT3  42272  sn-1ne2  42278  itrere  42331  oexpreposd  42335  tan3rdpi  42364  asin1half  42365  readvrec2  42369  sn-00idlem2  42405  sn-00idlem3  42406  sn-00id  42407  sn-0tie0  42445  sn-ltaddpos  42447  sn-ltaddneg  42448  relt0neg1  42450  sn-nnne0  42454  reelznn0nn  42455  sn-0lt1  42469  sn-inelr  42473  sn-itrere  42474  sn-retire  42475  pellexlem6  42821  elpell14qr2  42849  oddcomabszz  42932  zindbi  42934  jm2.24  42951  acongeq  42971  arearect  43203  areaquad  43204  reabsifneg  43621  reabsifnpos  43622  reabsifpos  43623  reabsifnneg  43624  imsqrtvalex  43635  relexp01min  43702  imo72b2lem2  44156  imo72b2lem1  44158  imo72b2  44161  dvconstbi  44329  binomcxplemnn0  44344  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemnotnn0  44351  sineq0ALT  44934  halffl  45246  ren0  45351  rexanuz2nf  45442  sqrlearg  45505  limsup10ex  45728  dvnmptdivc  45893  dvnmul  45898  itgsin0pilem1  45905  itgsinexplem1  45909  itgsinexp  45910  iblempty  45920  stoweidlem17  45972  stoweidlem36  45991  stoweidlem55  46010  wallispilem1  46020  wallispilem2  46021  wallispilem4  46023  stirlinglem4  46032  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  stirlingr  46045  dirker2re  46047  dirkerdenne0  46048  dirkerre  46050  dirkertrigeqlem1  46053  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem11  46073  fourierdlem16  46078  fourierdlem21  46083  fourierdlem22  46084  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem62  46123  fourierdlem66  46127  fourierdlem79  46140  fourierdlem83  46144  fourierdlem94  46155  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fourierdlem114  46175  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  etransclem23  46212  etransclem44  46233  etransclem46  46235  salexct3  46297  salgensscntex  46299  sge0rnn0  46323  sge00  46331  0ome  46484  ovn0lem  46520  ovnhoilem1  46556  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  smfmullem4  46749  zm1nn  47251  sqrtnegnre  47256  m1mod0mod1  47293  fmtnoprmfac2lem1  47490  31prm  47521  mod42tp1mod8  47526  nfermltl2rev  47667  tgblthelfgott  47739  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb0  47925  usgrexmpl2nb5  47930  usgrexmpl2trifr  47931  gpgusgralem  47945  altgsumbcALT  48197  expnegico01  48363  dignnld  48452  eenglngeehlnmlem1  48586  line2ylem  48600  line2y  48604  itsclc0yqsollem2  48612  icccldii  48714  i0oii  48715  sepfsepc  48723  ex-gt  48958