Theorem 0re 11292

Description: The number 0 is real. Remark: the first step could also be ax-icn 11243. See also 0reALT 11633. (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 11242	. 2 ⊢ 1 ∈ ℂ
2		cnre 11287	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 11255	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 11267	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2832	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 245	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3161	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 480	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3153	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∃wrex 3076  (class class class)co 7448  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185  ici 11186   + caddc 11187   · cmul 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addrcl 11245  ax-rnegex 11255  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-rex 3077

This theorem is referenced by:  0red  11293  0xr  11337  axmulgt0  11364  ne0gt0  11395  00id  11465  mul02lem1  11466  mul02lem2  11467  mul02  11468  addrid  11470  ltaddneg  11505  addgt0  11776  addgegt0  11777  addgtge0  11778  addge0  11779  ltaddpos  11780  ltneg  11790  leneg  11793  lt0neg1  11796  lt0neg2  11797  le0neg1  11798  le0neg2  11799  addge01  11800  suble0  11804  mulge0  11808  msqge0  11811  0le1  11813  relin01  11814  gt0ne0i  11825  gt0ne0d  11854  lt0ne0d  11855  elimge0  12133  ltm1  12136  recgt0  12140  prodgt0  12141  lemul1a  12148  ltmul12a  12150  lemul12a  12152  mulgt1OLD  12153  gt0div  12161  ge0div  12162  mulge0b  12165  lediv12a  12188  recgt1i  12192  recreclt  12194  ledivp1  12197  squeeze0  12198  recgt0ii  12201  ledivp1i  12220  ltdivp1i  12221  fimaxre2  12240  inelr  12283  crne0  12286  nnge1  12321  nngt0  12324  nnnle0  12326  nnne0  12327  nnrecgt0  12336  0le0  12394  neg1lt0  12410  halfge0  12510  nn0ssre  12557  nn0ge0  12578  nn0nlt0  12579  nn0le0eq0  12581  0mnnnnn0  12585  elnnnn0b  12597  elnnnn0c  12598  nn0sub  12603  elnnz  12649  0z  12650  elnn0z  12652  elnnz1  12669  recnz  12718  gtndiv  12720  fnn0ind  12742  10re  12777  rpge0  13070  rpneg  13089  0nrp  13092  0ltpnf  13185  mnflt0  13188  qsqueeze  13263  xneg0  13274  xaddrid  13303  xnn0xadd0  13309  xmulpnf1  13336  xlemul1a  13350  xadddi  13357  xrsupsslem  13369  xrinfmsslem  13370  elrege0  13514  0e0icopnf  13518  elicc01  13526  0elunit  13529  unitssre  13559  0nelfz1  13603  fzpreddisj  13633  fz0to4untppr  13687  fz0to5un2tp  13688  nn0p1elfzo  13759  ico01fl0  13870  rpsup  13917  modelico  13932  0mod  13953  1mod  13954  le2sq2  14185  expubnd  14227  sqlecan  14258  bernneq2  14279  expnbnd  14281  expnlbnd  14282  expmulnbnd  14284  discr1  14288  discr  14289  faclbnd  14339  faclbnd3  14341  faclbnd6  14348  bcval4  14356  bcval5  14367  bcpasc  14370  hasheq0  14412  hashneq0  14413  hashnn0n0nn  14440  hashgt12el  14471  hashgt12el2  14472  hashge2el2dif  14529  lsw0  14613  swrdccatin2  14777  pfxccatin12lem3  14780  reim0  15167  re0  15201  im0  15202  rei  15205  imi  15206  cj0  15207  sqeqd  15215  rennim  15288  cnpart  15289  sqrt0  15290  01sqrexlem4  15294  resqrex  15299  sqrtgt0  15307  sqrt00  15312  sqrtneglem  15315  sqrt9  15322  sqrt2gt1lt2  15323  leabs  15348  absor  15349  max0add  15359  eqsqrt2d  15417  sqrtpclii  15431  rlimconst  15590  rlimrege0  15625  lo1mul  15674  iserge0  15709  fsum00  15846  isumless  15893  arisum2  15909  georeclim  15920  geo2sum  15921  geoisumr  15926  0.999...  15929  cvgrat  15931  fprodge0  16041  bpoly4  16107  cos0  16198  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  cos2bnd  16236  sin01gt0  16238  cos01gt0  16239  sincos2sgn  16242  sin4lt0  16243  absef  16245  absefib  16246  efieq1re  16247  epos  16255  rpnnen2lem2  16263  rpnnen2lem3  16264  rpnnen2lem4  16265  rpnnen2lem9  16270  ruclem6  16283  dvdslelem  16357  divalglem1  16442  divalglem5  16445  divalglem6  16446  flodddiv4  16461  sadcadd  16504  gcdn0gt0  16564  nn0seqcvgd  16617  algcvgblem  16624  algcvga  16626  pythagtriplem12  16873  pythagtriplem13  16874  pythagtriplem14  16875  pythagtriplem16  16877  prmreclem4  16966  prmreclem5  16967  prmreclem6  16968  1arith  16974  ramz  17072  mulgnegnn  19124  subgmulg  19180  srgbinomlem4  20256  isabvd  20835  abvtrivd  20855  xrs1mnd  21445  xrs10  21446  rge0srg  21479  psgnodpmr  21631  re0g  21653  psrbaglesupp  21965  mnfnei  23250  imasdsf1olem  24404  ssblps  24453  ssbl  24454  xmeter  24464  dscmet  24606  dscopn  24607  nmoi  24770  nmoeq0  24778  0nghm  24783  idnghm  24785  cnbl0  24815  xrsxmet  24850  metdseq0  24895  iicmp  24931  iiconn  24932  iihalf1  24977  iihalf1cnOLD  24979  elii1  24983  icopnfcnv  24992  icopnfhmeo  24993  iccpnfcnv  24994  xrhmeo  24996  xrhmph  24997  htpycc  25031  reparphti  25048  reparphtiOLD  25049  pcoval1  25065  pco0  25066  pcoval2  25068  pcocn  25069  pcohtpylem  25071  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  reust  25434  recusp  25435  rrx0el  25451  minveclem4c  25478  minveclem2  25479  minveclem3b  25481  minveclem4  25485  minveclem7  25488  pjthlem1  25490  cniccbdd  25515  ovolunnul  25554  ovoliunnul  25561  ovolicc1  25570  ovolre  25579  iccvolcl  25621  ovolioo  25622  ioovolcl  25624  ioorcl  25631  vitalilem4  25665  vitalilem5  25666  vitali  25667  ismbf  25682  mbfmulc2lem  25701  mbfpos  25705  mbfposr  25706  i1f0  25741  i1f1  25744  itg1addlem2  25751  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfi1flimlem  25777  xrge0f  25786  itg2ge0  25790  itg2const  25795  itg2mulc  25802  itg2splitlem  25803  itg2gt0  25815  itg2cnlem1  25816  ibl0  25842  iblrelem  25846  iblposlem  25847  iblpos  25848  iblre  25849  itgreval  25852  itgneg  25859  iblss  25860  i1fibl  25863  itgitg1  25864  itgle  25865  itgeqa  25869  itgless  25872  iblconst  25873  itgconst  25874  ibladdlem  25875  itgaddlem2  25879  iblabslem  25883  iblabsr  25885  iblmulc2  25886  itgmulc2lem2  25888  itgabs  25890  itgsplit  25891  bddmulibl  25894  dvferm1  26043  dvferm2  26045  dvferm  26046  dvlip  26052  c1lip1  26056  dveq0  26059  dv11cn  26060  dvne0  26070  ftc1lem4  26100  ply1divex  26196  dgrco  26335  plyrecj  26339  vieta1lem2  26371  aalioulem2  26393  aalioulem3  26394  pserulm  26483  psercnlem2  26486  psercnlem1  26487  psercn  26488  abelth  26503  reeff1olem  26508  reeff1o  26509  pilem2  26514  pilem3  26515  pipos  26520  sinhalfpilem  26523  sincosq1sgn  26558  sincosq2sgn  26559  coseq00topi  26562  coseq0negpitopi  26563  tangtx  26565  tanabsge  26566  sinq12ge0  26568  sinq34lt0t  26569  cosq14ge0  26571  sincos4thpi  26573  sincos6thpi  26576  pige3ALT  26580  sineq0  26584  cosordlem  26590  cosord  26591  cos0pilt1  26592  cos11  26593  sinord  26594  recosf1o  26595  resinf1o  26596  tanord1  26597  tanord  26598  tanregt0  26599  efif1olem4  26605  efifo  26607  relogrn  26621  log1  26645  logi  26647  logneg  26648  argregt0  26670  argrege0  26671  argimgt0  26672  logneg2  26675  logdivlti  26680  logdivlt  26681  ellogdm  26699  logdmn0  26700  logdmnrp  26701  logcnlem3  26704  dvloglem  26708  logdmopn  26709  logf1o2  26710  dvlog2lem  26712  efopnlem1  26716  logtayl  26720  recxpcl  26735  cxpge0  26743  cxple2  26757  cxple2a  26759  cxpsqrtlem  26762  cxpcn3  26809  cxpaddlelem  26812  cxpaddle  26813  loglesqrt  26822  logbrec  26843  ang180lem3  26872  ang180lem4  26873  asinneg  26947  asin1  26955  reasinsin  26957  acosbnd  26961  atan0  26969  atanrecl  26972  atanlogaddlem  26974  atanlogsublem  26976  atanlogsub  26977  atantan  26984  atanbnd  26987  atan1  26989  atans2  26992  ressatans  26995  log2cnv  27005  log2tlbnd  27006  log2ub  27010  log2le1  27011  rlimcnp  27026  rlimcnp2  27027  o1cxp  27036  jensen  27050  amgm  27052  emgt0  27068  harmonicbnd3  27069  harmoniclbnd  27070  harmonicbnd4  27072  zetacvg  27076  eldmgm  27083  lgamgulmlem2  27091  basellem3  27144  basellem8  27149  efnnfsumcl  27164  ppisval  27165  vmage0  27182  chpge0  27187  efchtdvds  27220  ppiltx  27238  ppiub  27266  chpeq0  27270  chteq0  27271  chtleppi  27272  chpchtsum  27281  chpub  27282  dchr1re  27325  bcmono  27339  efexple  27343  bposlem1  27346  bposlem4  27349  bposlem5  27350  bposlem7  27352  bposlem8  27353  bposlem9  27354  lgsval2lem  27369  lgsval4a  27381  lgsneg  27383  lgsdilem  27386  lgsdir2lem1  27387  2lgsoddprmlem3a  27472  2lgsoddprmlem3b  27473  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  rplogsumlem2  27547  rpvmasumlem  27549  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0fno1  27573  rplogsum  27589  logdivsum  27595  mulog2sumlem2  27597  selberg2lem  27612  logdivbnd  27618  pntrsumo1  27627  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntpbnd1  27648  pntpbnd2  27649  pntlem3  27671  pntleml  27673  ostth2  27699  trgcgrg  28541  ttgcontlem1  28917  axlowdimlem1  28975  axlowdimlem6  28980  axlowdimlem7  28981  axlowdimlem10  28984  axlowdim1  28992  axlowdim2  28993  axlowdim  28994  elntg2  29018  umgrislfupgrlem  29157  lfgrnloop  29160  lfuhgr1v0e  29289  usgrexmplef  29294  pthdlem2  29804  crctcshwlkn0lem7  29849  rusgrnumwwlks  30007  clwwlkn0  30060  konigsberg  30289  ex-po  30467  ex-sqrt  30486  ex-gcd  30489  nvz0  30700  0blo  30824  nmlno0lem  30825  nmblolbii  30831  siilem2  30884  minvecolem2  30907  minvecolem3  30908  minvecolem4c  30911  minvecolem4  30912  minvecolem5  30913  minvecolem7  30915  htthlem  30949  hiidge0  31130  normlem6  31147  normgt0  31159  norm-i  31161  normpyc  31178  bcsiALT  31211  pjhthlem1  31423  pjneli  31755  nmlnop0iALT  32027  unopbd  32047  nmbdoplbi  32056  nmcoplbi  32060  nmbdfnlbi  32081  nmbdfnlb  32082  nmcfnlbi  32084  cnlnadjlem7  32105  nmopcoi  32127  branmfn  32137  leopmul  32166  nmopleid  32171  pjbdlni  32181  pjnormssi  32200  stle0i  32271  cdj3lem1  32466  xaddeq0  32760  expgt0b  32820  pr01ssre  32828  dp20u  32842  dp20h  32843  dp2clq  32845  dp2lt10  32848  dp2lt  32849  dp0u  32865  dplti  32869  dpexpp1  32872  xdiv0  32893  chnub  32984  xrge0slmod  33341  evl1deg3  33568  fldext2chn  33719  unitdivcld  33847  sqsscirc1  33854  xrge0iifcnv  33879  xrge0iifiso  33881  rezh  33917  indf  33979  indfval  33980  esumcvgsum  34052  voliune  34193  volfiniune  34194  sibfinima  34304  sitmcl  34316  0rrv  34416  coinfliprv  34447  ballotlem2  34453  ballotlem4  34463  ballotlemi1  34467  ballotlemic  34471  sgnclre  34504  sgnnbi  34510  sgnpbi  34511  plymulx0  34524  signsply0  34528  signswch  34538  signstf  34543  signstf0  34545  signstfveq0  34554  signlem0  34564  signshf  34565  itgexpif  34583  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  iisconn  35220  iillysconn  35221  cvmliftlem10  35262  fz0n  35693  bcneg1  35698  nn0prpwlem  36288  dnizeq0  36441  dnizphlfeqhlf  36442  knoppndvlem13  36490  cnndvlem1  36503  bj-pinftyccb  37187  bj-minftyccb  37191  bj-pinftynminfty  37193  taupilemrplb  37286  irrdiff  37292  sin2h  37570  tan2h  37572  ptrecube  37580  poimirlem16  37596  poimirlem17  37597  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem29  37609  poimirlem31  37611  poimir  37613  heicant  37615  mblfinlem2  37618  ismblfin  37621  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  mbfposadd  37627  itg2addnclem  37631  itg2addnclem2  37632  ibladdnclem  37636  itgaddnclem2  37639  iblabsnclem  37643  iblmulc2nc  37645  itgmulc2nclem2  37647  itgabsnc  37649  ftc1cnnclem  37651  ftc1anclem5  37657  ftc1anclem8  37660  asindmre  37663  dvasin  37664  areacirclem4  37671  areacirc  37673  isbnd3  37744  ssbnd  37748  prdsbnd  37753  bfplem2  37783  bfp  37784  renegclALT  38919  2xp3dxp2ge1d  42198  factwoffsmonot  42199  0cnALT3  42248  sn-1ne2  42254  itrere  42307  oexpreposd  42309  tan3rdpi  42338  asin1half  42339  sn-00idlem2  42375  sn-00idlem3  42376  sn-00id  42377  sn-0tie0  42415  sn-ltaddpos  42417  sn-ltaddneg  42418  relt0neg1  42420  sn-nnne0  42424  reelznn0nn  42425  sn-0lt1  42439  sn-inelr  42443  sn-itrere  42444  sn-retire  42445  pellexlem6  42790  elpell14qr2  42818  oddcomabszz  42901  zindbi  42903  jm2.24  42920  acongeq  42940  arearect  43176  areaquad  43177  reabsifneg  43594  reabsifnpos  43595  reabsifpos  43596  reabsifnneg  43597  imsqrtvalex  43608  relexp01min  43675  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2lem1  44131  imo72b2  44134  dvconstbi  44303  binomcxplemnn0  44318  binomcxplemdvbinom  44322  binomcxplemcvg  44323  binomcxplemnotnn0  44325  sineq0ALT  44908  halffl  45211  ren0  45317  rexanuz2nf  45408  sqrlearg  45471  limsup10ex  45694  dvnmptdivc  45859  dvnmul  45864  itgsin0pilem1  45871  itgsinexplem1  45875  itgsinexp  45876  iblempty  45886  stoweidlem17  45938  stoweidlem36  45957  stoweidlem55  45976  wallispilem1  45986  wallispilem2  45987  wallispilem4  45989  stirlinglem4  45998  stirlinglem13  46007  stirlinglem14  46008  stirlinglem15  46009  stirlingr  46011  dirker2re  46013  dirkerdenne0  46014  dirkerre  46016  dirkertrigeqlem1  46019  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem11  46039  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem62  46089  fourierdlem66  46093  fourierdlem79  46106  fourierdlem83  46110  fourierdlem94  46121  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fourierdlem114  46141  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  etransclem23  46178  etransclem44  46199  etransclem46  46201  salexct3  46263  salgensscntex  46265  sge0rnn0  46289  sge00  46297  0ome  46450  ovn0lem  46486  ovnhoilem1  46522  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714  smfmullem4  46715  zm1nn  47217  sqrtnegnre  47222  m1mod0mod1  47243  fmtnoprmfac2lem1  47440  31prm  47471  mod42tp1mod8  47476  nfermltl2rev  47617  tgblthelfgott  47689  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  altgsumbcALT  48078  expnegico01  48247  dignnld  48337  eenglngeehlnmlem1  48471  line2ylem  48485  line2y  48489  itsclc0yqsollem2  48497  icccldii  48598  i0oii  48599  sepfsepc  48607  ex-gt  48820