Theorem 0re 11152

Description: The number 0 is real. Remark: the first step could also be ax-icn 11103. See also 0reALT 11495. (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 11102	. 2 ⊢ 1 ∈ ℂ
2		cnre 11147	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11115	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11127	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2816	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3134	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3126	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  (class class class)co 7369  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045  ici 11046   + caddc 11047   · cmul 11049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11102  ax-addrcl 11105  ax-rnegex 11115  ax-cnre 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-rex 3054

This theorem is referenced by:  0red  11153  0xr  11197  axmulgt0  11224  ne0gt0  11255  00id  11325  mul02lem1  11326  mul02lem2  11327  mul02  11328  addrid  11330  ltaddneg  11366  addgt0  11640  addgegt0  11641  addgtge0  11642  addge0  11643  ltaddpos  11644  ltneg  11654  leneg  11657  lt0neg1  11660  lt0neg2  11661  le0neg1  11662  le0neg2  11663  addge01  11664  suble0  11668  mulge0  11672  msqge0  11675  0le1  11677  relin01  11678  gt0ne0i  11689  lt0ne0d  11719  elimge0  11997  ltm1  12000  recgt0  12004  prodgt0  12005  lemul1a  12012  ltmul12a  12014  lemul12a  12016  mulgt1OLD  12017  gt0div  12025  ge0div  12026  mulge0b  12029  lediv12a  12052  recgt1i  12056  recreclt  12058  ledivp1  12061  squeeze0  12062  recgt0ii  12065  ledivp1i  12084  ltdivp1i  12085  fimaxre2  12104  inelr  12152  crne0  12155  nnge1  12190  nngt0  12193  nnnle0  12195  nnne0  12196  nnrecgt0  12205  0le0  12263  halfge0  12374  nn0ssre  12422  nn0ge0  12443  nn0nlt0  12444  nn0le0eq0  12446  0mnnnnn0  12450  elnnnn0b  12462  elnnnn0c  12463  nn0sub  12468  elnnz  12515  0z  12516  elnn0z  12518  elnnz1  12535  recnz  12585  gtndiv  12587  fnn0ind  12609  10re  12644  rpge0  12941  rpneg  12961  0nrp  12964  0ltpnf  13058  mnflt0  13061  qsqueeze  13137  xneg0  13148  xaddrid  13177  xnn0xadd0  13183  xmulpnf1  13210  xlemul1a  13224  xadddi  13231  xrsupsslem  13243  xrinfmsslem  13244  elrege0  13391  0e0icopnf  13395  elicc01  13403  0elunit  13406  unitssre  13436  0nelfz1  13480  fzpreddisj  13510  fz0to4untppr  13567  fz0to5un2tp  13568  nn0p1elfzo  13639  ico01fl0  13757  rpsup  13804  modelico  13819  0mod  13840  1mod  13841  le2sq2  14076  expubnd  14119  sqlecan  14150  bernneq2  14171  expnbnd  14173  expnlbnd  14174  expmulnbnd  14176  discr1  14180  discr  14181  faclbnd  14231  faclbnd3  14233  faclbnd6  14240  bcval4  14248  bcval5  14259  bcpasc  14262  hasheq0  14304  hashneq0  14305  hashnn0n0nn  14332  hashgt12el  14363  hashgt12el2  14364  hashge2el2dif  14421  lsw0  14506  swrdccatin2  14670  pfxccatin12lem3  14673  reim0  15060  re0  15094  im0  15095  rei  15098  imi  15099  cj0  15100  sqeqd  15108  rennim  15181  cnpart  15182  sqrt0  15183  01sqrexlem4  15187  resqrex  15192  sqrtgt0  15200  sqrt00  15205  sqrtneglem  15208  sqrt9  15215  sqrt2gt1lt2  15216  leabs  15241  absor  15242  max0add  15252  eqsqrt2d  15311  sqrtpclii  15325  rlimconst  15486  rlimrege0  15521  lo1mul  15570  iserge0  15603  fsum00  15740  isumless  15787  arisum2  15803  georeclim  15814  geo2sum  15815  geoisumr  15820  0.999...  15823  cvgrat  15825  fprodge0  15935  bpoly4  16001  cos0  16094  ef01bndlem  16128  sin01bnd  16129  cos01bnd  16130  cos2bnd  16132  sin01gt0  16134  cos01gt0  16135  sincos2sgn  16138  sin4lt0  16139  absef  16141  absefib  16142  efieq1re  16143  epos  16151  rpnnen2lem2  16159  rpnnen2lem3  16160  rpnnen2lem4  16161  rpnnen2lem9  16166  ruclem6  16179  dvdslelem  16255  divalglem1  16340  divalglem5  16343  divalglem6  16344  flodddiv4  16361  sadcadd  16404  gcdn0gt0  16464  nn0seqcvgd  16516  algcvgblem  16523  algcvga  16525  pythagtriplem12  16773  pythagtriplem13  16774  pythagtriplem14  16775  pythagtriplem16  16777  prmreclem4  16866  prmreclem5  16867  prmreclem6  16868  1arith  16874  ramz  16972  mulgnegnn  18998  subgmulg  19054  srgbinomlem4  20149  isabvd  20732  abvtrivd  20752  rge0srg  21380  xrs1mnd  21382  xrs10  21383  psgnodpmr  21532  re0g  21554  psrbaglesupp  21864  psdmvr  22089  mnfnei  23141  imasdsf1olem  24294  ssblps  24343  ssbl  24344  xmeter  24354  dscmet  24493  dscopn  24494  nmoi  24649  nmoeq0  24657  0nghm  24662  idnghm  24664  cnbl0  24694  xrsxmet  24731  metdseq0  24776  iicmp  24812  iiconn  24813  iihalf1  24858  iihalf1cnOLD  24860  elii1  24864  icopnfcnv  24873  icopnfhmeo  24874  iccpnfcnv  24875  xrhmeo  24877  xrhmph  24878  htpycc  24912  reparphti  24929  reparphtiOLD  24930  pcoval1  24946  pco0  24947  pcoval2  24949  pcocn  24950  pcohtpylem  24952  pcopt  24955  pcopt2  24956  pcoass  24957  pcorevlem  24959  reust  25314  recusp  25315  rrx0el  25331  minveclem4c  25358  minveclem2  25359  minveclem3b  25361  minveclem4  25365  minveclem7  25368  pjthlem1  25370  cniccbdd  25395  ovolunnul  25434  ovoliunnul  25441  ovolicc1  25450  ovolre  25459  iccvolcl  25501  ovolioo  25502  ioovolcl  25504  ioorcl  25511  vitalilem4  25545  vitalilem5  25546  vitali  25547  ismbf  25562  mbfmulc2lem  25581  mbfpos  25585  mbfposr  25586  i1f0  25621  i1f1  25624  itg1addlem2  25631  itg1addlem4  25633  itg1addlem5  25634  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  mbfi1flimlem  25656  xrge0f  25665  itg2ge0  25669  itg2const  25674  itg2mulc  25681  itg2splitlem  25682  itg2gt0  25694  itg2cnlem1  25695  ibl0  25721  iblrelem  25725  iblposlem  25726  iblpos  25727  iblre  25728  itgreval  25731  itgneg  25738  iblss  25739  i1fibl  25742  itgitg1  25743  itgle  25744  itgeqa  25748  itgless  25751  iblconst  25752  itgconst  25753  ibladdlem  25754  itgaddlem2  25758  iblabslem  25762  iblabsr  25764  iblmulc2  25765  itgmulc2lem2  25767  itgabs  25769  itgsplit  25770  bddmulibl  25773  dvferm1  25922  dvferm2  25924  dvferm  25925  dvlip  25931  c1lip1  25935  dveq0  25938  dv11cn  25939  dvne0  25949  ftc1lem4  25979  ply1divex  26075  dgrco  26214  plyrecj  26220  vieta1lem2  26252  aalioulem2  26274  aalioulem3  26275  pserulm  26364  psercnlem2  26367  psercnlem1  26368  psercn  26369  abelth  26384  reeff1olem  26389  reeff1o  26390  pilem2  26395  pilem3  26396  pipos  26401  sinhalfpilem  26405  sincosq1sgn  26440  sincosq2sgn  26441  coseq00topi  26444  coseq0negpitopi  26445  tangtx  26447  tanabsge  26448  sinq12ge0  26450  sinq34lt0t  26451  cosq14ge0  26453  sincos4thpi  26455  sincos6thpi  26458  pige3ALT  26462  sineq0  26466  cosordlem  26472  cosord  26473  cos0pilt1  26474  cos11  26475  sinord  26476  recosf1o  26477  resinf1o  26478  tanord1  26479  tanord  26480  tanregt0  26481  efif1olem4  26487  efifo  26489  relogrn  26503  log1  26527  logi  26529  logneg  26530  argregt0  26552  argrege0  26553  argimgt0  26554  logneg2  26557  logdivlti  26562  logdivlt  26563  ellogdm  26581  logdmn0  26582  logdmnrp  26583  logcnlem3  26586  dvloglem  26590  logdmopn  26591  logf1o2  26592  dvlog2lem  26594  efopnlem1  26598  logtayl  26602  recxpcl  26617  cxpge0  26625  cxple2  26639  cxple2a  26641  cxpsqrtlem  26644  cxpcn3  26691  cxpaddlelem  26694  cxpaddle  26695  loglesqrt  26704  logbrec  26725  ang180lem3  26754  ang180lem4  26755  asinneg  26829  asin1  26837  reasinsin  26839  acosbnd  26843  atan0  26851  atanrecl  26854  atanlogaddlem  26856  atanlogsublem  26858  atanlogsub  26859  atantan  26866  atanbnd  26869  atan1  26871  atans2  26874  ressatans  26877  log2cnv  26887  log2tlbnd  26888  log2ub  26892  log2le1  26893  rlimcnp  26908  rlimcnp2  26909  o1cxp  26918  jensen  26932  amgm  26934  emgt0  26950  harmonicbnd3  26951  harmoniclbnd  26952  harmonicbnd4  26954  zetacvg  26958  eldmgm  26965  lgamgulmlem2  26973  basellem3  27026  basellem8  27031  efnnfsumcl  27046  ppisval  27047  vmage0  27064  chpge0  27069  efchtdvds  27102  ppiltx  27120  ppiub  27148  chpeq0  27152  chteq0  27153  chtleppi  27154  chpchtsum  27163  chpub  27164  dchr1re  27207  bcmono  27221  efexple  27225  bposlem1  27228  bposlem4  27231  bposlem5  27232  bposlem7  27234  bposlem8  27235  bposlem9  27236  lgsval2lem  27251  lgsval4a  27263  lgsneg  27265  lgsdilem  27268  lgsdir2lem1  27269  2lgsoddprmlem3a  27354  2lgsoddprmlem3b  27355  2lgsoddprmlem3c  27356  2lgsoddprmlem3d  27357  rplogsumlem2  27429  rpvmasumlem  27431  dchrisum0flblem1  27452  dchrisum0flblem2  27453  dchrisum0fno1  27455  rplogsum  27471  logdivsum  27477  mulog2sumlem2  27479  selberg2lem  27494  logdivbnd  27500  pntrsumo1  27509  pntrlog2bndlem4  27524  pntrlog2bndlem5  27525  pntpbnd1  27530  pntpbnd2  27531  pntlem3  27553  pntleml  27555  ostth2  27581  trgcgrg  28495  ttgcontlem1  28865  axlowdimlem1  28922  axlowdimlem6  28927  axlowdimlem7  28928  axlowdimlem10  28931  axlowdim1  28939  axlowdim2  28940  axlowdim  28941  elntg2  28965  umgrislfupgrlem  29102  lfgrnloop  29105  lfuhgr1v0e  29234  usgrexmplef  29239  pthdlem2  29748  crctcshwlkn0lem7  29796  rusgrnumwwlks  29954  clwwlkn0  30007  konigsberg  30236  ex-po  30414  ex-sqrt  30433  ex-gcd  30436  nvz0  30647  0blo  30771  nmlno0lem  30772  nmblolbii  30778  siilem2  30831  minvecolem2  30854  minvecolem3  30855  minvecolem4c  30858  minvecolem4  30859  minvecolem5  30860  minvecolem7  30862  htthlem  30896  hiidge0  31077  normlem6  31094  normgt0  31106  norm-i  31108  normpyc  31125  bcsiALT  31158  pjhthlem1  31370  pjneli  31702  nmlnop0iALT  31974  unopbd  31994  nmbdoplbi  32003  nmcoplbi  32007  nmbdfnlbi  32028  nmbdfnlb  32029  nmcfnlbi  32031  cnlnadjlem7  32052  nmopcoi  32074  branmfn  32084  leopmul  32113  nmopleid  32118  pjbdlni  32128  pjnormssi  32147  stle0i  32218  cdj3lem1  32413  xaddeq0  32726  expgt0b  32791  pr01ssre  32799  sgnclre  32807  sgnnbi  32813  sgnpbi  32814  indf  32828  indfval  32829  dp20u  32848  dp20h  32849  dp2clq  32851  dp2lt10  32854  dp2lt  32855  dp0u  32871  dplti  32875  dpexpp1  32878  xdiv0  32899  chnub  32984  xrge0slmod  33312  evl1deg3  33540  fldext2chn  33711  cos9thpiminplylem1  33765  unitdivcld  33884  sqsscirc1  33891  xrge0iifcnv  33916  xrge0iifiso  33918  rezh  33952  esumcvgsum  34071  voliune  34212  volfiniune  34213  sibfinima  34323  sitmcl  34335  0rrv  34435  coinfliprv  34467  ballotlem2  34473  ballotlem4  34483  ballotlemi1  34487  ballotlemic  34491  plymulx0  34531  signsply0  34535  signswch  34545  signstf  34550  signstf0  34552  signstfveq0  34561  signlem0  34571  signshf  34572  itgexpif  34590  hgt750lemd  34632  hgt750lem  34635  hgt750lem2  34636  hgt750leme  34642  iisconn  35232  iillysconn  35233  cvmliftlem10  35274  fz0n  35711  bcneg1  35716  nn0prpwlem  36303  dnizeq0  36456  dnizphlfeqhlf  36457  knoppndvlem13  36505  cnndvlem1  36518  bj-pinftyccb  37202  bj-minftyccb  37206  bj-pinftynminfty  37208  taupilemrplb  37301  irrdiff  37307  sin2h  37597  tan2h  37599  ptrecube  37607  poimirlem16  37623  poimirlem17  37624  poimirlem20  37627  poimirlem22  37629  poimirlem23  37630  poimirlem29  37636  poimirlem31  37638  poimir  37640  heicant  37642  mblfinlem2  37645  ismblfin  37648  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  mbfposadd  37654  itg2addnclem  37658  itg2addnclem2  37659  ibladdnclem  37663  itgaddnclem2  37666  iblabsnclem  37670  iblmulc2nc  37672  itgmulc2nclem2  37674  itgabsnc  37676  ftc1cnnclem  37678  ftc1anclem5  37684  ftc1anclem8  37687  asindmre  37690  dvasin  37691  areacirclem4  37698  areacirc  37700  isbnd3  37771  ssbnd  37775  prdsbnd  37780  bfplem2  37810  bfp  37811  renegclALT  38949  0cnALT3  42234  sn-1ne2  42246  itrere  42299  oexpreposd  42303  tan3rdpi  42333  asin1half  42338  readvrec2  42342  sn-00idlem2  42380  sn-00idlem3  42381  sn-00id  42382  sn-0tie0  42432  sn-ltaddpos  42434  sn-ltaddneg  42435  relt0neg1  42437  sn-nnne0  42441  reelznn0nn  42442  sn-0lt1  42456  sn-inelr  42468  sn-itrere  42469  sn-retire  42470  pellexlem6  42815  elpell14qr2  42843  oddcomabszz  42926  zindbi  42928  jm2.24  42945  acongeq  42965  arearect  43197  areaquad  43198  reabsifneg  43614  reabsifnpos  43615  reabsifpos  43616  reabsifnneg  43617  imsqrtvalex  43628  relexp01min  43695  imo72b2lem2  44149  imo72b2lem1  44151  imo72b2  44154  dvconstbi  44316  binomcxplemnn0  44331  binomcxplemdvbinom  44335  binomcxplemcvg  44336  binomcxplemnotnn0  44338  sineq0ALT  44919  halffl  45287  ren0  45391  rexanuz2nf  45481  sqrlearg  45544  limsup10ex  45764  dvnmptdivc  45929  dvnmul  45934  itgsin0pilem1  45941  itgsinexplem1  45945  itgsinexp  45946  iblempty  45956  stoweidlem17  46008  stoweidlem36  46027  stoweidlem55  46046  wallispilem1  46056  wallispilem2  46057  wallispilem4  46059  stirlinglem4  46068  stirlinglem13  46077  stirlinglem14  46078  stirlinglem15  46079  stirlingr  46081  dirker2re  46083  dirkerdenne0  46084  dirkerre  46086  dirkertrigeqlem1  46089  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem11  46109  fourierdlem16  46114  fourierdlem21  46119  fourierdlem22  46120  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fourierdlem62  46159  fourierdlem66  46163  fourierdlem79  46176  fourierdlem83  46180  fourierdlem94  46191  fourierdlem102  46199  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  fourierdlem112  46209  fourierdlem113  46210  fourierdlem114  46211  sqwvfoura  46219  sqwvfourb  46220  fourierswlem  46221  fouriersw  46222  etransclem23  46248  etransclem44  46269  etransclem46  46271  salexct3  46333  salgensscntex  46335  sge0rnn0  46359  sge00  46367  0ome  46520  ovn0lem  46556  ovnhoilem1  46592  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  smfmullem4  46785  squeezedltsq  46880  zm1nn  47296  sqrtnegnre  47301  m1mod0mod1  47348  fmtnoprmfac2lem1  47560  31prm  47591  mod42tp1mod8  47596  nfermltl2rev  47737  tgblthelfgott  47809  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb0  48015  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpgusgralem  48040  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  altgsumbcALT  48334  expnegico01  48500  dignnld  48585  eenglngeehlnmlem1  48719  line2ylem  48733  line2y  48737  itsclc0yqsollem2  48745  icccldii  48900  i0oii  48901  sepfsepc  48909  ex-gt  49710