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

Theorem 0re 9083
Description:  0 is a real number. See also 0reALT 9389. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
0re  |-  0  e.  RR

Proof of Theorem 0re
StepHypRef Expression
1 1re 9082 . 2  |-  1  e.  RR
2 ax-rnegex 9053 . 2  |-  ( 1  e.  RR  ->  E. x  e.  RR  ( 1  +  x )  =  0 )
3 readdcl 9065 . . . . 5  |-  ( ( 1  e.  RR  /\  x  e.  RR )  ->  ( 1  +  x
)  e.  RR )
41, 3mpan 652 . . . 4  |-  ( x  e.  RR  ->  (
1  +  x )  e.  RR )
5 eleq1 2495 . . . 4  |-  ( ( 1  +  x )  =  0  ->  (
( 1  +  x
)  e.  RR  <->  0  e.  RR ) )
64, 5syl5ibcom 212 . . 3  |-  ( x  e.  RR  ->  (
( 1  +  x
)  =  0  -> 
0  e.  RR ) )
76rexlimiv 2816 . 2  |-  ( E. x  e.  RR  (
1  +  x )  =  0  ->  0  e.  RR )
81, 2, 7mp2b 10 1  |-  0  e.  RR
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725   E.wrex 2698  (class class class)co 6073   RRcr 8981   0cc0 8982   1c1 8983    + caddc 8985
This theorem is referenced by:  0xr  9123  axmulgt0  9142  ne0gt0  9170  00id  9233  mul02lem1  9234  mul02lem2  9235  mul02  9236  addid1  9238  gt0ne0  9485  addgt0  9506  addgegt0  9507  addgtge0  9508  addge0  9509  ltaddpos  9510  ltneg  9520  leneg  9523  lt0neg1  9526  lt0neg2  9527  le0neg1  9528  le0neg2  9529  addge01  9530  add20  9532  subge0  9533  suble0  9534  lesub0  9536  mulge0  9537  msqgt0  9540  msqge0  9541  0le1  9543  gt0ne0i  9554  gt0ne0d  9583  lt0ne0d  9584  addgt0d  9593  elimge0  9839  ltm1  9842  recgt0  9846  prodgt0  9847  prodge0  9849  lemul1a  9856  ltmul12a  9858  lemul12a  9860  mulgt1  9861  gt0div  9868  ge0div  9869  lt2msq1  9885  lediv12a  9895  recgt1i  9899  recreclt  9901  ledivp1  9904  squeeze0  9905  recgt0ii  9908  ledivp1i  9928  ltdivp1i  9929  fimaxre2  9948  supmul1  9965  supmul  9968  inelr  9982  crne0  9985  nnge1  10018  nngt0  10021  nnrecgt0  10029  0le0  10073  nn0ssre  10217  nn0ge0  10239  nn0nlt0  10240  nn0le0eq0  10242  elnnnn0b  10256  elnnnn0c  10257  nn0sub  10262  elnnz  10284  0z  10285  elnn0z  10286  elnnz1  10299  nn0lt10b  10328  recnz  10337  gtndiv  10339  uzindOLD  10356  fnn0ind  10361  rpge0  10616  rpgecl  10629  ge0p1rp  10632  rpneg  10633  0nrp  10634  ge0gtmnf  10752  max0sub  10774  qsqueeze  10779  xneg0  10790  xaddid1  10817  xsubge0  10832  xmulpnf1  10845  xmulgt0  10854  xlemul1a  10859  xadddi  10866  xrsupsslem  10877  xrinfmsslem  10878  elrege0  10999  0elunit  11007  1elunit  11008  lincmb01cmp  11030  iccf1o  11031  xov1plusxeqvd  11033  unitssre  11034  elfznelfzo  11184  rpsup  11239  0mod  11264  1mod  11265  expgt1  11410  ltexp2a  11423  expcan  11424  ltexp2  11425  leexp2  11426  leexp2a  11427  expubnd  11432  le2sq2  11449  sqlecan  11479  bernneq2  11498  expnbnd  11500  expnlbnd  11501  expnlbnd2  11502  expmulnbnd  11503  discr1  11507  discr  11508  facdiv  11570  faclbnd  11573  faclbnd3  11575  faclbnd6  11582  bcval4  11590  bcval5  11601  bcpasc  11604  hasheq0  11636  hashnn0n0nn  11656  hashgt12el  11674  hashgt12el2  11675  brfi1uzind  11707  reim0  11915  re0  11949  im0  11950  rei  11953  imi  11954  cj0  11955  sqeqd  11963  rennim  12036  cnpart  12037  sqr0lem  12038  sqrlem4  12043  resqrex  12048  sqrgt0  12056  sqr00  12061  sqrneglem  12064  sqr4  12070  sqr9  12071  sqr2gt1lt2  12072  leabs  12096  absor  12097  max0add  12107  absgt0  12120  sqreulem  12155  eqsqr2d  12164  amgm2  12165  sqrpclii  12178  rlimconst  12330  rlimrege0  12365  lo1mul  12413  iserge0  12446  iseraltlem2  12468  fsumrecl  12520  fsumge0  12566  fsum00  12569  o1fsum  12584  cvgcmp  12587  cvgcmpce  12589  isumless  12617  arisum2  12632  georeclim  12641  geo2sum  12642  geo2lim  12644  geomulcvg  12645  geoisumr  12647  0.999...  12650  cvgrat  12652  mertenslem2  12654  efcllem  12672  ege2le3  12684  cos0  12743  ef01bndlem  12777  sin01bnd  12778  cos01bnd  12779  cos2bnd  12781  sin01gt0  12783  cos01gt0  12784  sincos2sgn  12787  sin4lt0  12788  absef  12790  absefib  12791  efieq1re  12792  epos  12798  znnenlem  12803  rpnnen2lem2  12807  rpnnen2lem3  12808  rpnnen2lem4  12809  rpnnen2lem9  12814  rpnnen2  12817  ruclem6  12826  nthruz  12843  moddvds  12851  dvdslelem  12886  divalglem1  12906  divalglem5  12909  divalglem6  12910  bitsp1o  12937  bitsinv1lem  12945  sadcaddlem  12961  sadcadd  12962  gcdn0gt0  13014  nn0seqcvgd  13053  algcvgblem  13060  algcvga  13062  qnumgt0  13134  pythagtriplem12  13192  pythagtriplem13  13193  pythagtriplem14  13194  pythagtriplem16  13196  qexpz  13262  prmreclem4  13279  prmreclem5  13280  prmreclem6  13281  1arith  13287  4sqlem6  13303  vdwap0  13336  ramz  13385  mulgnegnn  14892  subgmulg  14950  isabvd  15900  abvf  15903  abvtrivd  15920  psrbaglesupp  16425  xrs1mnd  16728  xrs10  16729  rege0subm  16747  gzrngunit  16756  leordtval2  17268  pnfnei  17276  mnfnei  17277  prdsmet  18392  imasdsf1olem  18395  ssblps  18444  ssbl  18445  xmeter  18455  metustexhalfOLD  18585  metustexhalf  18586  dscmet  18612  dscopn  18613  nlmvscnlem2  18713  nlmvscnlem1  18714  nmoi  18754  nmo0  18761  nmoeq0  18762  0nghm  18767  idnghm  18769  cnbl0  18800  blcvx  18821  xrsxmet  18832  metdseq0  18876  iicmp  18908  iicon  18909  iirev  18946  iihalf1  18948  iihalf1cn  18949  iihalf2  18950  elii1  18952  elii2  18953  iimulcl  18954  icopnfcnv  18959  icopnfhmeo  18960  iccpnfcnv  18961  iccpnfhmeo  18962  xrhmeo  18963  xrhmph  18964  evth  18976  lebnumlem1  18978  lebnumii  18983  htpycc  18997  reparphti  19014  pcoval1  19030  pco0  19031  pcoval2  19033  pcocn  19034  pcohtpylem  19036  pcopt  19039  pcopt2  19040  pcoass  19041  pcorevlem  19043  nmoleub2lem3  19115  cphsqrcl  19139  ipcnlem2  19190  ipcnlem1  19191  minveclem4c  19318  minveclem2  19319  minveclem3b  19321  minveclem4  19325  minveclem6  19327  minveclem7  19328  pjthlem1  19330  cniccbdd  19350  ovollb2lem  19376  ovollb2  19377  ovolunlem1a  19384  ovolunlem1  19385  ovolunnul  19388  ovoliunlem1  19390  ovoliunnul  19395  ovolicc1  19404  ovolicc2lem4  19408  ovolicopnf  19412  ovolre  19413  voliunlem3  19438  volsup  19442  ioombl1lem2  19445  ioombl1lem4  19447  iccvolcl  19453  ovolioo  19454  ioorcl2  19456  ioorcl  19461  uniioombllem1  19465  uniioombllem2  19467  uniioombllem3  19469  uniioombllem6  19472  volivth  19491  vitalilem2  19493  vitalilem4  19495  vitalilem5  19496  vitali  19497  ismbf  19514  mbfmulc2lem  19531  mbfpos  19535  mbfposr  19536  0plef  19556  i1f0  19571  i1f1  19574  itg1addlem2  19581  itg1addlem4  19583  itg1addlem5  19584  i1fmulc  19587  itg1mulc  19588  itg1ge0a  19595  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  mbfi1fseqlem5  19603  mbfi1fseqlem6  19604  mbfi1flimlem  19606  mbfi1flim  19607  xrge0f  19615  itg2ge0  19619  itg2const  19624  itg2seq  19626  itg2mulclem  19630  itg2mulc  19631  itg2splitlem  19632  itg2split  19633  itg2monolem1  19634  itg2monolem2  19635  itg2monolem3  19636  itg2mono  19637  itg2i1fseq  19639  itg2gt0  19644  itg2cnlem1  19645  itg2cnlem2  19646  ibl0  19670  iblrelem  19674  iblposlem  19675  iblpos  19676  iblre  19677  itgreval  19680  itgneg  19687  iblss  19688  i1fibl  19691  itgitg1  19692  itgle  19693  itgge0  19694  itgeqa  19697  itgless  19700  iblconst  19701  itgconst  19702  ibladdlem  19703  itgaddlem1  19706  itgaddlem2  19707  iblabslem  19711  iblabs  19712  iblabsr  19713  iblmulc2  19714  itgmulc2lem1  19715  itgmulc2lem2  19716  itgabs  19718  itgsplit  19719  bddmulibl  19722  itggt0  19725  itgcn  19726  dvferm1  19861  dvferm2  19863  dvferm  19864  dvlip  19869  dvlipcn  19870  c1lip1  19873  dveq0  19876  dv11cn  19877  dvlt0  19881  dvne0  19887  dvfsumge  19898  ftc1lem4  19915  deg1lt0  20006  ply1divex  20051  plypf1  20123  dgradd2  20178  dgrco  20185  plyrecj  20189  plydivlem3  20204  vieta1lem2  20220  aalioulem2  20242  aalioulem3  20243  mtest  20312  radcnvlem1  20321  radcnv0  20324  radcnvlt1  20326  radcnvle  20328  pserulm  20330  psercnlem2  20332  psercnlem1  20333  psercn  20334  pserdvlem1  20335  pserdv  20337  abelthlem2  20340  abelthlem6  20344  abelthlem7  20346  abelth  20349  abelth2  20350  reeff1olem  20354  reeff1o  20355  pilem2  20360  pilem3  20361  pipos  20365  sinhalfpilem  20366  sincosq1sgn  20398  sincosq2sgn  20399  coseq00topi  20402  coseq0negpitopi  20403  tangtx  20405  tanabsge  20406  sinq12ge0  20408  sinq34lt0t  20409  cosq14ge0  20411  sincos4thpi  20413  tan4thpi  20414  sincos6thpi  20415  pige3  20417  sineq0  20421  cosordlem  20425  cosord  20426  cos11  20427  sinord  20428  recosf1o  20429  resinf1o  20430  tanord1  20431  tanord  20432  tanregt0  20433  efif1olem4  20439  efifo  20441  relogrn  20451  log1  20472  logneg  20474  logne0  20489  rplogcl  20491  argregt0  20497  argrege0  20498  argimgt0  20499  logneg2  20502  logdivlti  20507  logdivlt  20508  logdivle  20509  ellogdm  20522  logdmn0  20523  logdmnrp  20524  logcnlem3  20527  logcnlem4  20528  dvloglem  20531  logdmopn  20532  logf1o2  20533  dvlog2lem  20535  efopnlem1  20539  logtayl  20543  recxpcl  20558  cxpge0  20566  abscxp2  20576  cxplt  20577  cxple  20578  cxple2  20580  cxple2a  20582  cxpsqrlem  20585  cxpcn3lem  20623  cxpcn3  20624  cxpaddlelem  20627  cxpaddle  20628  abscxpbnd  20629  loglesqr  20634  ang180lem3  20645  ang180lem4  20646  chordthmlem4  20668  chordthmlem5  20669  asinlem3  20703  atanre  20717  asinneg  20718  asin1  20726  reasinsin  20728  acosbnd  20732  atan0  20740  atanrecl  20743  atanlogaddlem  20745  atanlogadd  20746  atanlogsublem  20747  atanlogsub  20748  atantan  20755  atanbnd  20758  atan1  20760  atans2  20763  ressatans  20766  leibpi  20774  log2cnv  20776  log2tlbnd  20777  log2ublem3  20780  log2ub  20781  rlimcnp  20796  rlimcnp2  20797  rlimcnp3  20798  efrlim  20800  o1cxp  20805  cxp2limlem  20806  cxp2lim  20807  cxploglim2  20809  divsqrsumlem  20810  jensenlem1  20817  jensenlem2  20818  jensen  20819  amgm  20821  emgt0  20837  harmonicbnd3  20838  harmoniclbnd  20839  harmonicubnd  20840  harmonicbnd4  20841  fsumharmonic  20842  ftalem1  20847  ftalem2  20848  ftalem5  20851  basellem3  20857  basellem8  20862  efnnfsumcl  20877  ppisval  20878  vmacl  20893  vmage0  20896  chpge0  20901  chtwordi  20931  efchtdvds  20934  ppiwordi  20937  chtrpcl  20950  ppiltx  20952  fsumfldivdiaglem  20966  ppiub  20980  chpeq0  20984  chteq0  20985  chtleppi  20986  fsumvma2  20990  chpval2  20994  chpchtsum  20995  chpub  20996  logfacbnd3  20999  logexprlim  21001  mersenne  21003  dchr1re  21039  bcmono  21053  efexple  21057  bposlem1  21060  bposlem4  21063  bposlem5  21064  bposlem7  21066  bposlem8  21067  bposlem9  21068  lgslem4  21075  lgsval2lem  21082  lgsval4a  21094  lgsneg  21095  lgsdilem  21098  lgsdir2lem1  21099  lgsne0  21109  lgseisen  21129  lgsquadlem1  21130  lgsquadlem2  21131  m1lgs  21138  2sqlem11  21151  chebbnd1lem2  21156  chebbnd1lem3  21157  chebbnd1  21158  chtppilimlem1  21159  chtppilimlem2  21160  chtppilim  21161  chebbnd2  21163  chto1lb  21164  chpchtlim  21165  chpo1ub  21166  rplogsumlem2  21171  rpvmasumlem  21173  dchrisumlema  21174  dchrisumlem2  21176  dchrisumlem3  21177  dchrmusumlema  21179  dchrvmasumlem2  21184  dchrvmasumiflem1  21187  dchrisum0flblem1  21194  dchrisum0flblem2  21195  dchrisum0fno1  21197  dchrisum0re  21199  dchrisum0lema  21200  dchrisum0  21206  rplogsum  21213  dirith2  21214  logdivsum  21219  mulog2sumlem1  21220  mulog2sumlem2  21221  vmalogdivsum2  21224  log2sumbnd  21230  selberg2lem  21236  chpdifbndlem1  21239  chpdifbndlem2  21240  chpdifbnd  21241  logdivbnd  21242  selberg3lem1  21243  pntrmax  21250  pntrsumo1  21251  pntrlog2bndlem4  21266  pntrlog2bndlem5  21267  pntpbnd1a  21271  pntpbnd1  21272  pntpbnd2  21273  pntlemg  21284  pntlemj  21289  pntlemk  21292  pntlem3  21295  pntleml  21297  pnt2  21299  pnt  21300  ostth2lem1  21304  padicabv  21316  padicabvcxp  21318  ostth2lem3  21321  ostth2lem4  21322  ostth2  21323  ostth3  21324  usgraexvlem  21406  usgraex0elv  21407  spthispth  21565  nvnencycllem  21622  vdgr0  21663  konigsberg  21701  ex-po  21735  gxnval  21840  readdsubgo  21933  nvz0  22149  ipidsq  22201  0blo  22285  nmlno0lem  22286  nmblolbii  22292  siilem2  22345  minvecolem2  22369  minvecolem3  22370  minvecolem4c  22373  minvecolem4  22374  minvecolem5  22375  minvecolem6  22376  minvecolem7  22377  htthlem  22412  hiidge0  22592  normlem6  22609  normgt0  22621  norm-i  22623  normpyc  22640  normpar2i  22650  bcsiALT  22673  pjhthlem1  22885  pjneli  23217  0bdop  23488  nmlnop0iALT  23490  unopbd  23510  nmbdoplbi  23519  nmcoplbi  23523  nmbdfnlbi  23544  nmbdfnlb  23545  nmcfnlbi  23547  cnlnadjlem7  23568  nmopcoi  23590  branmfn  23600  leopmul  23629  nmopleid  23634  pjbdlni  23644  pjnormssi  23663  stge0  23719  stle1  23720  stle0i  23734  strlem3a  23747  cdj3lem1  23929  xaddeq0  24111  xlt2addrd  24116  bcm1n  24143  xdiv0  24167  xrge00  24200  xrge0neqmnf  24204  xrge0adddir  24207  fsumrp0cl  24209  re0g  24265  elunitrn  24287  elunitge0  24289  unitdivcld  24291  sqsscirc1  24298  xrge0iifcnv  24311  xrge0iifiso  24313  xrge0iifhom  24315  xrge0mulc1cn  24319  lmlimxrge0  24326  rge0scvg  24327  pnfneige0  24328  lmxrge0  24329  lmdvg  24330  reust  24336  recusp  24337  rezh  24347  rrhre  24379  rnlogblem  24391  logbrec  24397  log2le1  24399  indf  24405  indfval  24406  pr01ssre  24407  indf1o  24413  esumfsupre  24453  esumpfinvallem  24456  esumpfinval  24457  esumpfinvalf  24458  esumpcvgval  24460  esumcvg  24468  measinb  24567  voliune  24577  volfiniune  24578  sibfof  24646  sitgclg  24648  sitmcl  24655  0rrv  24701  coinfliprv  24732  ballotlem2  24738  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemodife  24747  ballotlem4  24748  ballotlemi1  24752  ballotlemic  24756  zetacvg  24791  eldmgm  24798  dmlogdmgm  24800  lgamgulmlem1  24805  lgamgulmlem2  24806  rescon  24925  iiscon  24931  iillyscon  24932  cvmliftlem2  24965  cvmliftlem10  24973  snmlff  25008  divelunit  25177  mulge0b  25183  relin01  25186  fz0n  25194  4bc2eq6  25196  brbtwn2  25836  axsegconlem7  25854  axsegconlem10  25857  ax5seglem1  25859  ax5seglem2  25860  ax5seglem3  25862  ax5seglem5  25864  ax5seglem6  25865  ax5seglem9  25868  ax5seg  25869  axbtwnid  25870  axpaschlem  25871  axpasch  25872  axlowdimlem1  25873  axlowdimlem6  25878  axlowdimlem7  25879  axlowdimlem10  25882  axlowdim1  25890  axlowdim2  25891  axlowdim  25892  axcontlem2  25896  axcontlem4  25898  axcontlem7  25901  axcontlem10  25904  bpoly4  26097  mblfinlem  26234  ismblfin  26237  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  mbfposadd  26244  itg2addnclem  26246  itg2addnclem2  26247  itg2addnclem3  26248  ibladdnclem  26251  itgaddnclem1  26253  itgaddnclem2  26254  iblabsnclem  26258  iblabsnc  26259  iblmulc2nc  26260  itgmulc2nclem1  26261  itgmulc2nclem2  26262  itgabsnc  26264  bddiblnc  26265  itggt0cn  26267  ftc1cnnclem  26268  ftc1anclem5  26274  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  dvreasin  26280  areacirclem2  26282  areacirclem3  26283  areacirclem4  26284  areacirclem5  26286  areacirc  26288  nn0prpwlem  26316  geomcau  26456  isbnd3  26484  isbnd3b  26485  ssbnd  26488  prdsbnd  26493  bfplem2  26523  bfp  26524  rrnequiv  26535  modelico  26875  irrapxlem1  26876  irrapxlem2  26877  irrapxlem3  26878  irrapxlem4  26879  pellexlem6  26888  pell14qrgt0  26913  elpell14qr2  26916  pell1qrgaplem  26927  pellfundex  26940  pellfundrp  26942  monotoddzzfi  26996  oddcomabszz  26998  zindbi  27000  jm2.24  27019  acongeq  27039  jm2.23  27058  jm2.26lem3  27063  jm3.1lem3  27081  hbtlem5  27300  dvconstbi  27519  ioovolcl  27709  itgsin0pilem1  27711  itgsinexplem1  27715  itgsinexp  27716  stoweidlem1  27717  stoweidlem7  27723  stoweidlem11  27727  stoweidlem17  27733  stoweidlem25  27741  stoweidlem26  27742  stoweidlem34  27750  stoweidlem36  27752  stoweidlem41  27757  stoweidlem42  27758  stoweidlem44  27760  stoweidlem45  27761  stoweidlem55  27771  stoweid  27779  wallispilem1  27781  wallispilem2  27782  wallispilem3  27783  wallispilem4  27784  wallispi  27786  wallispi2lem1  27787  wallispi2  27789  stirlinglem1  27790  stirlinglem3  27792  stirlinglem4  27793  stirlinglem5  27794  stirlinglem6  27795  stirlinglem7  27796  stirlinglem10  27799  stirlinglem11  27800  stirlinglem12  27801  stirlinglem13  27802  stirlinglem14  27803  stirlinglem15  27804  stirlingr  27806  sharhght  27822  0mnnnnn0  28080  2eluzge0  28086  elfz2z  28089  elfz0fzfz0  28098  fz0fzelfz0  28102  fzo1fzo0n0  28111  wrdsymb0  28147  ccatsymb  28152  swrdnd  28154  swrdvalodmlem1  28159  swrdvalodm2  28160  swrdswrdlem  28164  swrdswrd  28165  swrdccatin2  28176  swrdccatin12lem4  28179  modprm0  28194  cshwidx  28208  2cshw1lem1  28214  2cshw1lem2  28215  cshweqdif2s  28234  usgra2pthlem1  28263  ex-gt  28408  sgnpnf  28460  sgnmnf  28462  sineq0ALT  28986
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-1cn 9040  ax-icn 9041  ax-addcl 9042  ax-addrcl 9043  ax-mulcl 9044  ax-mulrcl 9045  ax-i2m1 9050  ax-1ne0 9051  ax-rnegex 9053  ax-rrecex 9054  ax-cnre 9055
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-iota 5410  df-fv 5454  df-ov 6076
  Copyright terms: Public domain W3C validator