Theorem 0re 10681

Description: The number 0 is real. Remark: the first step could also be ax-icn 10634. See also 0reALT 11021. (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 10633	. 2 ⊢ 1 ∈ ℂ
2		cnre 10676	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 10646	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 10658	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2839	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 248	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3208	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 484	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3205	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃wrex 3071  (class class class)co 7150  ℂcc 10573  ℝcr 10574  0cc0 10575  1c1 10576  ici 10577   + caddc 10578   · cmul 10580

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-1cn 10633  ax-addrcl 10636  ax-rnegex 10646  ax-cnre 10648

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076

This theorem is referenced by:  0red  10682  0xr  10726  axmulgt0  10753  ne0gt0  10783  00id  10853  mul02lem1  10854  mul02lem2  10855  mul02  10856  addid1  10858  ltaddneg  10893  addgt0  11164  addgegt0  11165  addgtge0  11166  addge0  11167  ltaddpos  11168  ltneg  11178  leneg  11181  lt0neg1  11184  lt0neg2  11185  le0neg1  11186  le0neg2  11187  addge01  11188  suble0  11192  mulge0  11196  msqge0  11199  0le1  11201  relin01  11202  gt0ne0i  11213  gt0ne0d  11242  lt0ne0d  11243  elimge0  11517  ltm1  11520  recgt0  11524  prodgt0  11525  lemul1a  11532  ltmul12a  11534  lemul12a  11536  mulgt1  11537  gt0div  11544  ge0div  11545  mulge0b  11548  lediv12a  11571  recgt1i  11575  recreclt  11577  ledivp1  11580  squeeze0  11581  recgt0ii  11584  ledivp1i  11603  ltdivp1i  11604  fimaxre2  11623  inelr  11664  crne0  11667  nnge1  11702  nngt0  11705  nnnle0  11707  nnne0  11708  nnrecgt0  11717  0le0  11775  neg1lt0  11791  halfge0  11891  nn0ssre  11938  nn0ge0  11959  nn0nlt0  11960  nn0le0eq0  11962  0mnnnnn0  11966  elnnnn0b  11978  elnnnn0c  11979  nn0sub  11984  elnnz  12030  0z  12031  elnn0z  12033  elnnz1  12047  recnz  12096  gtndiv  12098  fnn0ind  12120  10re  12156  rpge0  12443  rpneg  12462  0nrp  12465  0ltpnf  12558  mnflt0  12561  qsqueeze  12635  xneg0  12646  xaddid1  12675  xnn0xadd0  12681  xmulpnf1  12708  xlemul1a  12722  xadddi  12729  xrsupsslem  12741  xrinfmsslem  12742  elrege0  12886  0e0icopnf  12890  elicc01  12898  0elunit  12901  unitssre  12931  0nelfz1  12975  fzpreddisj  13005  fz0to4untppr  13059  nn0p1elfzo  13129  ico01fl0  13238  rpsup  13283  modelico  13298  0mod  13319  1mod  13320  le2sq2  13550  expubnd  13591  sqlecan  13621  bernneq2  13641  expnbnd  13643  expnlbnd  13644  expmulnbnd  13646  discr1  13650  discr  13651  faclbnd  13700  faclbnd3  13702  faclbnd6  13709  bcval4  13717  bcval5  13728  bcpasc  13731  hasheq0  13774  hashneq0  13775  hashnn0n0nn  13802  hashgt12el  13833  hashgt12el2  13834  hashge2el2dif  13890  lsw0  13964  swrdccatin2  14138  pfxccatin12lem3  14141  reim0  14525  re0  14559  im0  14560  rei  14563  imi  14564  cj0  14565  sqeqd  14573  rennim  14646  cnpart  14647  sqr0lem  14648  sqrlem4  14653  resqrex  14658  sqrtgt0  14666  sqrt00  14671  sqrtneglem  14674  sqrt9  14681  sqrt2gt1lt2  14682  leabs  14707  absor  14708  max0add  14718  eqsqrt2d  14776  sqrtpclii  14790  rlimconst  14949  rlimrege0  14984  lo1mul  15032  iserge0  15065  fsum00  15201  isumless  15248  arisum2  15264  georeclim  15276  geo2sum  15277  geoisumr  15282  0.999...  15285  cvgrat  15287  fprodge0  15395  bpoly4  15461  cos0  15551  ef01bndlem  15585  sin01bnd  15586  cos01bnd  15587  cos2bnd  15589  sin01gt0  15591  cos01gt0  15592  sincos2sgn  15595  sin4lt0  15596  absef  15598  absefib  15599  efieq1re  15600  epos  15608  rpnnen2lem2  15616  rpnnen2lem3  15617  rpnnen2lem4  15618  rpnnen2lem9  15623  ruclem6  15636  dvdslelem  15710  divalglem1  15795  divalglem5  15798  divalglem6  15799  flodddiv4  15814  sadcadd  15857  gcdn0gt0  15917  nn0seqcvgd  15966  algcvgblem  15973  algcvga  15975  pythagtriplem12  16218  pythagtriplem13  16219  pythagtriplem14  16220  pythagtriplem16  16222  prmreclem4  16310  prmreclem5  16311  prmreclem6  16312  1arith  16318  ramz  16416  mulgnegnn  18305  subgmulg  18360  srgbinomlem4  19361  isabvd  19659  abvtrivd  19679  xrs1mnd  20204  xrs10  20205  rge0srg  20237  psgnodpmr  20355  re0g  20377  psrbaglesupp  20686  psrbaglesuppOLD  20687  mnfnei  21921  imasdsf1olem  23075  ssblps  23124  ssbl  23125  xmeter  23135  dscmet  23274  dscopn  23275  nmoi  23430  nmoeq0  23438  0nghm  23443  idnghm  23445  cnbl0  23475  xrsxmet  23510  metdseq0  23555  iicmp  23587  iiconn  23588  iihalf1  23632  iihalf1cn  23633  elii1  23636  icopnfcnv  23643  icopnfhmeo  23644  iccpnfcnv  23645  xrhmeo  23647  xrhmph  23648  htpycc  23681  reparphti  23698  pcoval1  23714  pco0  23715  pcoval2  23717  pcocn  23718  pcohtpylem  23720  pcopt  23723  pcopt2  23724  pcoass  23725  pcorevlem  23727  reust  24081  recusp  24082  rrx0el  24098  minveclem4c  24125  minveclem2  24126  minveclem3b  24128  minveclem4  24132  minveclem7  24135  pjthlem1  24137  cniccbdd  24161  ovolunnul  24200  ovoliunnul  24207  ovolicc1  24216  ovolre  24225  iccvolcl  24267  ovolioo  24268  ioovolcl  24270  ioorcl  24277  vitalilem4  24311  vitalilem5  24312  vitali  24313  ismbf  24328  mbfmulc2lem  24347  mbfpos  24351  mbfposr  24352  i1f0  24387  i1f1  24390  itg1addlem2  24397  itg1addlem4  24399  itg1addlem5  24400  mbfi1fseqlem4  24418  mbfi1fseqlem5  24419  mbfi1flimlem  24422  xrge0f  24431  itg2ge0  24435  itg2const  24440  itg2mulc  24447  itg2splitlem  24448  itg2gt0  24460  itg2cnlem1  24461  ibl0  24486  iblrelem  24490  iblposlem  24491  iblpos  24492  iblre  24493  itgreval  24496  itgneg  24503  iblss  24504  i1fibl  24507  itgitg1  24508  itgle  24509  itgeqa  24513  itgless  24516  iblconst  24517  itgconst  24518  ibladdlem  24519  itgaddlem2  24523  iblabslem  24527  iblabsr  24529  iblmulc2  24530  itgmulc2lem2  24532  itgabs  24534  itgsplit  24535  bddmulibl  24538  dvferm1  24684  dvferm2  24686  dvferm  24687  dvlip  24692  c1lip1  24696  dveq0  24699  dv11cn  24700  dvne0  24710  ftc1lem4  24738  ply1divex  24836  dgrco  24971  plyrecj  24975  vieta1lem2  25006  aalioulem2  25028  aalioulem3  25029  pserulm  25116  psercnlem2  25118  psercnlem1  25119  psercn  25120  abelth  25135  reeff1olem  25140  reeff1o  25141  pilem2  25146  pilem3  25147  pipos  25152  sinhalfpilem  25155  sincosq1sgn  25190  sincosq2sgn  25191  coseq00topi  25194  coseq0negpitopi  25195  tangtx  25197  tanabsge  25198  sinq12ge0  25200  sinq34lt0t  25201  cosq14ge0  25203  sincos4thpi  25205  sincos6thpi  25207  pige3ALT  25211  sineq0  25215  cosordlem  25221  cosord  25222  cos0pilt1  25223  cos11  25224  sinord  25225  recosf1o  25226  resinf1o  25227  tanord1  25228  tanord  25229  tanregt0  25230  efif1olem4  25236  efifo  25238  relogrn  25252  log1  25276  logneg  25278  argregt0  25300  argrege0  25301  argimgt0  25302  logneg2  25305  logdivlti  25310  logdivlt  25311  ellogdm  25329  logdmn0  25330  logdmnrp  25331  logcnlem3  25334  dvloglem  25338  logdmopn  25339  logf1o2  25340  dvlog2lem  25342  efopnlem1  25346  logtayl  25350  recxpcl  25365  cxpge0  25373  cxple2  25387  cxple2a  25389  cxpsqrtlem  25392  cxpcn3  25436  cxpaddlelem  25439  cxpaddle  25440  loglesqrt  25446  logbrec  25467  ang180lem3  25496  ang180lem4  25497  asinneg  25571  asin1  25579  reasinsin  25581  acosbnd  25585  atan0  25593  atanrecl  25596  atanlogaddlem  25598  atanlogsublem  25600  atanlogsub  25601  atantan  25608  atanbnd  25611  atan1  25613  atans2  25616  ressatans  25619  log2cnv  25629  log2tlbnd  25630  log2ub  25634  log2le1  25635  rlimcnp  25650  rlimcnp2  25651  o1cxp  25659  jensen  25673  amgm  25675  emgt0  25691  harmonicbnd3  25692  harmoniclbnd  25693  harmonicbnd4  25695  zetacvg  25699  eldmgm  25706  lgamgulmlem2  25714  basellem3  25767  basellem8  25772  efnnfsumcl  25787  ppisval  25788  vmage0  25805  chpge0  25810  efchtdvds  25843  ppiltx  25861  ppiub  25887  chpeq0  25891  chteq0  25892  chtleppi  25893  chpchtsum  25902  chpub  25903  dchr1re  25946  bcmono  25960  efexple  25964  bposlem1  25967  bposlem4  25970  bposlem5  25971  bposlem7  25973  bposlem8  25974  bposlem9  25975  lgsval2lem  25990  lgsval4a  26002  lgsneg  26004  lgsdilem  26007  lgsdir2lem1  26008  2lgsoddprmlem3a  26093  2lgsoddprmlem3b  26094  2lgsoddprmlem3c  26095  2lgsoddprmlem3d  26096  rplogsumlem2  26168  rpvmasumlem  26170  dchrisum0flblem1  26191  dchrisum0flblem2  26192  dchrisum0fno1  26194  rplogsum  26210  logdivsum  26216  mulog2sumlem2  26218  selberg2lem  26233  logdivbnd  26239  pntrsumo1  26248  pntrlog2bndlem4  26263  pntrlog2bndlem5  26264  pntpbnd1  26269  pntpbnd2  26270  pntlem3  26292  pntleml  26294  ostth2  26320  trgcgrg  26408  ttgcontlem1  26778  axlowdimlem1  26835  axlowdimlem6  26840  axlowdimlem7  26841  axlowdimlem10  26844  axlowdim1  26852  axlowdim2  26853  axlowdim  26854  elntg2  26878  umgrislfupgrlem  27014  lfgrnloop  27017  lfuhgr1v0e  27143  usgrexmplef  27148  pthdlem2  27656  crctcshwlkn0lem7  27701  rusgrnumwwlks  27859  clwwlkn0  27912  konigsberg  28141  ex-po  28319  ex-sqrt  28338  ex-gcd  28341  nvz0  28550  0blo  28674  nmlno0lem  28675  nmblolbii  28681  siilem2  28734  minvecolem2  28757  minvecolem3  28758  minvecolem4c  28761  minvecolem4  28762  minvecolem5  28763  minvecolem7  28765  htthlem  28799  hiidge0  28980  normlem6  28997  normgt0  29009  norm-i  29011  normpyc  29028  bcsiALT  29061  pjhthlem1  29273  pjneli  29605  nmlnop0iALT  29877  unopbd  29897  nmbdoplbi  29906  nmcoplbi  29910  nmbdfnlbi  29931  nmbdfnlb  29932  nmcfnlbi  29934  cnlnadjlem7  29955  nmopcoi  29977  branmfn  29987  leopmul  30016  nmopleid  30021  pjbdlni  30031  pjnormssi  30050  stle0i  30121  cdj3lem1  30316  xaddeq0  30600  pr01ssre  30662  dp20u  30676  dp20h  30677  dp2clq  30679  dp2lt10  30682  dp2lt  30683  dp0u  30699  dplti  30703  dpexpp1  30706  xdiv0  30727  xrge0slmod  31069  unitdivcld  31372  sqsscirc1  31379  xrge0iifcnv  31404  xrge0iifiso  31406  rezh  31440  indf  31502  indfval  31503  esumcvgsum  31575  voliune  31716  volfiniune  31717  sibfinima  31825  sitmcl  31837  0rrv  31937  coinfliprv  31968  ballotlem2  31974  ballotlem4  31984  ballotlemi1  31988  ballotlemic  31992  sgnclre  32025  sgnnbi  32031  sgnpbi  32032  plymulx0  32045  signsply0  32049  signswch  32059  signstf  32064  signstf0  32066  signstfveq0  32075  signlem0  32085  signshf  32086  itgexpif  32105  hgt750lemd  32147  hgt750lem  32150  hgt750lem2  32151  hgt750leme  32157  iisconn  32730  iillysconn  32731  cvmliftlem10  32772  fz0n  33211  logi  33215  bcneg1  33217  nn0prpwlem  34060  dnizeq0  34204  dnizphlfeqhlf  34205  knoppndvlem13  34253  cnndvlem1  34266  bj-pinftyccb  34916  bj-minftyccb  34920  bj-pinftynminfty  34922  bj-isrvec  34988  taupilemrplb  35014  irrdiff  35020  sin2h  35327  tan2h  35329  ptrecube  35337  poimirlem16  35353  poimirlem17  35354  poimirlem20  35357  poimirlem22  35359  poimirlem23  35360  poimirlem29  35366  poimirlem31  35368  poimir  35370  heicant  35372  mblfinlem2  35375  ismblfin  35378  ovoliunnfl  35379  voliunnfl  35381  volsupnfl  35382  mbfposadd  35384  itg2addnclem  35388  itg2addnclem2  35389  ibladdnclem  35393  itgaddnclem2  35396  iblabsnclem  35400  iblmulc2nc  35402  itgmulc2nclem2  35404  itgabsnc  35406  ftc1cnnclem  35408  ftc1anclem5  35414  ftc1anclem8  35417  asindmre  35420  dvasin  35421  areacirclem4  35428  areacirc  35430  isbnd3  35502  ssbnd  35506  prdsbnd  35511  bfplem2  35541  bfp  35542  renegclALT  36539  2xp3dxp2ge1d  39684  factwoffsmonot  39685  0cnALT3  39792  sn-1ne2  39797  oexpreposd  39823  sn-00idlem2  39879  sn-00idlem3  39880  sn-00id  39881  rei4  39902  sn-0tie0  39918  sn-ltaddpos  39920  relt0neg1  39922  sn-0lt1  39929  sn-inelr  39932  itrere  39933  retire  39934  pellexlem6  40148  elpell14qr2  40176  oddcomabszz  40258  zindbi  40260  jm2.24  40277  acongeq  40297  arearect  40538  areaquad  40539  reabsifneg  40705  reabsifnpos  40706  reabsifpos  40707  reabsifnneg  40708  imsqrtvalex  40719  relexp01min  40787  imo72b2lem0  41242  imo72b2lem2  41244  imo72b2lem1  41247  imo72b2  41251  dvconstbi  41411  binomcxplemnn0  41426  binomcxplemdvbinom  41430  binomcxplemcvg  41431  binomcxplemnotnn0  41433  sineq0ALT  42016  halffl  42296  ren0  42405  sqrlearg  42556  limsup10ex  42781  dvnmptdivc  42946  dvnmul  42951  itgsin0pilem1  42958  itgsinexplem1  42962  itgsinexp  42963  iblempty  42973  stoweidlem17  43025  stoweidlem36  43044  stoweidlem55  43063  wallispilem1  43073  wallispilem2  43074  wallispilem4  43076  stirlinglem4  43085  stirlinglem13  43094  stirlinglem14  43095  stirlinglem15  43096  stirlingr  43098  dirker2re  43100  dirkerdenne0  43101  dirkerre  43103  dirkertrigeqlem1  43106  dirkercncflem2  43112  dirkercncflem4  43114  fourierdlem11  43126  fourierdlem16  43131  fourierdlem21  43136  fourierdlem22  43137  fourierdlem41  43156  fourierdlem42  43157  fourierdlem48  43162  fourierdlem62  43176  fourierdlem66  43180  fourierdlem79  43193  fourierdlem83  43197  fourierdlem94  43208  fourierdlem102  43216  fourierdlem103  43217  fourierdlem104  43218  fourierdlem111  43225  fourierdlem112  43226  fourierdlem113  43227  fourierdlem114  43228  sqwvfoura  43236  sqwvfourb  43237  fourierswlem  43238  fouriersw  43239  etransclem23  43265  etransclem44  43286  etransclem46  43288  salexct3  43348  salgensscntex  43350  sge0rnn0  43373  sge00  43381  0ome  43534  ovn0lem  43570  ovnhoilem1  43606  smfmullem1  43789  smfmullem2  43790  smfmullem3  43791  smfmullem4  43792  zm1nn  44227  sqrtnegnre  44232  m1mod0mod1  44254  fmtnoprmfac2lem1  44451  31prm  44482  mod42tp1mod8  44487  nfermltl2rev  44628  tgblthelfgott  44700  altgsumbcALT  45122  expnegico01  45292  dignnld  45382  eenglngeehlnmlem1  45516  line2ylem  45530  line2y  45534  itsclc0yqsollem2  45542  ex-gt  45645