MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0re Structured version   Visualization version   GIF version

Theorem 0re 10632
Description: The number 0 is real. Remark: the first step could also be ax-icn 10585. See also 0reALT 10972. (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.
StepHypRef Expression
1 ax-1cn 10584 . 2 1 ∈ ℂ
2 cnre 10627 . 2 (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3 ax-rnegex 10597 . . . . 5 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4 readdcl 10609 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5 eleq1 2900 . . . . . . 7 ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 246 . . . . . 6 ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
76rexlimdva 3284 . . . . 5 (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
83, 7mpd 15 . . . 4 (𝑥 ∈ ℝ → 0 ∈ ℝ)
98adantr 481 . . 3 ((𝑥 ∈ ℝ ∧ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦))) → 0 ∈ ℝ)
109rexlimiva 3281 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)) → 0 ∈ ℝ)
111, 2, 10mp2b 10 1 0 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1528  wcel 2105  wrex 3139  (class class class)co 7145  cc 10524  cr 10525  0cc0 10526  1c1 10527  ici 10528   + caddc 10529   · cmul 10531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793  ax-1cn 10584  ax-addrcl 10587  ax-rnegex 10597  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144
This theorem is referenced by:  0red  10633  0xr  10677  axmulgt0  10704  ne0gt0  10734  00id  10804  mul02lem1  10805  mul02lem2  10806  mul02  10807  addid1  10809  ltaddneg  10844  addgt0  11115  addgegt0  11116  addgtge0  11117  addge0  11118  ltaddpos  11119  ltneg  11129  leneg  11132  lt0neg1  11135  lt0neg2  11136  le0neg1  11137  le0neg2  11138  addge01  11139  suble0  11143  mulge0  11147  msqge0  11150  0le1  11152  relin01  11153  gt0ne0i  11164  gt0ne0d  11193  lt0ne0d  11194  elimge0  11468  ltm1  11471  recgt0  11475  prodgt0  11476  lemul1a  11483  ltmul12a  11485  lemul12a  11487  mulgt1  11488  gt0div  11495  ge0div  11496  mulge0b  11499  lediv12a  11522  recgt1i  11526  recreclt  11528  ledivp1  11531  squeeze0  11532  recgt0ii  11535  ledivp1i  11554  ltdivp1i  11555  fimaxre2  11575  inelr  11617  crne0  11620  nnge1  11654  nngt0  11657  nnnle0  11659  nnne0  11660  nnrecgt0  11669  0le0  11727  neg1lt0  11743  halfge0  11843  nn0ssre  11890  nn0ge0  11911  nn0nlt0  11912  nn0le0eq0  11914  0mnnnnn0  11918  elnnnn0b  11930  elnnnn0c  11931  nn0sub  11936  elnnz  11980  0z  11981  elnn0z  11983  elnnz1  11997  recnz  12046  gtndiv  12048  fnn0ind  12070  10re  12106  rpge0  12392  rpneg  12411  0nrp  12414  0ltpnf  12507  mnflt0  12510  qsqueeze  12584  xneg0  12595  xaddid1  12624  xnn0xadd0  12630  xmulpnf1  12657  xlemul1a  12671  xadddi  12678  xrsupsslem  12690  xrinfmsslem  12691  elrege0  12832  0e0icopnf  12836  elicc01  12844  0elunit  12845  unitssre  12875  0nelfz1  12916  fzpreddisj  12946  fz0to4untppr  13000  nn0p1elfzo  13070  ico01fl0  13179  rpsup  13224  modelico  13239  0mod  13260  1mod  13261  le2sq2  13490  expubnd  13531  sqlecan  13561  bernneq2  13581  expnbnd  13583  expnlbnd  13584  expmulnbnd  13586  discr1  13590  discr  13591  faclbnd  13640  faclbnd3  13642  faclbnd6  13649  bcval4  13657  bcval5  13668  bcpasc  13671  hasheq0  13714  hashneq0  13715  hashnn0n0nn  13742  hashgt12el  13773  hashgt12el2  13774  hashge2el2dif  13828  lsw0  13907  swrdccatin2  14081  pfxccatin12lem3  14084  reim0  14467  re0  14501  im0  14502  rei  14505  imi  14506  cj0  14507  sqeqd  14515  rennim  14588  cnpart  14589  sqr0lem  14590  sqrlem4  14595  resqrex  14600  sqrtgt0  14608  sqrt00  14613  sqrtneglem  14616  sqrt9  14623  sqrt2gt1lt2  14624  leabs  14649  absor  14650  max0add  14660  eqsqrt2d  14718  sqrtpclii  14732  rlimconst  14891  rlimrege0  14926  lo1mul  14974  iserge0  15007  fsum00  15143  isumless  15190  arisum2  15206  georeclim  15218  geo2sum  15219  geoisumr  15224  0.999...  15227  cvgrat  15229  fprodge0  15337  bpoly4  15403  cos0  15493  ef01bndlem  15527  sin01bnd  15528  cos01bnd  15529  cos2bnd  15531  sin01gt0  15533  cos01gt0  15534  sincos2sgn  15537  sin4lt0  15538  absef  15540  absefib  15541  efieq1re  15542  epos  15550  rpnnen2lem2  15558  rpnnen2lem3  15559  rpnnen2lem4  15560  rpnnen2lem9  15565  ruclem6  15578  dvdslelem  15649  divalglem1  15735  divalglem5  15738  divalglem6  15739  flodddiv4  15754  sadcadd  15797  gcdn0gt0  15856  nn0seqcvgd  15904  algcvgblem  15911  algcvga  15913  pythagtriplem12  16153  pythagtriplem13  16154  pythagtriplem14  16155  pythagtriplem16  16157  prmreclem4  16245  prmreclem5  16246  prmreclem6  16247  1arith  16253  ramz  16351  mulgnegnn  18178  subgmulg  18233  srgbinomlem4  19224  isabvd  19522  abvtrivd  19542  psrbaglesupp  20078  xrs1mnd  20513  xrs10  20514  rge0srg  20546  psgnodpmr  20664  re0g  20686  mnfnei  21759  imasdsf1olem  22912  ssblps  22961  ssbl  22962  xmeter  22972  dscmet  23111  dscopn  23112  nmoi  23266  nmoeq0  23274  0nghm  23279  idnghm  23281  cnbl0  23311  xrsxmet  23346  metdseq0  23391  iicmp  23423  iiconn  23424  iihalf1  23464  iihalf1cn  23465  elii1  23468  icopnfcnv  23475  icopnfhmeo  23476  iccpnfcnv  23477  xrhmeo  23479  xrhmph  23480  htpycc  23513  reparphti  23530  pcoval1  23546  pco0  23547  pcoval2  23549  pcocn  23550  pcohtpylem  23552  pcopt  23555  pcopt2  23556  pcoass  23557  pcorevlem  23559  reust  23913  recusp  23914  rrx0el  23930  minveclem4c  23957  minveclem2  23958  minveclem3b  23960  minveclem4  23964  minveclem7  23967  pjthlem1  23969  cniccbdd  23991  ovolunnul  24030  ovoliunnul  24037  ovolicc1  24046  ovolre  24055  iccvolcl  24097  ovolioo  24098  ioovolcl  24100  ioorcl  24107  vitalilem4  24141  vitalilem5  24142  vitali  24143  ismbf  24158  mbfmulc2lem  24177  mbfpos  24181  mbfposr  24182  i1f0  24217  i1f1  24220  itg1addlem2  24227  itg1addlem4  24229  itg1addlem5  24230  mbfi1fseqlem4  24248  mbfi1fseqlem5  24249  mbfi1flimlem  24252  xrge0f  24261  itg2ge0  24265  itg2const  24270  itg2mulc  24277  itg2splitlem  24278  itg2gt0  24290  itg2cnlem1  24291  ibl0  24316  iblrelem  24320  iblposlem  24321  iblpos  24322  iblre  24323  itgreval  24326  itgneg  24333  iblss  24334  i1fibl  24337  itgitg1  24338  itgle  24339  itgeqa  24343  itgless  24346  iblconst  24347  itgconst  24348  ibladdlem  24349  itgaddlem2  24353  iblabslem  24357  iblabsr  24359  iblmulc2  24360  itgmulc2lem2  24362  itgabs  24364  itgsplit  24365  bddmulibl  24368  dvferm1  24511  dvferm2  24513  dvferm  24514  dvlip  24519  c1lip1  24523  dveq0  24526  dv11cn  24527  dvne0  24537  ftc1lem4  24565  ply1divex  24659  dgrco  24794  plyrecj  24798  vieta1lem2  24829  aalioulem2  24851  aalioulem3  24852  pserulm  24939  psercnlem2  24941  psercnlem1  24942  psercn  24943  abelth  24958  reeff1olem  24963  reeff1o  24964  pilem2  24969  pilem3  24970  pipos  24975  sinhalfpilem  24978  sincosq1sgn  25013  sincosq2sgn  25014  coseq00topi  25017  coseq0negpitopi  25018  tangtx  25020  tanabsge  25021  sinq12ge0  25023  sinq34lt0t  25024  cosq14ge0  25026  sincos4thpi  25028  sincos6thpi  25030  pige3ALT  25034  sineq0  25038  cosordlem  25042  cosord  25043  cos11  25044  sinord  25045  recosf1o  25046  resinf1o  25047  tanord1  25048  tanord  25049  tanregt0  25050  efif1olem4  25056  efifo  25058  relogrn  25072  log1  25096  logneg  25098  argregt0  25120  argrege0  25121  argimgt0  25122  logneg2  25125  logdivlti  25130  logdivlt  25131  ellogdm  25149  logdmn0  25150  logdmnrp  25151  logcnlem3  25154  dvloglem  25158  logdmopn  25159  logf1o2  25160  dvlog2lem  25162  efopnlem1  25166  logtayl  25170  recxpcl  25185  cxpge0  25193  cxple2  25207  cxple2a  25209  cxpsqrtlem  25212  cxpcn3  25256  cxpaddlelem  25259  cxpaddle  25260  loglesqrt  25266  logbrec  25287  ang180lem3  25316  ang180lem4  25317  asinneg  25391  asin1  25399  reasinsin  25401  acosbnd  25405  atan0  25413  atanrecl  25416  atanlogaddlem  25418  atanlogsublem  25420  atanlogsub  25421  atantan  25428  atanbnd  25431  atan1  25433  atans2  25436  ressatans  25439  log2cnv  25450  log2tlbnd  25451  log2ub  25455  log2le1  25456  rlimcnp  25471  rlimcnp2  25472  o1cxp  25480  jensen  25494  amgm  25496  emgt0  25512  harmonicbnd3  25513  harmoniclbnd  25514  harmonicbnd4  25516  zetacvg  25520  eldmgm  25527  lgamgulmlem2  25535  basellem3  25588  basellem8  25593  efnnfsumcl  25608  ppisval  25609  vmage0  25626  chpge0  25631  efchtdvds  25664  ppiltx  25682  ppiub  25708  chpeq0  25712  chteq0  25713  chtleppi  25714  chpchtsum  25723  chpub  25724  dchr1re  25767  bcmono  25781  efexple  25785  bposlem1  25788  bposlem4  25791  bposlem5  25792  bposlem7  25794  bposlem8  25795  bposlem9  25796  lgsval2lem  25811  lgsval4a  25823  lgsneg  25825  lgsdilem  25828  lgsdir2lem1  25829  2lgsoddprmlem3a  25914  2lgsoddprmlem3b  25915  2lgsoddprmlem3c  25916  2lgsoddprmlem3d  25917  rplogsumlem2  25989  rpvmasumlem  25991  dchrisum0flblem1  26012  dchrisum0flblem2  26013  dchrisum0fno1  26015  rplogsum  26031  logdivsum  26037  mulog2sumlem2  26039  selberg2lem  26054  logdivbnd  26060  pntrsumo1  26069  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntpbnd1  26090  pntpbnd2  26091  pntlem3  26113  pntleml  26115  ostth2  26141  trgcgrg  26229  ttgcontlem1  26599  axlowdimlem1  26656  axlowdimlem6  26661  axlowdimlem7  26662  axlowdimlem10  26665  axlowdim1  26673  axlowdim2  26674  axlowdim  26675  elntg2  26699  umgrislfupgrlem  26835  lfgrnloop  26838  lfuhgr1v0e  26964  usgrexmplef  26969  pthdlem2  27477  crctcshwlkn0lem7  27522  rusgrnumwwlks  27681  clwwlkn0  27734  konigsberg  27964  ex-po  28142  ex-sqrt  28161  ex-gcd  28164  nvz0  28373  0blo  28497  nmlno0lem  28498  nmblolbii  28504  siilem2  28557  minvecolem2  28580  minvecolem3  28581  minvecolem4c  28584  minvecolem4  28585  minvecolem5  28586  minvecolem7  28588  htthlem  28622  hiidge0  28803  normlem6  28820  normgt0  28832  norm-i  28834  normpyc  28851  bcsiALT  28884  pjhthlem1  29096  pjneli  29428  nmlnop0iALT  29700  unopbd  29720  nmbdoplbi  29729  nmcoplbi  29733  nmbdfnlbi  29754  nmbdfnlb  29755  nmcfnlbi  29757  cnlnadjlem7  29778  nmopcoi  29800  branmfn  29810  leopmul  29839  nmopleid  29844  pjbdlni  29854  pjnormssi  29873  stle0i  29944  cdj3lem1  30139  xaddeq0  30404  pr01ssre  30468  dp20u  30482  dp20h  30483  dp2clq  30485  dp2lt10  30488  dp2lt  30489  dp0u  30505  dplti  30509  dpexpp1  30512  xdiv0  30533  xrge0slmod  30845  unitdivcld  31044  sqsscirc1  31051  xrge0iifcnv  31076  xrge0iifiso  31078  rezh  31112  indf  31174  indfval  31175  esumcvgsum  31247  voliune  31388  volfiniune  31389  sibfinima  31497  sitmcl  31509  0rrv  31609  coinfliprv  31640  ballotlem2  31646  ballotlem4  31656  ballotlemi1  31660  ballotlemic  31664  sgnclre  31697  sgnnbi  31703  sgnpbi  31704  plymulx0  31717  signsply0  31721  signswch  31731  signstf  31736  signstf0  31738  signstfveq0  31747  signlem0  31757  signshf  31758  itgexpif  31777  hgt750lemd  31819  hgt750lem  31822  hgt750lem2  31823  hgt750leme  31829  iisconn  32397  iillysconn  32398  cvmliftlem10  32439  fz0n  32860  logi  32864  bcneg1  32866  nn0prpwlem  33568  dnizeq0  33712  dnizphlfeqhlf  33713  knoppndvlem13  33761  cnndvlem1  33774  bj-pinftyccb  34396  bj-minftyccb  34400  bj-pinftynminfty  34402  bj-isrvec  34464  taupilemrplb  34484  sin2h  34764  tan2h  34766  ptrecube  34774  poimirlem16  34790  poimirlem17  34791  poimirlem20  34794  poimirlem22  34796  poimirlem23  34797  poimirlem29  34803  poimirlem31  34805  poimir  34807  heicant  34809  mblfinlem2  34812  ismblfin  34815  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  mbfposadd  34821  itg2addnclem  34825  itg2addnclem2  34826  ibladdnclem  34830  itgaddnclem2  34833  iblabsnclem  34837  iblmulc2nc  34839  itgmulc2nclem2  34841  itgabsnc  34843  ftc1cnnclem  34847  ftc1anclem5  34853  ftc1anclem8  34856  asindmre  34859  dvasin  34860  areacirclem4  34867  areacirc  34869  isbnd3  34945  ssbnd  34949  prdsbnd  34954  bfplem2  34984  bfp  34985  renegclALT  35981  0cnALT3  39033  sn-1ne2  39038  oexpreposd  39059  sn-00idlem2  39109  sn-00idlem3  39110  sn-00id  39111  sn-ltaddpos  39123  sn-0lt1  39126  pellexlem6  39311  elpell14qr2  39339  oddcomabszz  39421  zindbi  39423  jm2.24  39440  acongeq  39460  arearect  39702  areaquad  39703  relexp01min  39938  imo72b2lem0  40396  imo72b2lem2  40398  imo72b2lem1  40402  imo72b2  40406  dvconstbi  40546  binomcxplemnn0  40561  binomcxplemdvbinom  40565  binomcxplemcvg  40566  binomcxplemnotnn0  40568  sineq0ALT  41151  halffl  41443  ren0  41555  sqrlearg  41709  limsup10ex  41934  liminf10ex  41935  dvnmptdivc  42103  dvnmul  42108  itgsin0pilem1  42115  itgsinexplem1  42119  itgsinexp  42120  iblempty  42130  stoweidlem17  42183  stoweidlem36  42202  stoweidlem55  42221  wallispilem1  42231  wallispilem2  42232  wallispilem4  42234  stirlinglem4  42243  stirlinglem13  42252  stirlinglem14  42253  stirlinglem15  42254  stirlingr  42256  dirker2re  42258  dirkerdenne0  42259  dirkerre  42261  dirkertrigeqlem1  42264  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem11  42284  fourierdlem16  42289  fourierdlem21  42294  fourierdlem22  42295  fourierdlem41  42314  fourierdlem42  42315  fourierdlem48  42320  fourierdlem62  42334  fourierdlem66  42338  fourierdlem79  42351  fourierdlem83  42355  fourierdlem94  42366  fourierdlem102  42374  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fourierdlem112  42384  fourierdlem113  42385  fourierdlem114  42386  sqwvfoura  42394  sqwvfourb  42395  fourierswlem  42396  fouriersw  42397  etransclem23  42423  etransclem44  42444  etransclem46  42446  salexct3  42506  salgensscntex  42508  sge0rnn0  42531  sge00  42539  0ome  42692  ovn0lem  42728  ovnhoilem1  42764  smfmullem1  42947  smfmullem2  42948  smfmullem3  42949  smfmullem4  42950  zm1nn  43383  sqrtnegnre  43388  m1mod0mod1  43410  fmtnoprmfac2lem1  43575  31prm  43607  mod42tp1mod8  43614  nfermltl2rev  43755  tgblthelfgott  43827  altgsumbcALT  44299  expnegico01  44471  dignnld  44561  eenglngeehlnmlem1  44622  line2ylem  44636  line2y  44640  itsclc0yqsollem2  44648  ex-gt  44725
  Copyright terms: Public domain W3C validator