Theorem 0re 10040

Description: 0 is a real number. See also 0reALT 10378. (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

Step	Hyp	Ref	Expression
1		1re 10039	. 2 |- 1 e. RR
2		ax-rnegex 10007	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 10019	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 706	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2689	. . . 4 |- ( ( 1 + x ) = 0 -> ( ( 1 + x ) e. RR <-> 0 e. RR ) )
6	4, 5	syl5ibcom 235	. . 3 |- ( x e. RR -> ( ( 1 + x ) = 0 -> 0 e. RR ) )
7	6	rexlimiv 3027	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 10	1 |- 0 e. RR

Syntax hints:   = wceq 1483   e. wcel 1990   E.wrex 2913  (class class class)co 6650   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  0red  10041  0xr  10086  axmulgt0  10112  ne0gt0  10142  00id  10211  mul02lem1  10212  mul02lem2  10213  mul02  10214  addid1  10216  ltaddneg  10251  addgt0  10514  addgegt0  10515  addgtge0  10516  addge0  10517  ltaddpos  10518  ltneg  10528  leneg  10531  lt0neg1  10534  lt0neg2  10535  le0neg1  10536  le0neg2  10537  addge01  10538  suble0  10542  mulge0  10546  msqge0  10549  0le1  10551  relin01  10552  gt0ne0i  10563  gt0ne0d  10592  lt0ne0d  10593  elimge0  10860  ltm1  10863  recgt0  10867  prodgt0  10868  lemul1a  10877  ltmul12a  10879  lemul12a  10881  mulgt1  10882  gt0div  10889  ge0div  10890  mulge0b  10893  lediv12a  10916  recgt1i  10920  recreclt  10922  ledivp1  10925  squeeze0  10926  recgt0ii  10929  ledivp1i  10949  ltdivp1i  10950  fimaxre2  10969  inelr  11010  crne0  11013  nnge1  11046  nngt0  11049  nnnle0  11051  nnrecgt0  11058  0le0  11110  neg1lt0  11127  halfge0  11249  nn0ssre  11296  nn0ge0  11318  nn0nlt0  11319  nn0le0eq0  11321  0mnnnnn0  11325  elnnnn0b  11337  elnnnn0c  11338  nn0sub  11343  elnnz  11387  0z  11388  elnn0z  11390  elnnz1  11403  recnz  11452  gtndiv  11454  fnn0ind  11476  rpge0  11845  rpneg  11863  0nrp  11865  zgt1rpn0n1  11871  0ltpnf  11956  mnflt0  11959  qsqueeze  12032  xneg0  12043  xaddid1  12072  xnn0xadd0  12077  xmulpnf1  12104  xlemul1a  12118  xadddi  12125  xrsupsslem  12137  xrinfmsslem  12138  elrege0  12278  0e0icopnf  12282  0elunit  12290  1elunit  12291  divelunit  12314  lincmb01cmp  12315  iccf1o  12316  unitssre  12319  0nelfz1  12360  fzpreddisj  12390  fz0to4untppr  12442  nn0p1elfzo  12510  ico01fl0  12620  rpsup  12665  modelico  12680  0mod  12701  1mod  12702  expubnd  12921  le2sq2  12939  sqlecan  12971  bernneq2  12991  expnbnd  12993  expnlbnd  12994  expmulnbnd  12996  discr1  13000  discr  13001  facdiv  13074  faclbnd  13077  faclbnd3  13079  faclbnd6  13086  bcval4  13094  bcval5  13105  bcpasc  13108  hasheq0  13154  hashneq0  13155  hashnn0n0nn  13180  hashgt12el  13210  hashgt12el2  13211  hashge2el2dif  13262  lsw0  13352  reim0  13858  re0  13892  im0  13893  rei  13896  imi  13897  cj0  13898  sqeqd  13906  rennim  13979  cnpart  13980  sqr0lem  13981  sqrlem4  13986  resqrex  13991  sqrtgt0  13999  sqrt00  14004  sqrtneglem  14007  sqrt9  14014  sqrt2gt1lt2  14015  leabs  14039  absor  14040  max0add  14050  eqsqrt2d  14108  sqrtpclii  14122  rlimconst  14275  rlimrege0  14310  lo1mul  14358  iserge0  14391  fsum00  14530  isumless  14577  arisum2  14593  georeclim  14603  geo2sum  14604  geo2lim  14606  geoisumr  14609  0.999...  14612  0.999...OLD  14613  cvgrat  14615  bpoly4  14790  cos0  14880  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  cos2bnd  14918  sin01gt0  14920  cos01gt0  14921  sincos2sgn  14924  sin4lt0  14925  absef  14927  absefib  14928  efieq1re  14929  epos  14935  znnenlem  14940  rpnnen2lem2  14944  rpnnen2lem3  14945  rpnnen2lem4  14946  rpnnen2lem9  14951  rpnnen2lem12  14954  ruclem6  14964  dvdslelem  15031  divalglem1  15117  divalglem5  15120  divalglem6  15121  flodddiv4  15137  bitsp1o  15155  sadcadd  15180  gcdn0gt0  15239  nn0seqcvgd  15283  algcvgblem  15290  algcvga  15292  pythagtriplem12  15531  pythagtriplem13  15532  pythagtriplem14  15533  pythagtriplem16  15535  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  1arith  15631  vdwap0  15680  ramz  15729  mulgnegnn  17551  subgmulg  17608  srgbinomlem4  18543  isabvd  18820  abvtrivd  18840  psrbaglesupp  19368  xrs1mnd  19784  xrs10  19785  rge0srg  19817  psgnodpmr  19936  re0g  19958  mnfnei  21025  imasdsf1olem  22178  ssblps  22227  ssbl  22228  xmeter  22238  dscmet  22377  dscopn  22378  nmoi  22532  nmoeq0  22540  0nghm  22545  idnghm  22547  cnbl0  22577  blcvx  22601  xrsxmet  22612  metdseq0  22657  iicmp  22689  iiconn  22690  iirev  22728  iihalf1  22730  iihalf1cn  22731  iihalf2  22732  elii1  22734  elii2  22735  iimulcl  22736  icopnfcnv  22741  icopnfhmeo  22742  iccpnfcnv  22743  iccpnfhmeo  22744  xrhmeo  22745  xrhmph  22746  lebnumii  22765  htpycc  22779  reparphti  22797  pcoval1  22813  pco0  22814  pcoval2  22816  pcocn  22817  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  reust  23169  recusp  23170  minveclem4c  23196  minveclem2  23197  minveclem3b  23199  minveclem4  23203  minveclem7  23206  pjthlem1  23208  cniccbdd  23230  ovolunnul  23268  ovoliunnul  23275  ovolicc1  23284  ovolre  23293  iccvolcl  23335  ovolioo  23336  ioovolcl  23338  ioorcl  23345  vitalilem2  23378  vitalilem4  23380  vitalilem5  23381  vitali  23382  ismbf  23397  mbfmulc2lem  23414  mbfpos  23418  mbfposr  23419  i1f0  23454  i1f1  23457  itg1addlem2  23464  itg1addlem4  23466  itg1addlem5  23467  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  mbfi1flimlem  23489  xrge0f  23498  itg2ge0  23502  itg2const  23507  itg2mulc  23514  itg2splitlem  23515  itg2gt0  23527  itg2cnlem1  23528  ibl0  23553  iblrelem  23557  iblposlem  23558  iblpos  23559  iblre  23560  itgreval  23563  itgneg  23570  iblss  23571  i1fibl  23574  itgitg1  23575  itgle  23576  itgeqa  23580  itgless  23583  iblconst  23584  itgconst  23585  ibladdlem  23586  itgaddlem2  23590  iblabslem  23594  iblabsr  23596  iblmulc2  23597  itgmulc2lem2  23599  itgabs  23601  itgsplit  23602  bddmulibl  23605  dvferm1  23748  dvferm2  23750  dvferm  23751  dvlip  23756  c1lip1  23760  dveq0  23763  dv11cn  23764  dvne0  23774  ftc1lem4  23802  ply1divex  23896  dgrco  24031  plyrecj  24035  vieta1lem2  24066  aalioulem2  24088  aalioulem3  24089  pserulm  24176  psercnlem2  24178  psercnlem1  24179  psercn  24180  abelthlem6  24190  abelth  24195  abelth2  24196  reeff1olem  24200  reeff1o  24201  pilem2  24206  pilem3  24207  pipos  24212  sinhalfpilem  24215  sincosq1sgn  24250  sincosq2sgn  24251  coseq00topi  24254  coseq0negpitopi  24255  tangtx  24257  tanabsge  24258  sinq12ge0  24260  sinq34lt0t  24261  cosq14ge0  24263  sincos4thpi  24265  sincos6thpi  24267  pige3  24269  sineq0  24273  cosordlem  24277  cosord  24278  cos11  24279  sinord  24280  recosf1o  24281  resinf1o  24282  tanord1  24283  tanord  24284  tanregt0  24285  efif1olem4  24291  efifo  24293  relogrn  24308  log1  24332  logneg  24334  argregt0  24356  argrege0  24357  argimgt0  24358  logneg2  24361  logdivlti  24366  logdivlt  24367  ellogdm  24385  logdmn0  24386  logdmnrp  24387  logcnlem3  24390  dvloglem  24394  logdmopn  24395  logf1o2  24396  dvlog2lem  24398  efopnlem1  24402  logtayl  24406  recxpcl  24421  cxpge0  24429  cxple2  24443  cxple2a  24445  cxpsqrtlem  24448  cxpcn3  24489  cxpaddlelem  24492  cxpaddle  24493  loglesqrt  24499  logbrec  24520  ang180lem3  24541  ang180lem4  24542  chordthmlem4  24562  heron  24565  asinneg  24613  asin1  24621  reasinsin  24623  acosbnd  24627  atan0  24635  atanrecl  24638  atanlogaddlem  24640  atanlogsublem  24642  atanlogsub  24643  atantan  24650  atanbnd  24653  atan1  24655  atans2  24658  ressatans  24661  leibpi  24669  log2cnv  24671  log2tlbnd  24672  log2ub  24676  log2le1  24677  rlimcnp  24692  rlimcnp2  24693  o1cxp  24701  jensenlem2  24714  jensen  24715  amgm  24717  emgt0  24733  harmonicbnd3  24734  harmoniclbnd  24735  harmonicbnd4  24737  zetacvg  24741  eldmgm  24748  lgamgulmlem2  24756  basellem3  24809  basellem8  24814  efnnfsumcl  24829  ppisval  24830  vmage0  24847  chpge0  24852  efchtdvds  24885  ppiltx  24903  ppiub  24929  chpeq0  24933  chteq0  24934  chtleppi  24935  chpchtsum  24944  chpub  24945  dchr1re  24988  bcmono  25002  efexple  25006  bposlem1  25009  bposlem4  25012  bposlem5  25013  bposlem7  25015  bposlem8  25016  bposlem9  25017  lgsval2lem  25032  lgsval4a  25044  lgsneg  25046  lgsdilem  25049  lgsdir2lem1  25050  2lgsoddprmlem3a  25135  2lgsoddprmlem3b  25136  2lgsoddprmlem3c  25137  2lgsoddprmlem3d  25138  rplogsumlem2  25174  rpvmasumlem  25176  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0fno1  25200  rplogsum  25216  logdivsum  25222  mulog2sumlem2  25224  selberg2lem  25239  logdivbnd  25245  pntrsumo1  25254  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntpbnd1  25275  pntpbnd2  25276  pntlem3  25298  pntleml  25300  ostth2  25326  trgcgrg  25410  ttgcontlem1  25765  brbtwn2  25785  ax5seglem1  25808  ax5seglem2  25809  ax5seglem3  25811  ax5seglem5  25813  ax5seglem6  25814  ax5seglem9  25817  ax5seg  25818  axbtwnid  25819  axpaschlem  25820  axpasch  25821  axlowdimlem1  25822  axlowdimlem6  25827  axlowdimlem7  25828  axlowdimlem10  25831  axlowdim1  25839  axlowdim2  25840  axlowdim  25841  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  umgrislfupgrlem  26017  lfgrnloop  26020  lfuhgr1v0e  26146  usgrexmplef  26151  pthdlem2  26664  crctcshwlkn0lem7  26708  rusgrnumwwlks  26869  konigsberg  27119  ex-po  27292  ex-sqrt  27311  ex-gcd  27314  nvz0  27523  0blo  27647  nmlno0lem  27648  nmblolbii  27654  siilem2  27707  minvecolem2  27731  minvecolem3  27732  minvecolem4c  27735  minvecolem4  27736  minvecolem5  27737  minvecolem7  27739  htthlem  27774  hiidge0  27955  normlem6  27972  normgt0  27984  norm-i  27986  normpyc  28003  bcsiALT  28036  pjhthlem1  28250  pjneli  28582  nmlnop0iALT  28854  unopbd  28874  nmbdoplbi  28883  nmcoplbi  28887  nmbdfnlbi  28908  nmbdfnlb  28909  nmcfnlbi  28911  cnlnadjlem7  28932  nmopcoi  28954  branmfn  28964  leopmul  28993  nmopleid  28998  pjbdlni  29008  pjnormssi  29027  stge0  29083  stle1  29084  stle0i  29098  strlem3a  29111  cdj3lem1  29293  xaddeq0  29518  pr01ssre  29570  dp20u  29585  dp20h  29586  dp2clq  29588  dp2lt10  29591  dp2lt  29592  dp0u  29609  dplti  29613  dpexpp1  29616  xdiv0  29637  xrge0slmod  29844  elunitrn  29943  elunitge0  29945  unitdivcld  29947  sqsscirc1  29954  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  rezh  30015  indf  30077  indfval  30078  esumcvgsum  30150  voliune  30292  volfiniune  30293  sibfinima  30401  sitmcl  30413  0rrv  30513  coinfliprv  30544  ballotlem2  30550  ballotlem4  30560  ballotlemi1  30564  ballotlemic  30568  sgnclre  30601  sgnnbi  30607  sgnpbi  30608  plymulx0  30624  signsply0  30628  signswch  30638  signstf  30643  signstf0  30645  signstfveq0  30654  signlem0  30664  itgexpif  30684  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  hgt750leme  30736  resconn  31228  iisconn  31234  iillysconn  31235  cvmliftlem10  31276  snmlff  31311  fz0n  31616  logi  31620  bcneg1  31622  nn0prpwlem  32317  dnizeq0  32465  dnizphlfeqhlf  32466  knoppndvlem13  32515  cnndvlem1  32528  bj-pinftyccb  33108  bj-minftyccb  33112  bj-pinftynminfty  33114  taupilemrplb  33166  sin2h  33399  tan2h  33401  ptrecube  33409  poimirlem16  33425  poimirlem17  33426  poimirlem20  33429  poimirlem22  33431  poimirlem23  33432  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  poimir  33442  heicant  33444  mblfinlem2  33447  ismblfin  33450  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  mbfposadd  33457  itg2addnclem  33461  itg2addnclem2  33462  ibladdnclem  33466  itgaddnclem2  33469  iblabsnclem  33473  iblmulc2nc  33475  itgmulc2nclem2  33477  itgabsnc  33479  ftc1cnnclem  33483  ftc1anclem5  33489  ftc1anclem8  33492  asindmre  33495  dvasin  33496  areacirclem4  33503  areacirc  33505  isbnd3  33583  ssbnd  33587  prdsbnd  33592  bfplem2  33622  bfp  33623  renegclALT  34249  pellexlem6  37398  elpell14qr2  37426  oddcomabszz  37509  zindbi  37511  jm2.24  37530  acongeq  37550  arearect  37801  areaquad  37802  relexp01min  38005  imo72b2lem0  38465  imo72b2lem2  38467  imo72b2lem1  38471  imo72b2  38475  dvconstbi  38533  binomcxplemnn0  38548  binomcxplemdvbinom  38552  binomcxplemcvg  38553  binomcxplemnotnn0  38555  sineq0ALT  39173  halffl  39510  ren0  39626  sqrlearg  39780  limsup10ex  40005  liminf10ex  40006  dvnmptdivc  40153  dvnmul  40158  itgsin0pilem1  40165  itgsinexplem1  40169  itgsinexp  40170  iblempty  40181  stoweidlem17  40234  stoweidlem36  40253  stoweidlem55  40272  wallispilem1  40282  wallispilem2  40283  wallispilem4  40285  stirlinglem4  40294  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  stirlingr  40307  dirker2re  40309  dirkerdenne0  40310  dirkerre  40312  dirkertrigeqlem1  40315  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem11  40335  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem41  40365  fourierdlem42  40366  fourierdlem48  40371  fourierdlem62  40385  fourierdlem66  40389  fourierdlem79  40402  fourierdlem83  40406  fourierdlem94  40417  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  fourierdlem114  40437  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  etransclem23  40474  etransclem44  40495  etransclem46  40497  salexct3  40560  salgensscntex  40562  sge0rnn0  40585  sge00  40593  0ome  40743  ovn0lem  40779  ovnhoilem1  40815  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  smfmullem4  41001  zm1nn  41316  m1mod0mod1  41339  fmtnoprmfac2lem1  41478  31prm  41512  mod42tp1mod8  41519  tgblthelfgott  41703  tgblthelfgottOLD  41709  altgsumbcALT  42131  expnegico01  42308  dignnld  42397  ex-gt  42469