Theorem 0re 10380

Description: The number 0 is real. Remark: the first step could also be ax-icn 10333. See also 0reALT 10722. (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 10332	. 2 ⊢ 1 ∈ ℂ
2		cnre 10375	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 10345	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 10357	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2847	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 237	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3213	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 474	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3210	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 386   = wceq 1601   ∈ wcel 2107  ∃wrex 3091  (class class class)co 6924  ℂcc 10272  ℝcr 10273  0cc0 10274  1c1 10275  ici 10276   + caddc 10277   · cmul 10279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754  ax-1cn 10332  ax-addrcl 10335  ax-rnegex 10345  ax-cnre 10347

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-clel 2774  df-ral 3095  df-rex 3096

This theorem is referenced by:  0red  10382  0xr  10425  axmulgt0  10453  ne0gt0  10483  00id  10553  mul02lem1  10554  mul02lem2  10555  mul02  10556  addid1  10558  ltaddneg  10593  addgt0  10863  addgegt0  10864  addgtge0  10865  addge0  10866  ltaddpos  10867  ltneg  10877  leneg  10880  lt0neg1  10883  lt0neg2  10884  le0neg1  10885  le0neg2  10886  addge01  10887  suble0  10891  mulge0  10895  msqge0  10898  0le1  10900  relin01  10901  gt0ne0i  10912  gt0ne0d  10941  lt0ne0d  10942  elimge0  11216  ltm1  11219  recgt0  11223  prodgt0  11224  lemul1a  11233  ltmul12a  11235  lemul12a  11237  mulgt1  11238  gt0div  11245  ge0div  11246  mulge0b  11249  lediv12a  11272  recgt1i  11276  recreclt  11278  ledivp1  11281  squeeze0  11282  recgt0ii  11285  ledivp1i  11305  ltdivp1i  11306  fimaxre2  11326  inelr  11368  crne0  11371  nnge1  11408  nngt0  11411  nnnle0  11413  nnne0  11414  nnrecgt0  11422  0le0  11487  neg1lt0  11503  halfge0  11603  nn0ssre  11650  nn0ge0  11673  nn0nlt0  11674  nn0le0eq0  11676  0mnnnnn0  11680  elnnnn0b  11692  elnnnn0c  11693  nn0sub  11698  elnnz  11742  0z  11743  elnn0z  11745  elnnz1  11759  recnz  11808  gtndiv  11810  fnn0ind  11832  10re  11868  rpge0  12156  rpneg  12175  0nrp  12178  0ltpnf  12271  mnflt0  12274  qsqueeze  12348  xneg0  12359  xaddid1  12388  xnn0xadd0  12393  xmulpnf1  12420  xlemul1a  12434  xadddi  12441  xrsupsslem  12453  xrinfmsslem  12454  elrege0  12596  0e0icopnf  12600  elicc01  12608  0elunit  12609  unitssre  12640  0nelfz1  12681  fzpreddisj  12711  fz0to4untppr  12765  nn0p1elfzo  12834  ico01fl0  12943  rpsup  12988  modelico  13003  0mod  13024  1mod  13025  expubnd  13243  le2sq2  13262  sqlecan  13294  bernneq2  13314  expnbnd  13316  expnlbnd  13317  expmulnbnd  13319  discr1  13323  discr  13324  faclbnd  13399  faclbnd3  13401  faclbnd6  13408  bcval4  13416  bcval5  13427  bcpasc  13430  hasheq0  13473  hashneq0  13474  hashnn0n0nn  13499  hashgt12el  13528  hashgt12el2  13529  hashge2el2dif  13580  lsw0  13659  reim0  14269  re0  14303  im0  14304  rei  14307  imi  14308  cj0  14309  sqeqd  14317  rennim  14390  cnpart  14391  sqr0lem  14392  sqrlem4  14397  resqrex  14402  sqrtgt0  14410  sqrt00  14415  sqrtneglem  14418  sqrt9  14425  sqrt2gt1lt2  14426  leabs  14450  absor  14451  max0add  14461  eqsqrt2d  14519  sqrtpclii  14533  rlimconst  14687  rlimrege0  14722  lo1mul  14770  iserge0  14803  fsum00  14938  isumless  14985  arisum2  15001  georeclim  15011  geo2sum  15012  geoisumr  15017  0.999...  15020  cvgrat  15022  fprodge0  15130  bpoly4  15196  cos0  15286  ef01bndlem  15320  sin01bnd  15321  cos01bnd  15322  cos2bnd  15324  sin01gt0  15326  cos01gt0  15327  sincos2sgn  15330  sin4lt0  15331  absef  15333  absefib  15334  efieq1re  15335  epos  15343  znnenlemOLD  15348  rpnnen2lem2  15352  rpnnen2lem3  15353  rpnnen2lem4  15354  rpnnen2lem9  15359  ruclem6  15372  dvdslelem  15442  divalglem1  15528  divalglem5  15531  divalglem6  15532  flodddiv4  15547  sadcadd  15590  gcdn0gt0  15649  nn0seqcvgd  15693  algcvgblem  15700  algcvga  15702  pythagtriplem12  15939  pythagtriplem13  15940  pythagtriplem14  15941  pythagtriplem16  15943  prmreclem4  16031  prmreclem5  16032  prmreclem6  16033  1arith  16039  ramz  16137  mulgnegnn  17942  subgmulg  17996  srgbinomlem4  18934  isabvd  19216  abvtrivd  19236  psrbaglesupp  19769  xrs1mnd  20184  xrs10  20185  rge0srg  20217  psgnodpmr  20335  re0g  20359  mnfnei  21437  imasdsf1olem  22590  ssblps  22639  ssbl  22640  xmeter  22650  dscmet  22789  dscopn  22790  nmoi  22944  nmoeq0  22952  0nghm  22957  idnghm  22959  cnbl0  22989  blcvx  23013  xrsxmet  23024  metdseq0  23069  iicmp  23101  iiconn  23102  iihalf1  23142  iihalf1cn  23143  elii1  23146  icopnfcnv  23153  icopnfhmeo  23154  iccpnfcnv  23155  xrhmeo  23157  xrhmph  23158  htpycc  23191  reparphti  23208  pcoval1  23224  pco0  23225  pcoval2  23227  pcocn  23228  pcohtpylem  23230  pcopt  23233  pcopt2  23234  pcoass  23235  pcorevlem  23237  reust  23591  recusp  23592  rrx0el  23608  minveclem4c  23635  minveclem2  23636  minveclem3b  23638  minveclem4  23642  minveclem7  23645  pjthlem1  23647  cniccbdd  23669  ovolunnul  23708  ovoliunnul  23715  ovolicc1  23724  ovolre  23733  iccvolcl  23775  ovolioo  23776  ioovolcl  23778  ioorcl  23785  vitalilem4  23819  vitalilem5  23820  vitali  23821  ismbf  23836  mbfmulc2lem  23855  mbfpos  23859  mbfposr  23860  i1f0  23895  i1f1  23898  itg1addlem2  23905  itg1addlem4  23907  itg1addlem5  23908  mbfi1fseqlem4  23926  mbfi1fseqlem5  23927  mbfi1fseqlem6  23928  mbfi1flimlem  23930  xrge0f  23939  itg2ge0  23943  itg2const  23948  itg2mulc  23955  itg2splitlem  23956  itg2gt0  23968  itg2cnlem1  23969  ibl0  23994  iblrelem  23998  iblposlem  23999  iblpos  24000  iblre  24001  itgreval  24004  itgneg  24011  iblss  24012  i1fibl  24015  itgitg1  24016  itgle  24017  itgeqa  24021  itgless  24024  iblconst  24025  itgconst  24026  ibladdlem  24027  itgaddlem2  24031  iblabslem  24035  iblabsr  24037  iblmulc2  24038  itgmulc2lem2  24040  itgabs  24042  itgsplit  24043  bddmulibl  24046  dvferm1  24189  dvferm2  24191  dvferm  24192  dvlip  24197  c1lip1  24201  dveq0  24204  dv11cn  24205  dvne0  24215  ftc1lem4  24243  ply1divex  24337  dgrco  24472  plyrecj  24476  vieta1lem2  24507  aalioulem2  24529  aalioulem3  24530  pserulm  24617  psercnlem2  24619  psercnlem1  24620  psercn  24621  abelthlem6  24631  abelth  24636  reeff1olem  24641  reeff1o  24642  pilem2  24647  pilem3  24648  pilem3OLD  24649  pipos  24654  sinhalfpilem  24657  sincosq1sgn  24692  sincosq2sgn  24693  coseq00topi  24696  coseq0negpitopi  24697  tangtx  24699  tanabsge  24700  sinq12ge0  24702  sinq34lt0t  24703  cosq14ge0  24705  sincos4thpi  24707  sincos6thpi  24709  pige3  24711  sineq0  24715  cosordlem  24719  cosord  24720  cos11  24721  sinord  24722  recosf1o  24723  resinf1o  24724  tanord1  24725  tanord  24726  tanregt0  24727  efif1olem4  24733  efifo  24735  relogrn  24749  log1  24773  logneg  24775  argregt0  24797  argrege0  24798  argimgt0  24799  logneg2  24802  logdivlti  24807  logdivlt  24808  ellogdm  24826  logdmn0  24827  logdmnrp  24828  logcnlem3  24831  dvloglem  24835  logdmopn  24836  logf1o2  24837  dvlog2lem  24839  efopnlem1  24843  logtayl  24847  recxpcl  24862  cxpge0  24870  cxple2  24884  cxple2a  24886  cxpsqrtlem  24889  cxpcn3  24933  cxpaddlelem  24936  cxpaddle  24937  loglesqrt  24943  logbrec  24964  ang180lem3  24993  ang180lem4  24994  chordthmlem4  25017  heron  25020  asinneg  25068  asin1  25076  reasinsin  25078  acosbnd  25082  atan0  25090  atanrecl  25093  atanlogaddlem  25095  atanlogsublem  25097  atanlogsub  25098  atantan  25105  atanbnd  25108  atan1  25110  atans2  25113  ressatans  25116  log2cnv  25127  log2tlbnd  25128  log2ub  25132  log2le1  25133  rlimcnp  25148  rlimcnp2  25149  o1cxp  25157  jensen  25171  amgm  25173  emgt0  25189  harmonicbnd3  25190  harmoniclbnd  25191  harmonicbnd4  25193  zetacvg  25197  eldmgm  25204  lgamgulmlem2  25212  basellem3  25265  basellem8  25270  efnnfsumcl  25285  ppisval  25286  vmage0  25303  chpge0  25308  efchtdvds  25341  ppiltx  25359  ppiub  25385  chpeq0  25389  chteq0  25390  chtleppi  25391  chpchtsum  25400  chpub  25401  dchr1re  25444  bcmono  25458  efexple  25462  bposlem1  25465  bposlem4  25468  bposlem5  25469  bposlem7  25471  bposlem8  25472  bposlem9  25473  lgsval2lem  25488  lgsval4a  25500  lgsneg  25502  lgsdilem  25505  lgsdir2lem1  25506  2lgsoddprmlem3a  25591  2lgsoddprmlem3b  25592  2lgsoddprmlem3c  25593  2lgsoddprmlem3d  25594  rplogsumlem2  25630  rpvmasumlem  25632  dchrisum0flblem1  25653  dchrisum0flblem2  25654  dchrisum0fno1  25656  rplogsum  25672  logdivsum  25678  mulog2sumlem2  25680  selberg2lem  25695  logdivbnd  25701  pntrsumo1  25710  pntrlog2bndlem4  25725  pntrlog2bndlem5  25726  pntpbnd1  25731  pntpbnd2  25732  pntlem3  25754  pntleml  25756  ostth2  25782  trgcgrg  25870  ttgcontlem1  26238  axlowdimlem1  26295  axlowdimlem6  26300  axlowdimlem7  26301  axlowdimlem10  26304  axlowdim1  26312  axlowdim2  26313  axlowdim  26314  elntg2  26338  umgrislfupgrlem  26474  lfgrnloop  26477  lfuhgr1v0e  26605  usgrexmplef  26610  pthdlem2  27124  crctcshwlkn0lem7  27169  rusgrnumwwlks  27358  rusgrnumwwlksOLD  27359  clwwlkn0  27421  konigsberg  27667  ex-po  27871  ex-sqrt  27890  ex-gcd  27893  nvz0  28099  0blo  28223  nmlno0lem  28224  nmblolbii  28230  siilem2  28283  minvecolem2  28307  minvecolem3  28308  minvecolem4c  28311  minvecolem4  28312  minvecolem5  28313  minvecolem7  28315  htthlem  28350  hiidge0  28531  normlem6  28548  normgt0  28560  norm-i  28562  normpyc  28579  bcsiALT  28612  pjhthlem1  28826  pjneli  29158  nmlnop0iALT  29430  unopbd  29450  nmbdoplbi  29459  nmcoplbi  29463  nmbdfnlbi  29484  nmbdfnlb  29485  nmcfnlbi  29487  cnlnadjlem7  29508  nmopcoi  29530  branmfn  29540  leopmul  29569  nmopleid  29574  pjbdlni  29584  pjnormssi  29603  stle0i  29674  cdj3lem1  29869  xaddeq0  30087  pr01ssre  30138  dp20u  30152  dp20h  30153  dp2clq  30155  dp2lt10  30158  dp2lt  30159  dp0u  30175  dplti  30179  dpexpp1  30182  xdiv0  30203  xrge0slmod  30410  unitdivcld  30549  sqsscirc1  30556  xrge0iifcnv  30581  xrge0iifiso  30583  rezh  30617  indf  30679  indfval  30680  esumcvgsum  30752  voliune  30894  volfiniune  30895  sibfinima  31003  sitmcl  31015  0rrv  31116  coinfliprv  31147  ballotlem2  31153  ballotlem4  31163  ballotlemi1  31167  ballotlemic  31171  sgnclre  31204  sgnnbi  31210  sgnpbi  31211  plymulx0  31228  signsply0  31232  signswch  31242  signstf  31247  signstf0  31249  signstfveq0  31259  signstfveq0OLD  31260  signlem0  31270  itgexpif  31290  hgt750lemd  31332  hgt750lem  31335  hgt750lem2  31336  hgt750leme  31342  iisconn  31837  iillysconn  31838  cvmliftlem10  31879  fz0n  32214  logi  32218  bcneg1  32220  nn0prpwlem  32909  dnizeq0  33052  dnizphlfeqhlf  33053  knoppndvlem13  33101  cnndvlem1  33114  bj-pinftyccb  33702  bj-minftyccb  33706  bj-pinftynminfty  33708  taupilemrplb  33765  sin2h  34029  tan2h  34031  ptrecube  34040  poimirlem16  34056  poimirlem17  34057  poimirlem20  34060  poimirlem22  34062  poimirlem23  34063  poimirlem29  34069  poimirlem31  34071  poimir  34073  heicant  34075  mblfinlem2  34078  ismblfin  34081  ovoliunnfl  34082  voliunnfl  34084  volsupnfl  34085  mbfposadd  34087  itg2addnclem  34091  itg2addnclem2  34092  ibladdnclem  34096  itgaddnclem2  34099  iblabsnclem  34103  iblmulc2nc  34105  itgmulc2nclem2  34107  itgabsnc  34109  ftc1cnnclem  34113  ftc1anclem5  34119  ftc1anclem8  34122  asindmre  34125  dvasin  34126  areacirclem4  34133  areacirc  34135  isbnd3  34212  ssbnd  34216  prdsbnd  34221  bfplem2  34251  bfp  34252  renegclALT  35122  0cnALT3  38146  oexpreposd  38165  pellexlem6  38368  elpell14qr2  38396  oddcomabszz  38478  zindbi  38480  jm2.24  38499  acongeq  38519  arearect  38769  areaquad  38770  relexp01min  38972  imo72b2lem0  39431  imo72b2lem2  39433  imo72b2lem1  39437  imo72b2  39441  dvconstbi  39499  binomcxplemnn0  39514  binomcxplemdvbinom  39518  binomcxplemcvg  39519  binomcxplemnotnn0  39521  sineq0ALT  40116  halffl  40429  ren0  40542  sqrlearg  40698  limsup10ex  40923  liminf10ex  40924  dvnmptdivc  41091  dvnmul  41096  itgsin0pilem1  41103  itgsinexplem1  41107  itgsinexp  41108  iblempty  41118  stoweidlem17  41171  stoweidlem36  41190  stoweidlem55  41209  wallispilem1  41219  wallispilem2  41220  wallispilem4  41222  stirlinglem4  41231  stirlinglem13  41240  stirlinglem14  41241  stirlinglem15  41242  stirlingr  41244  dirker2re  41246  dirkerdenne0  41247  dirkerre  41249  dirkertrigeqlem1  41252  dirkercncflem2  41258  dirkercncflem4  41260  fourierdlem11  41272  fourierdlem16  41277  fourierdlem21  41282  fourierdlem22  41283  fourierdlem41  41302  fourierdlem42  41303  fourierdlem48  41308  fourierdlem62  41322  fourierdlem66  41326  fourierdlem79  41339  fourierdlem83  41343  fourierdlem94  41354  fourierdlem102  41362  fourierdlem103  41363  fourierdlem104  41364  fourierdlem111  41371  fourierdlem112  41372  fourierdlem113  41373  fourierdlem114  41374  sqwvfoura  41382  sqwvfourb  41383  fourierswlem  41384  fouriersw  41385  etransclem23  41411  etransclem44  41432  etransclem46  41434  salexct3  41494  salgensscntex  41496  sge0rnn0  41519  sge00  41527  0ome  41680  ovn0lem  41716  ovnhoilem1  41752  smfmullem1  41935  smfmullem2  41936  smfmullem3  41937  smfmullem4  41938  zm1nn  42354  sqrtnegnre  42359  m1mod0mod1  42381  fmtnoprmfac2lem1  42509  31prm  42543  mod42tp1mod8  42550  tgblthelfgott  42738  altgsumbcALT  43156  expnegico01  43333  dignnld  43422  eenglngeehlnmlem1  43483  line2ylem  43497  line2y  43501  itsclc0yqsollem2  43509  ex-gt  43587