Theorem 0re 10643

Description: The number 0 is real. Remark: the first step could also be ax-icn 10596. See also 0reALT 10983. (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 10595	. 2 ⊢ 1 ∈ ℂ
2		cnre 10638	. 2 ⊢ (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3		ax-rnegex 10608	. . . . 5 ⊢ (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4		readdcl 10620	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5		eleq1 2900	. . . . . . 7 ⊢ ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 247	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
7	6	rexlimdva 3284	. . . . 5 ⊢ (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
8	3, 7	mpd 15	. . . 4 ⊢ (𝑥 ∈ ℝ → 0 ∈ ℝ)
9	8	adantr 483	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
10	9	rexlimiva 3281	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
11	1, 2, 10	mp2b 10	1 ⊢ 0 ∈ ℝ

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃wrex 3139  (class class class)co 7156  ℂcc 10535  ℝcr 10536  0cc0 10537  1c1 10538  ici 10539   + caddc 10540   · cmul 10542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793  ax-1cn 10595  ax-addrcl 10598  ax-rnegex 10608  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144

This theorem is referenced by:  0red  10644  0xr  10688  axmulgt0  10715  ne0gt0  10745  00id  10815  mul02lem1  10816  mul02lem2  10817  mul02  10818  addid1  10820  ltaddneg  10855  addgt0  11126  addgegt0  11127  addgtge0  11128  addge0  11129  ltaddpos  11130  ltneg  11140  leneg  11143  lt0neg1  11146  lt0neg2  11147  le0neg1  11148  le0neg2  11149  addge01  11150  suble0  11154  mulge0  11158  msqge0  11161  0le1  11163  relin01  11164  gt0ne0i  11175  gt0ne0d  11204  lt0ne0d  11205  elimge0  11479  ltm1  11482  recgt0  11486  prodgt0  11487  lemul1a  11494  ltmul12a  11496  lemul12a  11498  mulgt1  11499  gt0div  11506  ge0div  11507  mulge0b  11510  lediv12a  11533  recgt1i  11537  recreclt  11539  ledivp1  11542  squeeze0  11543  recgt0ii  11546  ledivp1i  11565  ltdivp1i  11566  fimaxre2  11586  inelr  11628  crne0  11631  nnge1  11666  nngt0  11669  nnnle0  11671  nnne0  11672  nnrecgt0  11681  0le0  11739  neg1lt0  11755  halfge0  11855  nn0ssre  11902  nn0ge0  11923  nn0nlt0  11924  nn0le0eq0  11926  0mnnnnn0  11930  elnnnn0b  11942  elnnnn0c  11943  nn0sub  11948  elnnz  11992  0z  11993  elnn0z  11995  elnnz1  12009  recnz  12058  gtndiv  12060  fnn0ind  12082  10re  12118  rpge0  12403  rpneg  12422  0nrp  12425  0ltpnf  12518  mnflt0  12521  qsqueeze  12595  xneg0  12606  xaddid1  12635  xnn0xadd0  12641  xmulpnf1  12668  xlemul1a  12682  xadddi  12689  xrsupsslem  12701  xrinfmsslem  12702  elrege0  12843  0e0icopnf  12847  elicc01  12855  0elunit  12856  unitssre  12886  0nelfz1  12927  fzpreddisj  12957  fz0to4untppr  13011  nn0p1elfzo  13081  ico01fl0  13190  rpsup  13235  modelico  13250  0mod  13271  1mod  13272  le2sq2  13501  expubnd  13542  sqlecan  13572  bernneq2  13592  expnbnd  13594  expnlbnd  13595  expmulnbnd  13597  discr1  13601  discr  13602  faclbnd  13651  faclbnd3  13653  faclbnd6  13660  bcval4  13668  bcval5  13679  bcpasc  13682  hasheq0  13725  hashneq0  13726  hashnn0n0nn  13753  hashgt12el  13784  hashgt12el2  13785  hashge2el2dif  13839  lsw0  13917  swrdccatin2  14091  pfxccatin12lem3  14094  reim0  14477  re0  14511  im0  14512  rei  14515  imi  14516  cj0  14517  sqeqd  14525  rennim  14598  cnpart  14599  sqr0lem  14600  sqrlem4  14605  resqrex  14610  sqrtgt0  14618  sqrt00  14623  sqrtneglem  14626  sqrt9  14633  sqrt2gt1lt2  14634  leabs  14659  absor  14660  max0add  14670  eqsqrt2d  14728  sqrtpclii  14742  rlimconst  14901  rlimrege0  14936  lo1mul  14984  iserge0  15017  fsum00  15153  isumless  15200  arisum2  15216  georeclim  15228  geo2sum  15229  geoisumr  15234  0.999...  15237  cvgrat  15239  fprodge0  15347  bpoly4  15413  cos0  15503  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  cos2bnd  15541  sin01gt0  15543  cos01gt0  15544  sincos2sgn  15547  sin4lt0  15548  absef  15550  absefib  15551  efieq1re  15552  epos  15560  rpnnen2lem2  15568  rpnnen2lem3  15569  rpnnen2lem4  15570  rpnnen2lem9  15575  ruclem6  15588  dvdslelem  15659  divalglem1  15745  divalglem5  15748  divalglem6  15749  flodddiv4  15764  sadcadd  15807  gcdn0gt0  15866  nn0seqcvgd  15914  algcvgblem  15921  algcvga  15923  pythagtriplem12  16163  pythagtriplem13  16164  pythagtriplem14  16165  pythagtriplem16  16167  prmreclem4  16255  prmreclem5  16256  prmreclem6  16257  1arith  16263  ramz  16361  mulgnegnn  18238  subgmulg  18293  srgbinomlem4  19293  isabvd  19591  abvtrivd  19611  psrbaglesupp  20148  xrs1mnd  20583  xrs10  20584  rge0srg  20616  psgnodpmr  20734  re0g  20756  mnfnei  21829  imasdsf1olem  22983  ssblps  23032  ssbl  23033  xmeter  23043  dscmet  23182  dscopn  23183  nmoi  23337  nmoeq0  23345  0nghm  23350  idnghm  23352  cnbl0  23382  xrsxmet  23417  metdseq0  23462  iicmp  23494  iiconn  23495  iihalf1  23535  iihalf1cn  23536  elii1  23539  icopnfcnv  23546  icopnfhmeo  23547  iccpnfcnv  23548  xrhmeo  23550  xrhmph  23551  htpycc  23584  reparphti  23601  pcoval1  23617  pco0  23618  pcoval2  23620  pcocn  23621  pcohtpylem  23623  pcopt  23626  pcopt2  23627  pcoass  23628  pcorevlem  23630  reust  23984  recusp  23985  rrx0el  24001  minveclem4c  24028  minveclem2  24029  minveclem3b  24031  minveclem4  24035  minveclem7  24038  pjthlem1  24040  cniccbdd  24062  ovolunnul  24101  ovoliunnul  24108  ovolicc1  24117  ovolre  24126  iccvolcl  24168  ovolioo  24169  ioovolcl  24171  ioorcl  24178  vitalilem4  24212  vitalilem5  24213  vitali  24214  ismbf  24229  mbfmulc2lem  24248  mbfpos  24252  mbfposr  24253  i1f0  24288  i1f1  24291  itg1addlem2  24298  itg1addlem4  24300  itg1addlem5  24301  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1flimlem  24323  xrge0f  24332  itg2ge0  24336  itg2const  24341  itg2mulc  24348  itg2splitlem  24349  itg2gt0  24361  itg2cnlem1  24362  ibl0  24387  iblrelem  24391  iblposlem  24392  iblpos  24393  iblre  24394  itgreval  24397  itgneg  24404  iblss  24405  i1fibl  24408  itgitg1  24409  itgle  24410  itgeqa  24414  itgless  24417  iblconst  24418  itgconst  24419  ibladdlem  24420  itgaddlem2  24424  iblabslem  24428  iblabsr  24430  iblmulc2  24431  itgmulc2lem2  24433  itgabs  24435  itgsplit  24436  bddmulibl  24439  dvferm1  24582  dvferm2  24584  dvferm  24585  dvlip  24590  c1lip1  24594  dveq0  24597  dv11cn  24598  dvne0  24608  ftc1lem4  24636  ply1divex  24730  dgrco  24865  plyrecj  24869  vieta1lem2  24900  aalioulem2  24922  aalioulem3  24923  pserulm  25010  psercnlem2  25012  psercnlem1  25013  psercn  25014  abelth  25029  reeff1olem  25034  reeff1o  25035  pilem2  25040  pilem3  25041  pipos  25046  sinhalfpilem  25049  sincosq1sgn  25084  sincosq2sgn  25085  coseq00topi  25088  coseq0negpitopi  25089  tangtx  25091  tanabsge  25092  sinq12ge0  25094  sinq34lt0t  25095  cosq14ge0  25097  sincos4thpi  25099  sincos6thpi  25101  pige3ALT  25105  sineq0  25109  cosordlem  25115  cosord  25116  cos11  25117  sinord  25118  recosf1o  25119  resinf1o  25120  tanord1  25121  tanord  25122  tanregt0  25123  efif1olem4  25129  efifo  25131  relogrn  25145  log1  25169  logneg  25171  argregt0  25193  argrege0  25194  argimgt0  25195  logneg2  25198  logdivlti  25203  logdivlt  25204  ellogdm  25222  logdmn0  25223  logdmnrp  25224  logcnlem3  25227  dvloglem  25231  logdmopn  25232  logf1o2  25233  dvlog2lem  25235  efopnlem1  25239  logtayl  25243  recxpcl  25258  cxpge0  25266  cxple2  25280  cxple2a  25282  cxpsqrtlem  25285  cxpcn3  25329  cxpaddlelem  25332  cxpaddle  25333  loglesqrt  25339  logbrec  25360  ang180lem3  25389  ang180lem4  25390  asinneg  25464  asin1  25472  reasinsin  25474  acosbnd  25478  atan0  25486  atanrecl  25489  atanlogaddlem  25491  atanlogsublem  25493  atanlogsub  25494  atantan  25501  atanbnd  25504  atan1  25506  atans2  25509  ressatans  25512  log2cnv  25522  log2tlbnd  25523  log2ub  25527  log2le1  25528  rlimcnp  25543  rlimcnp2  25544  o1cxp  25552  jensen  25566  amgm  25568  emgt0  25584  harmonicbnd3  25585  harmoniclbnd  25586  harmonicbnd4  25588  zetacvg  25592  eldmgm  25599  lgamgulmlem2  25607  basellem3  25660  basellem8  25665  efnnfsumcl  25680  ppisval  25681  vmage0  25698  chpge0  25703  efchtdvds  25736  ppiltx  25754  ppiub  25780  chpeq0  25784  chteq0  25785  chtleppi  25786  chpchtsum  25795  chpub  25796  dchr1re  25839  bcmono  25853  efexple  25857  bposlem1  25860  bposlem4  25863  bposlem5  25864  bposlem7  25866  bposlem8  25867  bposlem9  25868  lgsval2lem  25883  lgsval4a  25895  lgsneg  25897  lgsdilem  25900  lgsdir2lem1  25901  2lgsoddprmlem3a  25986  2lgsoddprmlem3b  25987  2lgsoddprmlem3c  25988  2lgsoddprmlem3d  25989  rplogsumlem2  26061  rpvmasumlem  26063  dchrisum0flblem1  26084  dchrisum0flblem2  26085  dchrisum0fno1  26087  rplogsum  26103  logdivsum  26109  mulog2sumlem2  26111  selberg2lem  26126  logdivbnd  26132  pntrsumo1  26141  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntpbnd1  26162  pntpbnd2  26163  pntlem3  26185  pntleml  26187  ostth2  26213  trgcgrg  26301  ttgcontlem1  26671  axlowdimlem1  26728  axlowdimlem6  26733  axlowdimlem7  26734  axlowdimlem10  26737  axlowdim1  26745  axlowdim2  26746  axlowdim  26747  elntg2  26771  umgrislfupgrlem  26907  lfgrnloop  26910  lfuhgr1v0e  27036  usgrexmplef  27041  pthdlem2  27549  crctcshwlkn0lem7  27594  rusgrnumwwlks  27753  clwwlkn0  27806  konigsberg  28036  ex-po  28214  ex-sqrt  28233  ex-gcd  28236  nvz0  28445  0blo  28569  nmlno0lem  28570  nmblolbii  28576  siilem2  28629  minvecolem2  28652  minvecolem3  28653  minvecolem4c  28656  minvecolem4  28657  minvecolem5  28658  minvecolem7  28660  htthlem  28694  hiidge0  28875  normlem6  28892  normgt0  28904  norm-i  28906  normpyc  28923  bcsiALT  28956  pjhthlem1  29168  pjneli  29500  nmlnop0iALT  29772  unopbd  29792  nmbdoplbi  29801  nmcoplbi  29805  nmbdfnlbi  29826  nmbdfnlb  29827  nmcfnlbi  29829  cnlnadjlem7  29850  nmopcoi  29872  branmfn  29882  leopmul  29911  nmopleid  29916  pjbdlni  29926  pjnormssi  29945  stle0i  30016  cdj3lem1  30211  xaddeq0  30477  pr01ssre  30540  dp20u  30554  dp20h  30555  dp2clq  30557  dp2lt10  30560  dp2lt  30561  dp0u  30577  dplti  30581  dpexpp1  30584  xdiv0  30605  xrge0slmod  30917  unitdivcld  31144  sqsscirc1  31151  xrge0iifcnv  31176  xrge0iifiso  31178  rezh  31212  indf  31274  indfval  31275  esumcvgsum  31347  voliune  31488  volfiniune  31489  sibfinima  31597  sitmcl  31609  0rrv  31709  coinfliprv  31740  ballotlem2  31746  ballotlem4  31756  ballotlemi1  31760  ballotlemic  31764  sgnclre  31797  sgnnbi  31803  sgnpbi  31804  plymulx0  31817  signsply0  31821  signswch  31831  signstf  31836  signstf0  31838  signstfveq0  31847  signlem0  31857  signshf  31858  itgexpif  31877  hgt750lemd  31919  hgt750lem  31922  hgt750lem2  31923  hgt750leme  31929  iisconn  32499  iillysconn  32500  cvmliftlem10  32541  fz0n  32962  logi  32966  bcneg1  32968  nn0prpwlem  33670  dnizeq0  33814  dnizphlfeqhlf  33815  knoppndvlem13  33863  cnndvlem1  33876  bj-pinftyccb  34506  bj-minftyccb  34510  bj-pinftynminfty  34512  bj-isrvec  34578  taupilemrplb  34604  sin2h  34897  tan2h  34899  ptrecube  34907  poimirlem16  34923  poimirlem17  34924  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem29  34936  poimirlem31  34938  poimir  34940  heicant  34942  mblfinlem2  34945  ismblfin  34948  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  mbfposadd  34954  itg2addnclem  34958  itg2addnclem2  34959  ibladdnclem  34963  itgaddnclem2  34966  iblabsnclem  34970  iblmulc2nc  34972  itgmulc2nclem2  34974  itgabsnc  34976  ftc1cnnclem  34980  ftc1anclem5  34986  ftc1anclem8  34989  asindmre  34992  dvasin  34993  areacirclem4  35000  areacirc  35002  isbnd3  35077  ssbnd  35081  prdsbnd  35086  bfplem2  35116  bfp  35117  renegclALT  36114  2xp3dxp2ge1d  39117  factwoffsmonot  39118  0cnALT3  39173  sn-1ne2  39178  oexpreposd  39199  sn-00idlem2  39249  sn-00idlem3  39250  sn-00id  39251  sn-ltaddpos  39263  sn-0lt1  39266  pellexlem6  39451  elpell14qr2  39479  oddcomabszz  39561  zindbi  39563  jm2.24  39580  acongeq  39600  arearect  39842  areaquad  39843  relexp01min  40078  imo72b2lem0  40536  imo72b2lem2  40538  imo72b2lem1  40541  imo72b2  40545  dvconstbi  40686  binomcxplemnn0  40701  binomcxplemdvbinom  40705  binomcxplemcvg  40706  binomcxplemnotnn0  40708  sineq0ALT  41291  halffl  41583  ren0  41695  sqrlearg  41849  limsup10ex  42074  dvnmptdivc  42243  dvnmul  42248  itgsin0pilem1  42255  itgsinexplem1  42259  itgsinexp  42260  iblempty  42270  stoweidlem17  42322  stoweidlem36  42341  stoweidlem55  42360  wallispilem1  42370  wallispilem2  42371  wallispilem4  42373  stirlinglem4  42382  stirlinglem13  42391  stirlinglem14  42392  stirlinglem15  42393  stirlingr  42395  dirker2re  42397  dirkerdenne0  42398  dirkerre  42400  dirkertrigeqlem1  42403  dirkercncflem2  42409  dirkercncflem4  42411  fourierdlem11  42423  fourierdlem16  42428  fourierdlem21  42433  fourierdlem22  42434  fourierdlem41  42453  fourierdlem42  42454  fourierdlem48  42459  fourierdlem62  42473  fourierdlem66  42477  fourierdlem79  42490  fourierdlem83  42494  fourierdlem94  42505  fourierdlem102  42513  fourierdlem103  42514  fourierdlem104  42515  fourierdlem111  42522  fourierdlem112  42523  fourierdlem113  42524  fourierdlem114  42525  sqwvfoura  42533  sqwvfourb  42534  fourierswlem  42535  fouriersw  42536  etransclem23  42562  etransclem44  42583  etransclem46  42585  salexct3  42645  salgensscntex  42647  sge0rnn0  42670  sge00  42678  0ome  42831  ovn0lem  42867  ovnhoilem1  42903  smfmullem1  43086  smfmullem2  43087  smfmullem3  43088  smfmullem4  43089  zm1nn  43522  sqrtnegnre  43527  m1mod0mod1  43549  fmtnoprmfac2lem1  43748  31prm  43780  mod42tp1mod8  43787  nfermltl2rev  43928  tgblthelfgott  44000  altgsumbcALT  44421  expnegico01  44593  dignnld  44683  eenglngeehlnmlem1  44744  line2ylem  44758  line2y  44762  itsclc0yqsollem2  44770  ex-gt  44847