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

Theorem 0re 10637
Description: The number 0 is real. Remark: the first step could also be ax-icn 10590. See also 0reALT 10977. (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 10589 . 2 1 ∈ ℂ
2 cnre 10632 . 2 (1 ∈ ℂ → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 1 = (𝑥 + (i · 𝑦)))
3 ax-rnegex 10602 . . . . 5 (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0)
4 readdcl 10614 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑥 + 𝑧) ∈ ℝ)
5 eleq1 2900 . . . . . . 7 ((𝑥 + 𝑧) = 0 → ((𝑥 + 𝑧) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 247 . . . . . 6 ((𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ) → ((𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
76rexlimdva 3284 . . . . 5 (𝑥 ∈ ℝ → (∃𝑧 ∈ ℝ (𝑥 + 𝑧) = 0 → 0 ∈ ℝ))
83, 7mpd 15 . . . 4 (𝑥 ∈ ℝ → 0 ∈ ℝ)
98adantr 483 . . 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 398   = wceq 1533  wcel 2110  wrex 3139  (class class class)co 7150  cc 10529  cr 10530  0cc0 10531  1c1 10532  ici 10533   + caddc 10534   · cmul 10536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793  ax-1cn 10589  ax-addrcl 10592  ax-rnegex 10602  ax-cnre 10604
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144
This theorem is referenced by:  0red  10638  0xr  10682  axmulgt0  10709  ne0gt0  10739  00id  10809  mul02lem1  10810  mul02lem2  10811  mul02  10812  addid1  10814  ltaddneg  10849  addgt0  11120  addgegt0  11121  addgtge0  11122  addge0  11123  ltaddpos  11124  ltneg  11134  leneg  11137  lt0neg1  11140  lt0neg2  11141  le0neg1  11142  le0neg2  11143  addge01  11144  suble0  11148  mulge0  11152  msqge0  11155  0le1  11157  relin01  11158  gt0ne0i  11169  gt0ne0d  11198  lt0ne0d  11199  elimge0  11473  ltm1  11476  recgt0  11480  prodgt0  11481  lemul1a  11488  ltmul12a  11490  lemul12a  11492  mulgt1  11493  gt0div  11500  ge0div  11501  mulge0b  11504  lediv12a  11527  recgt1i  11531  recreclt  11533  ledivp1  11536  squeeze0  11537  recgt0ii  11540  ledivp1i  11559  ltdivp1i  11560  fimaxre2  11580  inelr  11622  crne0  11625  nnge1  11659  nngt0  11662  nnnle0  11664  nnne0  11665  nnrecgt0  11674  0le0  11732  neg1lt0  11748  halfge0  11848  nn0ssre  11895  nn0ge0  11916  nn0nlt0  11917  nn0le0eq0  11919  0mnnnnn0  11923  elnnnn0b  11935  elnnnn0c  11936  nn0sub  11941  elnnz  11985  0z  11986  elnn0z  11988  elnnz1  12002  recnz  12051  gtndiv  12053  fnn0ind  12075  10re  12111  rpge0  12396  rpneg  12415  0nrp  12418  0ltpnf  12511  mnflt0  12514  qsqueeze  12588  xneg0  12599  xaddid1  12628  xnn0xadd0  12634  xmulpnf1  12661  xlemul1a  12675  xadddi  12682  xrsupsslem  12694  xrinfmsslem  12695  elrege0  12836  0e0icopnf  12840  elicc01  12848  0elunit  12849  unitssre  12879  0nelfz1  12920  fzpreddisj  12950  fz0to4untppr  13004  nn0p1elfzo  13074  ico01fl0  13183  rpsup  13228  modelico  13243  0mod  13264  1mod  13265  le2sq2  13494  expubnd  13535  sqlecan  13565  bernneq2  13585  expnbnd  13587  expnlbnd  13588  expmulnbnd  13590  discr1  13594  discr  13595  faclbnd  13644  faclbnd3  13646  faclbnd6  13653  bcval4  13661  bcval5  13672  bcpasc  13675  hasheq0  13718  hashneq0  13719  hashnn0n0nn  13746  hashgt12el  13777  hashgt12el2  13778  hashge2el2dif  13832  lsw0  13911  swrdccatin2  14085  pfxccatin12lem3  14088  reim0  14471  re0  14505  im0  14506  rei  14509  imi  14510  cj0  14511  sqeqd  14519  rennim  14592  cnpart  14593  sqr0lem  14594  sqrlem4  14599  resqrex  14604  sqrtgt0  14612  sqrt00  14617  sqrtneglem  14620  sqrt9  14627  sqrt2gt1lt2  14628  leabs  14653  absor  14654  max0add  14664  eqsqrt2d  14722  sqrtpclii  14736  rlimconst  14895  rlimrege0  14930  lo1mul  14978  iserge0  15011  fsum00  15147  isumless  15194  arisum2  15210  georeclim  15222  geo2sum  15223  geoisumr  15228  0.999...  15231  cvgrat  15233  fprodge0  15341  bpoly4  15407  cos0  15497  ef01bndlem  15531  sin01bnd  15532  cos01bnd  15533  cos2bnd  15535  sin01gt0  15537  cos01gt0  15538  sincos2sgn  15541  sin4lt0  15542  absef  15544  absefib  15545  efieq1re  15546  epos  15554  rpnnen2lem2  15562  rpnnen2lem3  15563  rpnnen2lem4  15564  rpnnen2lem9  15569  ruclem6  15582  dvdslelem  15653  divalglem1  15739  divalglem5  15742  divalglem6  15743  flodddiv4  15758  sadcadd  15801  gcdn0gt0  15860  nn0seqcvgd  15908  algcvgblem  15915  algcvga  15917  pythagtriplem12  16157  pythagtriplem13  16158  pythagtriplem14  16159  pythagtriplem16  16161  prmreclem4  16249  prmreclem5  16250  prmreclem6  16251  1arith  16257  ramz  16355  mulgnegnn  18232  subgmulg  18287  srgbinomlem4  19287  isabvd  19585  abvtrivd  19605  psrbaglesupp  20142  xrs1mnd  20577  xrs10  20578  rge0srg  20610  psgnodpmr  20728  re0g  20750  mnfnei  21823  imasdsf1olem  22977  ssblps  23026  ssbl  23027  xmeter  23037  dscmet  23176  dscopn  23177  nmoi  23331  nmoeq0  23339  0nghm  23344  idnghm  23346  cnbl0  23376  xrsxmet  23411  metdseq0  23456  iicmp  23488  iiconn  23489  iihalf1  23529  iihalf1cn  23530  elii1  23533  icopnfcnv  23540  icopnfhmeo  23541  iccpnfcnv  23542  xrhmeo  23544  xrhmph  23545  htpycc  23578  reparphti  23595  pcoval1  23611  pco0  23612  pcoval2  23614  pcocn  23615  pcohtpylem  23617  pcopt  23620  pcopt2  23621  pcoass  23622  pcorevlem  23624  reust  23978  recusp  23979  rrx0el  23995  minveclem4c  24022  minveclem2  24023  minveclem3b  24025  minveclem4  24029  minveclem7  24032  pjthlem1  24034  cniccbdd  24056  ovolunnul  24095  ovoliunnul  24102  ovolicc1  24111  ovolre  24120  iccvolcl  24162  ovolioo  24163  ioovolcl  24165  ioorcl  24172  vitalilem4  24206  vitalilem5  24207  vitali  24208  ismbf  24223  mbfmulc2lem  24242  mbfpos  24246  mbfposr  24247  i1f0  24282  i1f1  24285  itg1addlem2  24292  itg1addlem4  24294  itg1addlem5  24295  mbfi1fseqlem4  24313  mbfi1fseqlem5  24314  mbfi1flimlem  24317  xrge0f  24326  itg2ge0  24330  itg2const  24335  itg2mulc  24342  itg2splitlem  24343  itg2gt0  24355  itg2cnlem1  24356  ibl0  24381  iblrelem  24385  iblposlem  24386  iblpos  24387  iblre  24388  itgreval  24391  itgneg  24398  iblss  24399  i1fibl  24402  itgitg1  24403  itgle  24404  itgeqa  24408  itgless  24411  iblconst  24412  itgconst  24413  ibladdlem  24414  itgaddlem2  24418  iblabslem  24422  iblabsr  24424  iblmulc2  24425  itgmulc2lem2  24427  itgabs  24429  itgsplit  24430  bddmulibl  24433  dvferm1  24576  dvferm2  24578  dvferm  24579  dvlip  24584  c1lip1  24588  dveq0  24591  dv11cn  24592  dvne0  24602  ftc1lem4  24630  ply1divex  24724  dgrco  24859  plyrecj  24863  vieta1lem2  24894  aalioulem2  24916  aalioulem3  24917  pserulm  25004  psercnlem2  25006  psercnlem1  25007  psercn  25008  abelth  25023  reeff1olem  25028  reeff1o  25029  pilem2  25034  pilem3  25035  pipos  25040  sinhalfpilem  25043  sincosq1sgn  25078  sincosq2sgn  25079  coseq00topi  25082  coseq0negpitopi  25083  tangtx  25085  tanabsge  25086  sinq12ge0  25088  sinq34lt0t  25089  cosq14ge0  25091  sincos4thpi  25093  sincos6thpi  25095  pige3ALT  25099  sineq0  25103  cosordlem  25109  cosord  25110  cos11  25111  sinord  25112  recosf1o  25113  resinf1o  25114  tanord1  25115  tanord  25116  tanregt0  25117  efif1olem4  25123  efifo  25125  relogrn  25139  log1  25163  logneg  25165  argregt0  25187  argrege0  25188  argimgt0  25189  logneg2  25192  logdivlti  25197  logdivlt  25198  ellogdm  25216  logdmn0  25217  logdmnrp  25218  logcnlem3  25221  dvloglem  25225  logdmopn  25226  logf1o2  25227  dvlog2lem  25229  efopnlem1  25233  logtayl  25237  recxpcl  25252  cxpge0  25260  cxple2  25274  cxple2a  25276  cxpsqrtlem  25279  cxpcn3  25323  cxpaddlelem  25326  cxpaddle  25327  loglesqrt  25333  logbrec  25354  ang180lem3  25383  ang180lem4  25384  asinneg  25458  asin1  25466  reasinsin  25468  acosbnd  25472  atan0  25480  atanrecl  25483  atanlogaddlem  25485  atanlogsublem  25487  atanlogsub  25488  atantan  25495  atanbnd  25498  atan1  25500  atans2  25503  ressatans  25506  log2cnv  25516  log2tlbnd  25517  log2ub  25521  log2le1  25522  rlimcnp  25537  rlimcnp2  25538  o1cxp  25546  jensen  25560  amgm  25562  emgt0  25578  harmonicbnd3  25579  harmoniclbnd  25580  harmonicbnd4  25582  zetacvg  25586  eldmgm  25593  lgamgulmlem2  25601  basellem3  25654  basellem8  25659  efnnfsumcl  25674  ppisval  25675  vmage0  25692  chpge0  25697  efchtdvds  25730  ppiltx  25748  ppiub  25774  chpeq0  25778  chteq0  25779  chtleppi  25780  chpchtsum  25789  chpub  25790  dchr1re  25833  bcmono  25847  efexple  25851  bposlem1  25854  bposlem4  25857  bposlem5  25858  bposlem7  25860  bposlem8  25861  bposlem9  25862  lgsval2lem  25877  lgsval4a  25889  lgsneg  25891  lgsdilem  25894  lgsdir2lem1  25895  2lgsoddprmlem3a  25980  2lgsoddprmlem3b  25981  2lgsoddprmlem3c  25982  2lgsoddprmlem3d  25983  rplogsumlem2  26055  rpvmasumlem  26057  dchrisum0flblem1  26078  dchrisum0flblem2  26079  dchrisum0fno1  26081  rplogsum  26097  logdivsum  26103  mulog2sumlem2  26105  selberg2lem  26120  logdivbnd  26126  pntrsumo1  26135  pntrlog2bndlem4  26150  pntrlog2bndlem5  26151  pntpbnd1  26156  pntpbnd2  26157  pntlem3  26179  pntleml  26181  ostth2  26207  trgcgrg  26295  ttgcontlem1  26665  axlowdimlem1  26722  axlowdimlem6  26727  axlowdimlem7  26728  axlowdimlem10  26731  axlowdim1  26739  axlowdim2  26740  axlowdim  26741  elntg2  26765  umgrislfupgrlem  26901  lfgrnloop  26904  lfuhgr1v0e  27030  usgrexmplef  27035  pthdlem2  27543  crctcshwlkn0lem7  27588  rusgrnumwwlks  27747  clwwlkn0  27800  konigsberg  28030  ex-po  28208  ex-sqrt  28227  ex-gcd  28230  nvz0  28439  0blo  28563  nmlno0lem  28564  nmblolbii  28570  siilem2  28623  minvecolem2  28646  minvecolem3  28647  minvecolem4c  28650  minvecolem4  28651  minvecolem5  28652  minvecolem7  28654  htthlem  28688  hiidge0  28869  normlem6  28886  normgt0  28898  norm-i  28900  normpyc  28917  bcsiALT  28950  pjhthlem1  29162  pjneli  29494  nmlnop0iALT  29766  unopbd  29786  nmbdoplbi  29795  nmcoplbi  29799  nmbdfnlbi  29820  nmbdfnlb  29821  nmcfnlbi  29823  cnlnadjlem7  29844  nmopcoi  29866  branmfn  29876  leopmul  29905  nmopleid  29910  pjbdlni  29920  pjnormssi  29939  stle0i  30010  cdj3lem1  30205  xaddeq0  30471  pr01ssre  30535  dp20u  30549  dp20h  30550  dp2clq  30552  dp2lt10  30555  dp2lt  30556  dp0u  30572  dplti  30576  dpexpp1  30579  xdiv0  30600  xrge0slmod  30912  unitdivcld  31139  sqsscirc1  31146  xrge0iifcnv  31171  xrge0iifiso  31173  rezh  31207  indf  31269  indfval  31270  esumcvgsum  31342  voliune  31483  volfiniune  31484  sibfinima  31592  sitmcl  31604  0rrv  31704  coinfliprv  31735  ballotlem2  31741  ballotlem4  31751  ballotlemi1  31755  ballotlemic  31759  sgnclre  31792  sgnnbi  31798  sgnpbi  31799  plymulx0  31812  signsply0  31816  signswch  31826  signstf  31831  signstf0  31833  signstfveq0  31842  signlem0  31852  signshf  31853  itgexpif  31872  hgt750lemd  31914  hgt750lem  31917  hgt750lem2  31918  hgt750leme  31924  iisconn  32494  iillysconn  32495  cvmliftlem10  32536  fz0n  32957  logi  32961  bcneg1  32963  nn0prpwlem  33665  dnizeq0  33809  dnizphlfeqhlf  33810  knoppndvlem13  33858  cnndvlem1  33871  bj-pinftyccb  34497  bj-minftyccb  34501  bj-pinftynminfty  34503  bj-isrvec  34569  taupilemrplb  34595  sin2h  34876  tan2h  34878  ptrecube  34886  poimirlem16  34902  poimirlem17  34903  poimirlem20  34906  poimirlem22  34908  poimirlem23  34909  poimirlem29  34915  poimirlem31  34917  poimir  34919  heicant  34921  mblfinlem2  34924  ismblfin  34927  ovoliunnfl  34928  voliunnfl  34930  volsupnfl  34931  mbfposadd  34933  itg2addnclem  34937  itg2addnclem2  34938  ibladdnclem  34942  itgaddnclem2  34945  iblabsnclem  34949  iblmulc2nc  34951  itgmulc2nclem2  34953  itgabsnc  34955  ftc1cnnclem  34959  ftc1anclem5  34965  ftc1anclem8  34968  asindmre  34971  dvasin  34972  areacirclem4  34979  areacirc  34981  isbnd3  35056  ssbnd  35060  prdsbnd  35065  bfplem2  35095  bfp  35096  renegclALT  36093  0cnALT3  39146  sn-1ne2  39151  oexpreposd  39172  sn-00idlem2  39222  sn-00idlem3  39223  sn-00id  39224  sn-ltaddpos  39236  sn-0lt1  39239  pellexlem6  39424  elpell14qr2  39452  oddcomabszz  39534  zindbi  39536  jm2.24  39553  acongeq  39573  arearect  39815  areaquad  39816  relexp01min  40051  imo72b2lem0  40509  imo72b2lem2  40511  imo72b2lem1  40514  imo72b2  40518  dvconstbi  40659  binomcxplemnn0  40674  binomcxplemdvbinom  40678  binomcxplemcvg  40679  binomcxplemnotnn0  40681  sineq0ALT  41264  halffl  41556  ren0  41668  sqrlearg  41822  limsup10ex  42047  dvnmptdivc  42216  dvnmul  42221  itgsin0pilem1  42228  itgsinexplem1  42232  itgsinexp  42233  iblempty  42243  stoweidlem17  42296  stoweidlem36  42315  stoweidlem55  42334  wallispilem1  42344  wallispilem2  42345  wallispilem4  42347  stirlinglem4  42356  stirlinglem13  42365  stirlinglem14  42366  stirlinglem15  42367  stirlingr  42369  dirker2re  42371  dirkerdenne0  42372  dirkerre  42374  dirkertrigeqlem1  42377  dirkercncflem2  42383  dirkercncflem4  42385  fourierdlem11  42397  fourierdlem16  42402  fourierdlem21  42407  fourierdlem22  42408  fourierdlem41  42427  fourierdlem42  42428  fourierdlem48  42433  fourierdlem62  42447  fourierdlem66  42451  fourierdlem79  42464  fourierdlem83  42468  fourierdlem94  42479  fourierdlem102  42487  fourierdlem103  42488  fourierdlem104  42489  fourierdlem111  42496  fourierdlem112  42497  fourierdlem113  42498  fourierdlem114  42499  sqwvfoura  42507  sqwvfourb  42508  fourierswlem  42509  fouriersw  42510  etransclem23  42536  etransclem44  42557  etransclem46  42559  salexct3  42619  salgensscntex  42621  sge0rnn0  42644  sge00  42652  0ome  42805  ovn0lem  42841  ovnhoilem1  42877  smfmullem1  43060  smfmullem2  43061  smfmullem3  43062  smfmullem4  43063  zm1nn  43496  sqrtnegnre  43501  m1mod0mod1  43523  fmtnoprmfac2lem1  43722  31prm  43754  mod42tp1mod8  43761  nfermltl2rev  43902  tgblthelfgott  43974  altgsumbcALT  44395  expnegico01  44567  dignnld  44657  eenglngeehlnmlem1  44718  line2ylem  44732  line2y  44736  itsclc0yqsollem2  44744  ex-gt  44821
  Copyright terms: Public domain W3C validator