Theorem 0re 11216

Description: The number 0 is real. Remark: the first step could also be ax-icn 11169. See also 0reALT 11557. (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 11168	. 2 ⊢ 1 ∈ ℂ
2		cnre 11211	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11181	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11193	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2822	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 244	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3156	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 482	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3148	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃wrex 3071  (class class class)co 7409  ℂcc 11108  ℝcr 11109  0cc0 11110  1c1 11111  ici 11112   + caddc 11113   · cmul 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-addrcl 11171  ax-rnegex 11181  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-rex 3072

This theorem is referenced by:  0red  11217  0xr  11261  axmulgt0  11288  ne0gt0  11319  00id  11389  mul02lem1  11390  mul02lem2  11391  mul02  11392  addrid  11394  ltaddneg  11429  addgt0  11700  addgegt0  11701  addgtge0  11702  addge0  11703  ltaddpos  11704  ltneg  11714  leneg  11717  lt0neg1  11720  lt0neg2  11721  le0neg1  11722  le0neg2  11723  addge01  11724  suble0  11728  mulge0  11732  msqge0  11735  0le1  11737  relin01  11738  gt0ne0i  11749  gt0ne0d  11778  lt0ne0d  11779  elimge0  12053  ltm1  12056  recgt0  12060  prodgt0  12061  lemul1a  12068  ltmul12a  12070  lemul12a  12072  mulgt1  12073  gt0div  12080  ge0div  12081  mulge0b  12084  lediv12a  12107  recgt1i  12111  recreclt  12113  ledivp1  12116  squeeze0  12117  recgt0ii  12120  ledivp1i  12139  ltdivp1i  12140  fimaxre2  12159  inelr  12202  crne0  12205  nnge1  12240  nngt0  12243  nnnle0  12245  nnne0  12246  nnrecgt0  12255  0le0  12313  neg1lt0  12329  halfge0  12429  nn0ssre  12476  nn0ge0  12497  nn0nlt0  12498  nn0le0eq0  12500  0mnnnnn0  12504  elnnnn0b  12516  elnnnn0c  12517  nn0sub  12522  elnnz  12568  0z  12569  elnn0z  12571  elnnz1  12588  recnz  12637  gtndiv  12639  fnn0ind  12661  10re  12696  rpge0  12987  rpneg  13006  0nrp  13009  0ltpnf  13102  mnflt0  13105  qsqueeze  13180  xneg0  13191  xaddrid  13220  xnn0xadd0  13226  xmulpnf1  13253  xlemul1a  13267  xadddi  13274  xrsupsslem  13286  xrinfmsslem  13287  elrege0  13431  0e0icopnf  13435  elicc01  13443  0elunit  13446  unitssre  13476  0nelfz1  13520  fzpreddisj  13550  fz0to4untppr  13604  nn0p1elfzo  13675  ico01fl0  13784  rpsup  13831  modelico  13846  0mod  13867  1mod  13868  le2sq2  14100  expubnd  14142  sqlecan  14173  bernneq2  14193  expnbnd  14195  expnlbnd  14196  expmulnbnd  14198  discr1  14202  discr  14203  faclbnd  14250  faclbnd3  14252  faclbnd6  14259  bcval4  14267  bcval5  14278  bcpasc  14281  hasheq0  14323  hashneq0  14324  hashnn0n0nn  14351  hashgt12el  14382  hashgt12el2  14383  hashge2el2dif  14441  lsw0  14515  swrdccatin2  14679  pfxccatin12lem3  14682  reim0  15065  re0  15099  im0  15100  rei  15103  imi  15104  cj0  15105  sqeqd  15113  rennim  15186  cnpart  15187  sqrt0  15188  01sqrexlem4  15192  resqrex  15197  sqrtgt0  15205  sqrt00  15210  sqrtneglem  15213  sqrt9  15220  sqrt2gt1lt2  15221  leabs  15246  absor  15247  max0add  15257  eqsqrt2d  15315  sqrtpclii  15329  rlimconst  15488  rlimrege0  15523  lo1mul  15572  iserge0  15607  fsum00  15744  isumless  15791  arisum2  15807  georeclim  15818  geo2sum  15819  geoisumr  15824  0.999...  15827  cvgrat  15829  fprodge0  15937  bpoly4  16003  cos0  16093  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  cos2bnd  16131  sin01gt0  16133  cos01gt0  16134  sincos2sgn  16137  sin4lt0  16138  absef  16140  absefib  16141  efieq1re  16142  epos  16150  rpnnen2lem2  16158  rpnnen2lem3  16159  rpnnen2lem4  16160  rpnnen2lem9  16165  ruclem6  16178  dvdslelem  16252  divalglem1  16337  divalglem5  16340  divalglem6  16341  flodddiv4  16356  sadcadd  16399  gcdn0gt0  16459  nn0seqcvgd  16507  algcvgblem  16514  algcvga  16516  pythagtriplem12  16759  pythagtriplem13  16760  pythagtriplem14  16761  pythagtriplem16  16763  prmreclem4  16852  prmreclem5  16853  prmreclem6  16854  1arith  16860  ramz  16958  mulgnegnn  18964  subgmulg  19020  srgbinomlem4  20052  isabvd  20428  abvtrivd  20448  xrs1mnd  20983  xrs10  20984  rge0srg  21016  psgnodpmr  21143  re0g  21165  psrbaglesupp  21477  psrbaglesuppOLD  21478  mnfnei  22725  imasdsf1olem  23879  ssblps  23928  ssbl  23929  xmeter  23939  dscmet  24081  dscopn  24082  nmoi  24245  nmoeq0  24253  0nghm  24258  idnghm  24260  cnbl0  24290  xrsxmet  24325  metdseq0  24370  iicmp  24402  iiconn  24403  iihalf1  24447  iihalf1cn  24448  elii1  24451  icopnfcnv  24458  icopnfhmeo  24459  iccpnfcnv  24460  xrhmeo  24462  xrhmph  24463  htpycc  24496  reparphti  24513  pcoval1  24529  pco0  24530  pcoval2  24532  pcocn  24533  pcohtpylem  24535  pcopt  24538  pcopt2  24539  pcoass  24540  pcorevlem  24542  reust  24898  recusp  24899  rrx0el  24915  minveclem4c  24942  minveclem2  24943  minveclem3b  24945  minveclem4  24949  minveclem7  24952  pjthlem1  24954  cniccbdd  24978  ovolunnul  25017  ovoliunnul  25024  ovolicc1  25033  ovolre  25042  iccvolcl  25084  ovolioo  25085  ioovolcl  25087  ioorcl  25094  vitalilem4  25128  vitalilem5  25129  vitali  25130  ismbf  25145  mbfmulc2lem  25164  mbfpos  25168  mbfposr  25169  i1f0  25204  i1f1  25207  itg1addlem2  25214  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1flimlem  25240  xrge0f  25249  itg2ge0  25253  itg2const  25258  itg2mulc  25265  itg2splitlem  25266  itg2gt0  25278  itg2cnlem1  25279  ibl0  25304  iblrelem  25308  iblposlem  25309  iblpos  25310  iblre  25311  itgreval  25314  itgneg  25321  iblss  25322  i1fibl  25325  itgitg1  25326  itgle  25327  itgeqa  25331  itgless  25334  iblconst  25335  itgconst  25336  ibladdlem  25337  itgaddlem2  25341  iblabslem  25345  iblabsr  25347  iblmulc2  25348  itgmulc2lem2  25350  itgabs  25352  itgsplit  25353  bddmulibl  25356  dvferm1  25502  dvferm2  25504  dvferm  25505  dvlip  25510  c1lip1  25514  dveq0  25517  dv11cn  25518  dvne0  25528  ftc1lem4  25556  ply1divex  25654  dgrco  25789  plyrecj  25793  vieta1lem2  25824  aalioulem2  25846  aalioulem3  25847  pserulm  25934  psercnlem2  25936  psercnlem1  25937  psercn  25938  abelth  25953  reeff1olem  25958  reeff1o  25959  pilem2  25964  pilem3  25965  pipos  25970  sinhalfpilem  25973  sincosq1sgn  26008  sincosq2sgn  26009  coseq00topi  26012  coseq0negpitopi  26013  tangtx  26015  tanabsge  26016  sinq12ge0  26018  sinq34lt0t  26019  cosq14ge0  26021  sincos4thpi  26023  sincos6thpi  26025  pige3ALT  26029  sineq0  26033  cosordlem  26039  cosord  26040  cos0pilt1  26041  cos11  26042  sinord  26043  recosf1o  26044  resinf1o  26045  tanord1  26046  tanord  26047  tanregt0  26048  efif1olem4  26054  efifo  26056  relogrn  26070  log1  26094  logneg  26096  argregt0  26118  argrege0  26119  argimgt0  26120  logneg2  26123  logdivlti  26128  logdivlt  26129  ellogdm  26147  logdmn0  26148  logdmnrp  26149  logcnlem3  26152  dvloglem  26156  logdmopn  26157  logf1o2  26158  dvlog2lem  26160  efopnlem1  26164  logtayl  26168  recxpcl  26183  cxpge0  26191  cxple2  26205  cxple2a  26207  cxpsqrtlem  26210  cxpcn3  26256  cxpaddlelem  26259  cxpaddle  26260  loglesqrt  26266  logbrec  26287  ang180lem3  26316  ang180lem4  26317  asinneg  26391  asin1  26399  reasinsin  26401  acosbnd  26405  atan0  26413  atanrecl  26416  atanlogaddlem  26418  atanlogsublem  26420  atanlogsub  26421  atantan  26428  atanbnd  26431  atan1  26433  atans2  26436  ressatans  26439  log2cnv  26449  log2tlbnd  26450  log2ub  26454  log2le1  26455  rlimcnp  26470  rlimcnp2  26471  o1cxp  26479  jensen  26493  amgm  26495  emgt0  26511  harmonicbnd3  26512  harmoniclbnd  26513  harmonicbnd4  26515  zetacvg  26519  eldmgm  26526  lgamgulmlem2  26534  basellem3  26587  basellem8  26592  efnnfsumcl  26607  ppisval  26608  vmage0  26625  chpge0  26630  efchtdvds  26663  ppiltx  26681  ppiub  26707  chpeq0  26711  chteq0  26712  chtleppi  26713  chpchtsum  26722  chpub  26723  dchr1re  26766  bcmono  26780  efexple  26784  bposlem1  26787  bposlem4  26790  bposlem5  26791  bposlem7  26793  bposlem8  26794  bposlem9  26795  lgsval2lem  26810  lgsval4a  26822  lgsneg  26824  lgsdilem  26827  lgsdir2lem1  26828  2lgsoddprmlem3a  26913  2lgsoddprmlem3b  26914  2lgsoddprmlem3c  26915  2lgsoddprmlem3d  26916  rplogsumlem2  26988  rpvmasumlem  26990  dchrisum0flblem1  27011  dchrisum0flblem2  27012  dchrisum0fno1  27014  rplogsum  27030  logdivsum  27036  mulog2sumlem2  27038  selberg2lem  27053  logdivbnd  27059  pntrsumo1  27068  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntpbnd1  27089  pntpbnd2  27090  pntlem3  27112  pntleml  27114  ostth2  27140  trgcgrg  27766  ttgcontlem1  28142  axlowdimlem1  28200  axlowdimlem6  28205  axlowdimlem7  28206  axlowdimlem10  28209  axlowdim1  28217  axlowdim2  28218  axlowdim  28219  elntg2  28243  umgrislfupgrlem  28382  lfgrnloop  28385  lfuhgr1v0e  28511  usgrexmplef  28516  pthdlem2  29025  crctcshwlkn0lem7  29070  rusgrnumwwlks  29228  clwwlkn0  29281  konigsberg  29510  ex-po  29688  ex-sqrt  29707  ex-gcd  29710  nvz0  29921  0blo  30045  nmlno0lem  30046  nmblolbii  30052  siilem2  30105  minvecolem2  30128  minvecolem3  30129  minvecolem4c  30132  minvecolem4  30133  minvecolem5  30134  minvecolem7  30136  htthlem  30170  hiidge0  30351  normlem6  30368  normgt0  30380  norm-i  30382  normpyc  30399  bcsiALT  30432  pjhthlem1  30644  pjneli  30976  nmlnop0iALT  31248  unopbd  31268  nmbdoplbi  31277  nmcoplbi  31281  nmbdfnlbi  31302  nmbdfnlb  31303  nmcfnlbi  31305  cnlnadjlem7  31326  nmopcoi  31348  branmfn  31358  leopmul  31387  nmopleid  31392  pjbdlni  31402  pjnormssi  31421  stle0i  31492  cdj3lem1  31687  xaddeq0  31966  pr01ssre  32030  dp20u  32044  dp20h  32045  dp2clq  32047  dp2lt10  32050  dp2lt  32051  dp0u  32067  dplti  32071  dpexpp1  32074  xdiv0  32095  xrge0slmod  32463  unitdivcld  32881  sqsscirc1  32888  xrge0iifcnv  32913  xrge0iifiso  32915  rezh  32951  indf  33013  indfval  33014  esumcvgsum  33086  voliune  33227  volfiniune  33228  sibfinima  33338  sitmcl  33350  0rrv  33450  coinfliprv  33481  ballotlem2  33487  ballotlem4  33497  ballotlemi1  33501  ballotlemic  33505  sgnclre  33538  sgnnbi  33544  sgnpbi  33545  plymulx0  33558  signsply0  33562  signswch  33572  signstf  33577  signstf0  33579  signstfveq0  33588  signlem0  33598  signshf  33599  itgexpif  33618  hgt750lemd  33660  hgt750lem  33663  hgt750lem2  33664  hgt750leme  33670  iisconn  34243  iillysconn  34244  cvmliftlem10  34285  fz0n  34700  logi  34704  bcneg1  34706  gg-iihalf1cn  35167  gg-reparphti  35172  nn0prpwlem  35207  dnizeq0  35351  dnizphlfeqhlf  35352  knoppndvlem13  35400  cnndvlem1  35413  bj-pinftyccb  36102  bj-minftyccb  36106  bj-pinftynminfty  36108  taupilemrplb  36201  irrdiff  36207  sin2h  36478  tan2h  36480  ptrecube  36488  poimirlem16  36504  poimirlem17  36505  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimirlem29  36517  poimirlem31  36519  poimir  36521  heicant  36523  mblfinlem2  36526  ismblfin  36529  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  mbfposadd  36535  itg2addnclem  36539  itg2addnclem2  36540  ibladdnclem  36544  itgaddnclem2  36547  iblabsnclem  36551  iblmulc2nc  36553  itgmulc2nclem2  36555  itgabsnc  36557  ftc1cnnclem  36559  ftc1anclem5  36565  ftc1anclem8  36568  asindmre  36571  dvasin  36572  areacirclem4  36579  areacirc  36581  isbnd3  36652  ssbnd  36656  prdsbnd  36661  bfplem2  36691  bfp  36692  renegclALT  37833  2xp3dxp2ge1d  41022  factwoffsmonot  41023  0cnALT3  41174  sn-1ne2  41179  oexpreposd  41212  sn-00idlem2  41272  sn-00idlem3  41273  sn-00id  41274  sn-0tie0  41312  sn-ltaddpos  41314  sn-ltaddneg  41315  relt0neg1  41317  sn-nnne0  41321  reelznn0nn  41322  sn-0lt1  41335  sn-inelr  41338  itrere  41339  retire  41340  pellexlem6  41572  elpell14qr2  41600  oddcomabszz  41683  zindbi  41685  jm2.24  41702  acongeq  41722  arearect  41964  areaquad  41965  reabsifneg  42383  reabsifnpos  42384  reabsifpos  42385  reabsifnneg  42386  imsqrtvalex  42397  relexp01min  42464  imo72b2lem0  42917  imo72b2lem2  42919  imo72b2lem1  42921  imo72b2  42924  dvconstbi  43093  binomcxplemnn0  43108  binomcxplemdvbinom  43112  binomcxplemcvg  43113  binomcxplemnotnn0  43115  sineq0ALT  43698  halffl  44006  ren0  44112  rexanuz2nf  44203  sqrlearg  44266  limsup10ex  44489  dvnmptdivc  44654  dvnmul  44659  itgsin0pilem1  44666  itgsinexplem1  44670  itgsinexp  44671  iblempty  44681  stoweidlem17  44733  stoweidlem36  44752  stoweidlem55  44771  wallispilem1  44781  wallispilem2  44782  wallispilem4  44784  stirlinglem4  44793  stirlinglem13  44802  stirlinglem14  44803  stirlinglem15  44804  stirlingr  44806  dirker2re  44808  dirkerdenne0  44809  dirkerre  44811  dirkertrigeqlem1  44814  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem11  44834  fourierdlem16  44839  fourierdlem21  44844  fourierdlem22  44845  fourierdlem41  44864  fourierdlem42  44865  fourierdlem48  44870  fourierdlem62  44884  fourierdlem66  44888  fourierdlem79  44901  fourierdlem83  44905  fourierdlem94  44916  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  fourierdlem114  44936  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  etransclem23  44973  etransclem44  44994  etransclem46  44996  salexct3  45058  salgensscntex  45060  sge0rnn0  45084  sge00  45092  0ome  45245  ovn0lem  45281  ovnhoilem1  45317  smfmullem1  45507  smfmullem2  45508  smfmullem3  45509  smfmullem4  45510  zm1nn  46010  sqrtnegnre  46015  m1mod0mod1  46037  fmtnoprmfac2lem1  46234  31prm  46265  mod42tp1mod8  46270  nfermltl2rev  46411  tgblthelfgott  46483  altgsumbcALT  47029  expnegico01  47199  dignnld  47289  eenglngeehlnmlem1  47423  line2ylem  47437  line2y  47441  itsclc0yqsollem2  47449  icccldii  47551  i0oii  47552  sepfsepc  47560  ex-gt  47773