Theorem 0re 11198

Description: The number 0 is real. Remark: the first step could also be ax-icn 11151. See also 0reALT 11539. (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 11150	. 2 ⊢ 1 ∈ ℂ
2		cnre 11193	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11163	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11175	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2820	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 244	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3154	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 481	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3146	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∃wrex 3069  (class class class)co 7393  ℂcc 11090  ℝcr 11091  0cc0 11092  1c1 11093  ici 11094   + caddc 11095   · cmul 11097

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11150  ax-addrcl 11153  ax-rnegex 11163  ax-cnre 11165

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809  df-rex 3070

This theorem is referenced by:  0red  11199  0xr  11243  axmulgt0  11270  ne0gt0  11301  00id  11371  mul02lem1  11372  mul02lem2  11373  mul02  11374  addrid  11376  ltaddneg  11411  addgt0  11682  addgegt0  11683  addgtge0  11684  addge0  11685  ltaddpos  11686  ltneg  11696  leneg  11699  lt0neg1  11702  lt0neg2  11703  le0neg1  11704  le0neg2  11705  addge01  11706  suble0  11710  mulge0  11714  msqge0  11717  0le1  11719  relin01  11720  gt0ne0i  11731  gt0ne0d  11760  lt0ne0d  11761  elimge0  12035  ltm1  12038  recgt0  12042  prodgt0  12043  lemul1a  12050  ltmul12a  12052  lemul12a  12054  mulgt1  12055  gt0div  12062  ge0div  12063  mulge0b  12066  lediv12a  12089  recgt1i  12093  recreclt  12095  ledivp1  12098  squeeze0  12099  recgt0ii  12102  ledivp1i  12121  ltdivp1i  12122  fimaxre2  12141  inelr  12184  crne0  12187  nnge1  12222  nngt0  12225  nnnle0  12227  nnne0  12228  nnrecgt0  12237  0le0  12295  neg1lt0  12311  halfge0  12411  nn0ssre  12458  nn0ge0  12479  nn0nlt0  12480  nn0le0eq0  12482  0mnnnnn0  12486  elnnnn0b  12498  elnnnn0c  12499  nn0sub  12504  elnnz  12550  0z  12551  elnn0z  12553  elnnz1  12570  recnz  12619  gtndiv  12621  fnn0ind  12643  10re  12678  rpge0  12969  rpneg  12988  0nrp  12991  0ltpnf  13084  mnflt0  13087  qsqueeze  13162  xneg0  13173  xaddrid  13202  xnn0xadd0  13208  xmulpnf1  13235  xlemul1a  13249  xadddi  13256  xrsupsslem  13268  xrinfmsslem  13269  elrege0  13413  0e0icopnf  13417  elicc01  13425  0elunit  13428  unitssre  13458  0nelfz1  13502  fzpreddisj  13532  fz0to4untppr  13586  nn0p1elfzo  13657  ico01fl0  13766  rpsup  13813  modelico  13828  0mod  13849  1mod  13850  le2sq2  14082  expubnd  14124  sqlecan  14155  bernneq2  14175  expnbnd  14177  expnlbnd  14178  expmulnbnd  14180  discr1  14184  discr  14185  faclbnd  14232  faclbnd3  14234  faclbnd6  14241  bcval4  14249  bcval5  14260  bcpasc  14263  hasheq0  14305  hashneq0  14306  hashnn0n0nn  14333  hashgt12el  14364  hashgt12el2  14365  hashge2el2dif  14423  lsw0  14497  swrdccatin2  14661  pfxccatin12lem3  14664  reim0  15047  re0  15081  im0  15082  rei  15085  imi  15086  cj0  15087  sqeqd  15095  rennim  15168  cnpart  15169  sqrt0  15170  01sqrexlem4  15174  resqrex  15179  sqrtgt0  15187  sqrt00  15192  sqrtneglem  15195  sqrt9  15202  sqrt2gt1lt2  15203  leabs  15228  absor  15229  max0add  15239  eqsqrt2d  15297  sqrtpclii  15311  rlimconst  15470  rlimrege0  15505  lo1mul  15554  iserge0  15589  fsum00  15726  isumless  15773  arisum2  15789  georeclim  15800  geo2sum  15801  geoisumr  15806  0.999...  15809  cvgrat  15811  fprodge0  15919  bpoly4  15985  cos0  16075  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  cos2bnd  16113  sin01gt0  16115  cos01gt0  16116  sincos2sgn  16119  sin4lt0  16120  absef  16122  absefib  16123  efieq1re  16124  epos  16132  rpnnen2lem2  16140  rpnnen2lem3  16141  rpnnen2lem4  16142  rpnnen2lem9  16147  ruclem6  16160  dvdslelem  16234  divalglem1  16319  divalglem5  16322  divalglem6  16323  flodddiv4  16338  sadcadd  16381  gcdn0gt0  16441  nn0seqcvgd  16489  algcvgblem  16496  algcvga  16498  pythagtriplem12  16741  pythagtriplem13  16742  pythagtriplem14  16743  pythagtriplem16  16745  prmreclem4  16834  prmreclem5  16835  prmreclem6  16836  1arith  16842  ramz  16940  mulgnegnn  18936  subgmulg  18992  srgbinomlem4  20010  isabvd  20377  abvtrivd  20397  xrs1mnd  20917  xrs10  20918  rge0srg  20950  psgnodpmr  21076  re0g  21098  psrbaglesupp  21408  psrbaglesuppOLD  21409  mnfnei  22654  imasdsf1olem  23808  ssblps  23857  ssbl  23858  xmeter  23868  dscmet  24010  dscopn  24011  nmoi  24174  nmoeq0  24182  0nghm  24187  idnghm  24189  cnbl0  24219  xrsxmet  24254  metdseq0  24299  iicmp  24331  iiconn  24332  iihalf1  24376  iihalf1cn  24377  elii1  24380  icopnfcnv  24387  icopnfhmeo  24388  iccpnfcnv  24389  xrhmeo  24391  xrhmph  24392  htpycc  24425  reparphti  24442  pcoval1  24458  pco0  24459  pcoval2  24461  pcocn  24462  pcohtpylem  24464  pcopt  24467  pcopt2  24468  pcoass  24469  pcorevlem  24471  reust  24827  recusp  24828  rrx0el  24844  minveclem4c  24871  minveclem2  24872  minveclem3b  24874  minveclem4  24878  minveclem7  24881  pjthlem1  24883  cniccbdd  24907  ovolunnul  24946  ovoliunnul  24953  ovolicc1  24962  ovolre  24971  iccvolcl  25013  ovolioo  25014  ioovolcl  25016  ioorcl  25023  vitalilem4  25057  vitalilem5  25058  vitali  25059  ismbf  25074  mbfmulc2lem  25093  mbfpos  25097  mbfposr  25098  i1f0  25133  i1f1  25136  itg1addlem2  25143  itg1addlem4  25145  itg1addlem4OLD  25146  itg1addlem5  25147  mbfi1fseqlem4  25165  mbfi1fseqlem5  25166  mbfi1flimlem  25169  xrge0f  25178  itg2ge0  25182  itg2const  25187  itg2mulc  25194  itg2splitlem  25195  itg2gt0  25207  itg2cnlem1  25208  ibl0  25233  iblrelem  25237  iblposlem  25238  iblpos  25239  iblre  25240  itgreval  25243  itgneg  25250  iblss  25251  i1fibl  25254  itgitg1  25255  itgle  25256  itgeqa  25260  itgless  25263  iblconst  25264  itgconst  25265  ibladdlem  25266  itgaddlem2  25270  iblabslem  25274  iblabsr  25276  iblmulc2  25277  itgmulc2lem2  25279  itgabs  25281  itgsplit  25282  bddmulibl  25285  dvferm1  25431  dvferm2  25433  dvferm  25434  dvlip  25439  c1lip1  25443  dveq0  25446  dv11cn  25447  dvne0  25457  ftc1lem4  25485  ply1divex  25583  dgrco  25718  plyrecj  25722  vieta1lem2  25753  aalioulem2  25775  aalioulem3  25776  pserulm  25863  psercnlem2  25865  psercnlem1  25866  psercn  25867  abelth  25882  reeff1olem  25887  reeff1o  25888  pilem2  25893  pilem3  25894  pipos  25899  sinhalfpilem  25902  sincosq1sgn  25937  sincosq2sgn  25938  coseq00topi  25941  coseq0negpitopi  25942  tangtx  25944  tanabsge  25945  sinq12ge0  25947  sinq34lt0t  25948  cosq14ge0  25950  sincos4thpi  25952  sincos6thpi  25954  pige3ALT  25958  sineq0  25962  cosordlem  25968  cosord  25969  cos0pilt1  25970  cos11  25971  sinord  25972  recosf1o  25973  resinf1o  25974  tanord1  25975  tanord  25976  tanregt0  25977  efif1olem4  25983  efifo  25985  relogrn  25999  log1  26023  logneg  26025  argregt0  26047  argrege0  26048  argimgt0  26049  logneg2  26052  logdivlti  26057  logdivlt  26058  ellogdm  26076  logdmn0  26077  logdmnrp  26078  logcnlem3  26081  dvloglem  26085  logdmopn  26086  logf1o2  26087  dvlog2lem  26089  efopnlem1  26093  logtayl  26097  recxpcl  26112  cxpge0  26120  cxple2  26134  cxple2a  26136  cxpsqrtlem  26139  cxpcn3  26183  cxpaddlelem  26186  cxpaddle  26187  loglesqrt  26193  logbrec  26214  ang180lem3  26243  ang180lem4  26244  asinneg  26318  asin1  26326  reasinsin  26328  acosbnd  26332  atan0  26340  atanrecl  26343  atanlogaddlem  26345  atanlogsublem  26347  atanlogsub  26348  atantan  26355  atanbnd  26358  atan1  26360  atans2  26363  ressatans  26366  log2cnv  26376  log2tlbnd  26377  log2ub  26381  log2le1  26382  rlimcnp  26397  rlimcnp2  26398  o1cxp  26406  jensen  26420  amgm  26422  emgt0  26438  harmonicbnd3  26439  harmoniclbnd  26440  harmonicbnd4  26442  zetacvg  26446  eldmgm  26453  lgamgulmlem2  26461  basellem3  26514  basellem8  26519  efnnfsumcl  26534  ppisval  26535  vmage0  26552  chpge0  26557  efchtdvds  26590  ppiltx  26608  ppiub  26634  chpeq0  26638  chteq0  26639  chtleppi  26640  chpchtsum  26649  chpub  26650  dchr1re  26693  bcmono  26707  efexple  26711  bposlem1  26714  bposlem4  26717  bposlem5  26718  bposlem7  26720  bposlem8  26721  bposlem9  26722  lgsval2lem  26737  lgsval4a  26749  lgsneg  26751  lgsdilem  26754  lgsdir2lem1  26755  2lgsoddprmlem3a  26840  2lgsoddprmlem3b  26841  2lgsoddprmlem3c  26842  2lgsoddprmlem3d  26843  rplogsumlem2  26915  rpvmasumlem  26917  dchrisum0flblem1  26938  dchrisum0flblem2  26939  dchrisum0fno1  26941  rplogsum  26957  logdivsum  26963  mulog2sumlem2  26965  selberg2lem  26980  logdivbnd  26986  pntrsumo1  26995  pntrlog2bndlem4  27010  pntrlog2bndlem5  27011  pntpbnd1  27016  pntpbnd2  27017  pntlem3  27039  pntleml  27041  ostth2  27067  trgcgrg  27631  ttgcontlem1  28007  axlowdimlem1  28065  axlowdimlem6  28070  axlowdimlem7  28071  axlowdimlem10  28074  axlowdim1  28082  axlowdim2  28083  axlowdim  28084  elntg2  28108  umgrislfupgrlem  28247  lfgrnloop  28250  lfuhgr1v0e  28376  usgrexmplef  28381  pthdlem2  28890  crctcshwlkn0lem7  28935  rusgrnumwwlks  29093  clwwlkn0  29146  konigsberg  29375  ex-po  29553  ex-sqrt  29572  ex-gcd  29575  nvz0  29784  0blo  29908  nmlno0lem  29909  nmblolbii  29915  siilem2  29968  minvecolem2  29991  minvecolem3  29992  minvecolem4c  29995  minvecolem4  29996  minvecolem5  29997  minvecolem7  29999  htthlem  30033  hiidge0  30214  normlem6  30231  normgt0  30243  norm-i  30245  normpyc  30262  bcsiALT  30295  pjhthlem1  30507  pjneli  30839  nmlnop0iALT  31111  unopbd  31131  nmbdoplbi  31140  nmcoplbi  31144  nmbdfnlbi  31165  nmbdfnlb  31166  nmcfnlbi  31168  cnlnadjlem7  31189  nmopcoi  31211  branmfn  31221  leopmul  31250  nmopleid  31255  pjbdlni  31265  pjnormssi  31284  stle0i  31355  cdj3lem1  31550  xaddeq0  31837  pr01ssre  31901  dp20u  31915  dp20h  31916  dp2clq  31918  dp2lt10  31921  dp2lt  31922  dp0u  31938  dplti  31942  dpexpp1  31945  xdiv0  31966  xrge0slmod  32325  unitdivcld  32710  sqsscirc1  32717  xrge0iifcnv  32742  xrge0iifiso  32744  rezh  32780  indf  32842  indfval  32843  esumcvgsum  32915  voliune  33056  volfiniune  33057  sibfinima  33167  sitmcl  33179  0rrv  33279  coinfliprv  33310  ballotlem2  33316  ballotlem4  33326  ballotlemi1  33330  ballotlemic  33334  sgnclre  33367  sgnnbi  33373  sgnpbi  33374  plymulx0  33387  signsply0  33391  signswch  33401  signstf  33406  signstf0  33408  signstfveq0  33417  signlem0  33427  signshf  33428  itgexpif  33447  hgt750lemd  33489  hgt750lem  33492  hgt750lem2  33493  hgt750leme  33499  iisconn  34072  iillysconn  34073  cvmliftlem10  34114  fz0n  34528  logi  34532  bcneg1  34534  nn0prpwlem  35009  dnizeq0  35153  dnizphlfeqhlf  35154  knoppndvlem13  35202  cnndvlem1  35215  bj-pinftyccb  35904  bj-minftyccb  35908  bj-pinftynminfty  35910  taupilemrplb  36003  irrdiff  36009  sin2h  36280  tan2h  36282  ptrecube  36290  poimirlem16  36306  poimirlem17  36307  poimirlem20  36310  poimirlem22  36312  poimirlem23  36313  poimirlem29  36319  poimirlem31  36321  poimir  36323  heicant  36325  mblfinlem2  36328  ismblfin  36331  ovoliunnfl  36332  voliunnfl  36334  volsupnfl  36335  mbfposadd  36337  itg2addnclem  36341  itg2addnclem2  36342  ibladdnclem  36346  itgaddnclem2  36349  iblabsnclem  36353  iblmulc2nc  36355  itgmulc2nclem2  36357  itgabsnc  36359  ftc1cnnclem  36361  ftc1anclem5  36367  ftc1anclem8  36370  asindmre  36373  dvasin  36374  areacirclem4  36381  areacirc  36383  isbnd3  36455  ssbnd  36459  prdsbnd  36464  bfplem2  36494  bfp  36495  renegclALT  37636  2xp3dxp2ge1d  40825  factwoffsmonot  40826  0cnALT3  40960  sn-1ne2  40965  oexpreposd  40991  sn-00idlem2  41052  sn-00idlem3  41053  sn-00id  41054  sn-0tie0  41092  sn-ltaddpos  41094  sn-ltaddneg  41095  relt0neg1  41097  sn-nnne0  41101  reelznn0nn  41102  sn-0lt1  41115  sn-inelr  41118  itrere  41119  retire  41120  pellexlem6  41341  elpell14qr2  41369  oddcomabszz  41452  zindbi  41454  jm2.24  41471  acongeq  41491  arearect  41733  areaquad  41734  reabsifneg  42152  reabsifnpos  42153  reabsifpos  42154  reabsifnneg  42155  imsqrtvalex  42166  relexp01min  42233  imo72b2lem0  42686  imo72b2lem2  42688  imo72b2lem1  42690  imo72b2  42693  dvconstbi  42862  binomcxplemnn0  42877  binomcxplemdvbinom  42881  binomcxplemcvg  42882  binomcxplemnotnn0  42884  sineq0ALT  43467  halffl  43777  ren0  43883  rexanuz2nf  43974  sqrlearg  44037  limsup10ex  44260  dvnmptdivc  44425  dvnmul  44430  itgsin0pilem1  44437  itgsinexplem1  44441  itgsinexp  44442  iblempty  44452  stoweidlem17  44504  stoweidlem36  44523  stoweidlem55  44542  wallispilem1  44552  wallispilem2  44553  wallispilem4  44555  stirlinglem4  44564  stirlinglem13  44573  stirlinglem14  44574  stirlinglem15  44575  stirlingr  44577  dirker2re  44579  dirkerdenne0  44580  dirkerre  44582  dirkertrigeqlem1  44585  dirkercncflem2  44591  dirkercncflem4  44593  fourierdlem11  44605  fourierdlem16  44610  fourierdlem21  44615  fourierdlem22  44616  fourierdlem41  44635  fourierdlem42  44636  fourierdlem48  44641  fourierdlem62  44655  fourierdlem66  44659  fourierdlem79  44672  fourierdlem83  44676  fourierdlem94  44687  fourierdlem102  44695  fourierdlem103  44696  fourierdlem104  44697  fourierdlem111  44704  fourierdlem112  44705  fourierdlem113  44706  fourierdlem114  44707  sqwvfoura  44715  sqwvfourb  44716  fourierswlem  44717  fouriersw  44718  etransclem23  44744  etransclem44  44765  etransclem46  44767  salexct3  44829  salgensscntex  44831  sge0rnn0  44855  sge00  44863  0ome  45016  ovn0lem  45052  ovnhoilem1  45088  smfmullem1  45278  smfmullem2  45279  smfmullem3  45280  smfmullem4  45281  zm1nn  45780  sqrtnegnre  45785  m1mod0mod1  45807  fmtnoprmfac2lem1  46004  31prm  46035  mod42tp1mod8  46040  nfermltl2rev  46181  tgblthelfgott  46253  altgsumbcALT  46675  expnegico01  46845  dignnld  46935  eenglngeehlnmlem1  47069  line2ylem  47083  line2y  47087  itsclc0yqsollem2  47095  icccldii  47197  i0oii  47198  sepfsepc  47206  ex-gt  47419