Theorem 0re 10986

Description: The number 0 is real. Remark: the first step could also be ax-icn 10939. See also 0reALT 11327. (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 10938	. 2 ⊢ 1 ∈ ℂ
2		cnre 10981	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 10951	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 10963	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2827	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 244	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3214	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 481	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3211	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 396   = wceq 1539   ∈ wcel 2107  ∃wrex 3066  (class class class)co 7284  ℂcc 10878  ℝcr 10879  0cc0 10880  1c1 10881  ici 10882   + caddc 10883   · cmul 10885

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 2710  ax-1cn 10938  ax-addrcl 10941  ax-rnegex 10951  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071

This theorem is referenced by:  0red  10987  0xr  11031  axmulgt0  11058  ne0gt0  11089  00id  11159  mul02lem1  11160  mul02lem2  11161  mul02  11162  addid1  11164  ltaddneg  11199  addgt0  11470  addgegt0  11471  addgtge0  11472  addge0  11473  ltaddpos  11474  ltneg  11484  leneg  11487  lt0neg1  11490  lt0neg2  11491  le0neg1  11492  le0neg2  11493  addge01  11494  suble0  11498  mulge0  11502  msqge0  11505  0le1  11507  relin01  11508  gt0ne0i  11519  gt0ne0d  11548  lt0ne0d  11549  elimge0  11823  ltm1  11826  recgt0  11830  prodgt0  11831  lemul1a  11838  ltmul12a  11840  lemul12a  11842  mulgt1  11843  gt0div  11850  ge0div  11851  mulge0b  11854  lediv12a  11877  recgt1i  11881  recreclt  11883  ledivp1  11886  squeeze0  11887  recgt0ii  11890  ledivp1i  11909  ltdivp1i  11910  fimaxre2  11929  inelr  11972  crne0  11975  nnge1  12010  nngt0  12013  nnnle0  12015  nnne0  12016  nnrecgt0  12025  0le0  12083  neg1lt0  12099  halfge0  12199  nn0ssre  12246  nn0ge0  12267  nn0nlt0  12268  nn0le0eq0  12270  0mnnnnn0  12274  elnnnn0b  12286  elnnnn0c  12287  nn0sub  12292  elnnz  12338  0z  12339  elnn0z  12341  elnnz1  12355  recnz  12404  gtndiv  12406  fnn0ind  12428  10re  12465  rpge0  12752  rpneg  12771  0nrp  12774  0ltpnf  12867  mnflt0  12870  qsqueeze  12944  xneg0  12955  xaddid1  12984  xnn0xadd0  12990  xmulpnf1  13017  xlemul1a  13031  xadddi  13038  xrsupsslem  13050  xrinfmsslem  13051  elrege0  13195  0e0icopnf  13199  elicc01  13207  0elunit  13210  unitssre  13240  0nelfz1  13284  fzpreddisj  13314  fz0to4untppr  13368  nn0p1elfzo  13439  ico01fl0  13548  rpsup  13595  modelico  13610  0mod  13631  1mod  13632  le2sq2  13863  expubnd  13904  sqlecan  13934  bernneq2  13954  expnbnd  13956  expnlbnd  13957  expmulnbnd  13959  discr1  13963  discr  13964  faclbnd  14013  faclbnd3  14015  faclbnd6  14022  bcval4  14030  bcval5  14041  bcpasc  14044  hasheq0  14087  hashneq0  14088  hashnn0n0nn  14115  hashgt12el  14146  hashgt12el2  14147  hashge2el2dif  14203  lsw0  14277  swrdccatin2  14451  pfxccatin12lem3  14454  reim0  14838  re0  14872  im0  14873  rei  14876  imi  14877  cj0  14878  sqeqd  14886  rennim  14959  cnpart  14960  sqr0lem  14961  sqrlem4  14966  resqrex  14971  sqrtgt0  14979  sqrt00  14984  sqrtneglem  14987  sqrt9  14994  sqrt2gt1lt2  14995  leabs  15020  absor  15021  max0add  15031  eqsqrt2d  15089  sqrtpclii  15103  rlimconst  15262  rlimrege0  15297  lo1mul  15346  iserge0  15381  fsum00  15519  isumless  15566  arisum2  15582  georeclim  15593  geo2sum  15594  geoisumr  15599  0.999...  15602  cvgrat  15604  fprodge0  15712  bpoly4  15778  cos0  15868  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  cos2bnd  15906  sin01gt0  15908  cos01gt0  15909  sincos2sgn  15912  sin4lt0  15913  absef  15915  absefib  15916  efieq1re  15917  epos  15925  rpnnen2lem2  15933  rpnnen2lem3  15934  rpnnen2lem4  15935  rpnnen2lem9  15940  ruclem6  15953  dvdslelem  16027  divalglem1  16112  divalglem5  16115  divalglem6  16116  flodddiv4  16131  sadcadd  16174  gcdn0gt0  16234  nn0seqcvgd  16284  algcvgblem  16291  algcvga  16293  pythagtriplem12  16536  pythagtriplem13  16537  pythagtriplem14  16538  pythagtriplem16  16540  prmreclem4  16629  prmreclem5  16630  prmreclem6  16631  1arith  16637  ramz  16735  mulgnegnn  18723  subgmulg  18778  srgbinomlem4  19788  isabvd  20089  abvtrivd  20109  xrs1mnd  20645  xrs10  20646  rge0srg  20678  psgnodpmr  20804  re0g  20826  psrbaglesupp  21136  psrbaglesuppOLD  21137  mnfnei  22381  imasdsf1olem  23535  ssblps  23584  ssbl  23585  xmeter  23595  dscmet  23737  dscopn  23738  nmoi  23901  nmoeq0  23909  0nghm  23914  idnghm  23916  cnbl0  23946  xrsxmet  23981  metdseq0  24026  iicmp  24058  iiconn  24059  iihalf1  24103  iihalf1cn  24104  elii1  24107  icopnfcnv  24114  icopnfhmeo  24115  iccpnfcnv  24116  xrhmeo  24118  xrhmph  24119  htpycc  24152  reparphti  24169  pcoval1  24185  pco0  24186  pcoval2  24188  pcocn  24189  pcohtpylem  24191  pcopt  24194  pcopt2  24195  pcoass  24196  pcorevlem  24198  reust  24554  recusp  24555  rrx0el  24571  minveclem4c  24598  minveclem2  24599  minveclem3b  24601  minveclem4  24605  minveclem7  24608  pjthlem1  24610  cniccbdd  24634  ovolunnul  24673  ovoliunnul  24680  ovolicc1  24689  ovolre  24698  iccvolcl  24740  ovolioo  24741  ioovolcl  24743  ioorcl  24750  vitalilem4  24784  vitalilem5  24785  vitali  24786  ismbf  24801  mbfmulc2lem  24820  mbfpos  24824  mbfposr  24825  i1f0  24860  i1f1  24863  itg1addlem2  24870  itg1addlem4  24872  itg1addlem4OLD  24873  itg1addlem5  24874  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfi1flimlem  24896  xrge0f  24905  itg2ge0  24909  itg2const  24914  itg2mulc  24921  itg2splitlem  24922  itg2gt0  24934  itg2cnlem1  24935  ibl0  24960  iblrelem  24964  iblposlem  24965  iblpos  24966  iblre  24967  itgreval  24970  itgneg  24977  iblss  24978  i1fibl  24981  itgitg1  24982  itgle  24983  itgeqa  24987  itgless  24990  iblconst  24991  itgconst  24992  ibladdlem  24993  itgaddlem2  24997  iblabslem  25001  iblabsr  25003  iblmulc2  25004  itgmulc2lem2  25006  itgabs  25008  itgsplit  25009  bddmulibl  25012  dvferm1  25158  dvferm2  25160  dvferm  25161  dvlip  25166  c1lip1  25170  dveq0  25173  dv11cn  25174  dvne0  25184  ftc1lem4  25212  ply1divex  25310  dgrco  25445  plyrecj  25449  vieta1lem2  25480  aalioulem2  25502  aalioulem3  25503  pserulm  25590  psercnlem2  25592  psercnlem1  25593  psercn  25594  abelth  25609  reeff1olem  25614  reeff1o  25615  pilem2  25620  pilem3  25621  pipos  25626  sinhalfpilem  25629  sincosq1sgn  25664  sincosq2sgn  25665  coseq00topi  25668  coseq0negpitopi  25669  tangtx  25671  tanabsge  25672  sinq12ge0  25674  sinq34lt0t  25675  cosq14ge0  25677  sincos4thpi  25679  sincos6thpi  25681  pige3ALT  25685  sineq0  25689  cosordlem  25695  cosord  25696  cos0pilt1  25697  cos11  25698  sinord  25699  recosf1o  25700  resinf1o  25701  tanord1  25702  tanord  25703  tanregt0  25704  efif1olem4  25710  efifo  25712  relogrn  25726  log1  25750  logneg  25752  argregt0  25774  argrege0  25775  argimgt0  25776  logneg2  25779  logdivlti  25784  logdivlt  25785  ellogdm  25803  logdmn0  25804  logdmnrp  25805  logcnlem3  25808  dvloglem  25812  logdmopn  25813  logf1o2  25814  dvlog2lem  25816  efopnlem1  25820  logtayl  25824  recxpcl  25839  cxpge0  25847  cxple2  25861  cxple2a  25863  cxpsqrtlem  25866  cxpcn3  25910  cxpaddlelem  25913  cxpaddle  25914  loglesqrt  25920  logbrec  25941  ang180lem3  25970  ang180lem4  25971  asinneg  26045  asin1  26053  reasinsin  26055  acosbnd  26059  atan0  26067  atanrecl  26070  atanlogaddlem  26072  atanlogsublem  26074  atanlogsub  26075  atantan  26082  atanbnd  26085  atan1  26087  atans2  26090  ressatans  26093  log2cnv  26103  log2tlbnd  26104  log2ub  26108  log2le1  26109  rlimcnp  26124  rlimcnp2  26125  o1cxp  26133  jensen  26147  amgm  26149  emgt0  26165  harmonicbnd3  26166  harmoniclbnd  26167  harmonicbnd4  26169  zetacvg  26173  eldmgm  26180  lgamgulmlem2  26188  basellem3  26241  basellem8  26246  efnnfsumcl  26261  ppisval  26262  vmage0  26279  chpge0  26284  efchtdvds  26317  ppiltx  26335  ppiub  26361  chpeq0  26365  chteq0  26366  chtleppi  26367  chpchtsum  26376  chpub  26377  dchr1re  26420  bcmono  26434  efexple  26438  bposlem1  26441  bposlem4  26444  bposlem5  26445  bposlem7  26447  bposlem8  26448  bposlem9  26449  lgsval2lem  26464  lgsval4a  26476  lgsneg  26478  lgsdilem  26481  lgsdir2lem1  26482  2lgsoddprmlem3a  26567  2lgsoddprmlem3b  26568  2lgsoddprmlem3c  26569  2lgsoddprmlem3d  26570  rplogsumlem2  26642  rpvmasumlem  26644  dchrisum0flblem1  26665  dchrisum0flblem2  26666  dchrisum0fno1  26668  rplogsum  26684  logdivsum  26690  mulog2sumlem2  26692  selberg2lem  26707  logdivbnd  26713  pntrsumo1  26722  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntpbnd1  26743  pntpbnd2  26744  pntlem3  26766  pntleml  26768  ostth2  26794  trgcgrg  26885  ttgcontlem1  27261  axlowdimlem1  27319  axlowdimlem6  27324  axlowdimlem7  27325  axlowdimlem10  27328  axlowdim1  27336  axlowdim2  27337  axlowdim  27338  elntg2  27362  umgrislfupgrlem  27501  lfgrnloop  27504  lfuhgr1v0e  27630  usgrexmplef  27635  pthdlem2  28145  crctcshwlkn0lem7  28190  rusgrnumwwlks  28348  clwwlkn0  28401  konigsberg  28630  ex-po  28808  ex-sqrt  28827  ex-gcd  28830  nvz0  29039  0blo  29163  nmlno0lem  29164  nmblolbii  29170  siilem2  29223  minvecolem2  29246  minvecolem3  29247  minvecolem4c  29250  minvecolem4  29251  minvecolem5  29252  minvecolem7  29254  htthlem  29288  hiidge0  29469  normlem6  29486  normgt0  29498  norm-i  29500  normpyc  29517  bcsiALT  29550  pjhthlem1  29762  pjneli  30094  nmlnop0iALT  30366  unopbd  30386  nmbdoplbi  30395  nmcoplbi  30399  nmbdfnlbi  30420  nmbdfnlb  30421  nmcfnlbi  30423  cnlnadjlem7  30444  nmopcoi  30466  branmfn  30476  leopmul  30505  nmopleid  30510  pjbdlni  30520  pjnormssi  30539  stle0i  30610  cdj3lem1  30805  xaddeq0  31085  pr01ssre  31147  dp20u  31161  dp20h  31162  dp2clq  31164  dp2lt10  31167  dp2lt  31168  dp0u  31184  dplti  31188  dpexpp1  31191  xdiv0  31212  xrge0slmod  31557  unitdivcld  31860  sqsscirc1  31867  xrge0iifcnv  31892  xrge0iifiso  31894  rezh  31930  indf  31992  indfval  31993  esumcvgsum  32065  voliune  32206  volfiniune  32207  sibfinima  32315  sitmcl  32327  0rrv  32427  coinfliprv  32458  ballotlem2  32464  ballotlem4  32474  ballotlemi1  32478  ballotlemic  32482  sgnclre  32515  sgnnbi  32521  sgnpbi  32522  plymulx0  32535  signsply0  32539  signswch  32549  signstf  32554  signstf0  32556  signstfveq0  32565  signlem0  32575  signshf  32576  itgexpif  32595  hgt750lemd  32637  hgt750lem  32640  hgt750lem2  32641  hgt750leme  32647  iisconn  33223  iillysconn  33224  cvmliftlem10  33265  fz0n  33705  logi  33709  bcneg1  33711  nn0prpwlem  34520  dnizeq0  34664  dnizphlfeqhlf  34665  knoppndvlem13  34713  cnndvlem1  34726  bj-pinftyccb  35401  bj-minftyccb  35405  bj-pinftynminfty  35407  taupilemrplb  35500  irrdiff  35506  sin2h  35776  tan2h  35778  ptrecube  35786  poimirlem16  35802  poimirlem17  35803  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem29  35815  poimirlem31  35817  poimir  35819  heicant  35821  mblfinlem2  35824  ismblfin  35827  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  mbfposadd  35833  itg2addnclem  35837  itg2addnclem2  35838  ibladdnclem  35842  itgaddnclem2  35845  iblabsnclem  35849  iblmulc2nc  35851  itgmulc2nclem2  35853  itgabsnc  35855  ftc1cnnclem  35857  ftc1anclem5  35863  ftc1anclem8  35866  asindmre  35869  dvasin  35870  areacirclem4  35877  areacirc  35879  isbnd3  35951  ssbnd  35955  prdsbnd  35960  bfplem2  35990  bfp  35991  renegclALT  36984  2xp3dxp2ge1d  40169  factwoffsmonot  40170  0cnALT3  40297  sn-1ne2  40302  oexpreposd  40328  sn-00idlem2  40389  sn-00idlem3  40390  sn-00id  40391  rei4  40412  sn-0tie0  40428  sn-ltaddpos  40430  relt0neg1  40432  sn-0lt1  40439  sn-inelr  40442  itrere  40443  retire  40444  pellexlem6  40663  elpell14qr2  40691  oddcomabszz  40773  zindbi  40775  jm2.24  40792  acongeq  40812  arearect  41053  areaquad  41054  reabsifneg  41247  reabsifnpos  41248  reabsifpos  41249  reabsifnneg  41250  imsqrtvalex  41261  relexp01min  41328  imo72b2lem0  41783  imo72b2lem2  41785  imo72b2lem1  41787  imo72b2  41790  dvconstbi  41959  binomcxplemnn0  41974  binomcxplemdvbinom  41978  binomcxplemcvg  41979  binomcxplemnotnn0  41981  sineq0ALT  42564  halffl  42842  ren0  42949  sqrlearg  43098  limsup10ex  43321  dvnmptdivc  43486  dvnmul  43491  itgsin0pilem1  43498  itgsinexplem1  43502  itgsinexp  43503  iblempty  43513  stoweidlem17  43565  stoweidlem36  43584  stoweidlem55  43603  wallispilem1  43613  wallispilem2  43614  wallispilem4  43616  stirlinglem4  43625  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  stirlingr  43638  dirker2re  43640  dirkerdenne0  43641  dirkerre  43643  dirkertrigeqlem1  43646  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem11  43666  fourierdlem16  43671  fourierdlem21  43676  fourierdlem22  43677  fourierdlem41  43696  fourierdlem42  43697  fourierdlem48  43702  fourierdlem62  43716  fourierdlem66  43720  fourierdlem79  43733  fourierdlem83  43737  fourierdlem94  43748  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fourierdlem114  43768  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  etransclem23  43805  etransclem44  43826  etransclem46  43828  salexct3  43888  salgensscntex  43890  sge0rnn0  43913  sge00  43921  0ome  44074  ovn0lem  44110  ovnhoilem1  44146  smfmullem1  44336  smfmullem2  44337  smfmullem3  44338  smfmullem4  44339  zm1nn  44805  sqrtnegnre  44810  m1mod0mod1  44832  fmtnoprmfac2lem1  45029  31prm  45060  mod42tp1mod8  45065  nfermltl2rev  45206  tgblthelfgott  45278  altgsumbcALT  45700  expnegico01  45870  dignnld  45960  eenglngeehlnmlem1  46094  line2ylem  46108  line2y  46112  itsclc0yqsollem2  46120  icccldii  46223  i0oii  46224  sepfsepc  46232  ex-gt  46441