Theorem 0xr 10086

Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)

Assertion

Ref	Expression
0xr	|- 0 e. RR*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 10083	. 2 |- RR C_ RR*
2		0re 10040	. 2 |- 0 e. RR
3	1, 2	sselii 3600	1 |- 0 e. RR*

Syntax hints:   e. wcel 1990   RRcr 9935   0cc0 9936   RR*cxr 10073

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  df-xr 10078

This theorem is referenced by:  0lepnf  11966  ge0gtmnf  12003  max0sub  12027  xlt0neg1  12050  xlt0neg2  12051  xle0neg1  12052  xle0neg2  12053  xaddf  12055  xaddid1  12072  xaddid2  12073  xnn0xadd0  12077  xaddge0  12088  xsubge0  12091  xposdif  12092  xmullem  12094  xmullem2  12095  xmul01  12097  xmul02  12098  xmulneg1  12099  xmulf  12102  xmulpnf1  12104  xmulasslem2  12112  xmulge0  12114  xmulasslem  12115  xlemul1a  12118  xadddi  12125  xadddi2  12127  ioopos  12250  ioorebas  12275  xrge0neqmnf  12276  elxrge0  12281  0e0iccpnf  12283  xov1plusxeqvd  12318  xnn0xrge0  12325  ico01fl0  12620  rpsup  12665  addmodid  12718  hashgt0  13177  hashle00  13188  hashgt0elex  13189  sgn0  13829  sgnp  13830  sgnn  13834  fprodge0  14724  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  cos1bnd  14917  sinltx  14919  sin01gt0  14920  cos01gt0  14921  sin02gt0  14922  sincos1sgn  14923  sincos2sgn  14924  halfleoddlt  15086  xrsmgm  19781  leordtval2  21016  pnfnei  21024  mnfnei  21025  psmetge0  22117  isxmet2d  22132  xmetge0  22149  xmetgt0  22163  prdsdsf  22172  prdsxmetlem  22173  xpsdsval  22186  blgt0  22204  xblss2ps  22206  xblss2  22207  xbln0  22219  prdsbl  22296  stdbdxmet  22320  stdbdmopn  22323  metustto  22358  metustid  22359  metustexhalf  22361  cfilucfil  22364  blval2  22367  metuel2  22370  nmoge0  22525  nmo0  22539  cnblcld  22578  blssioo  22598  blcvx  22601  xrsxmet  22612  metdsf  22651  metds0  22653  metdseq0  22657  metnrmlem1a  22661  iccpnfcnv  22743  iccpnfhmeo  22744  xrhmeo  22745  pcoass  22824  iscfil2  23064  ovolmge0  23245  ovolge0  23249  ovolf  23250  ovolssnul  23255  ovolctb  23258  ovoliunnul  23275  ovolicopnf  23292  voliunlem3  23320  volsup  23324  ioorf  23341  volivth  23375  vitalilem4  23380  vitalilem5  23381  itg2ge0  23502  itg2const2  23508  itg2seq  23509  itg2monolem1  23517  itg2monolem2  23518  itg2monolem3  23519  itg2gt0  23527  dvne0  23774  mdegle0  23837  ply1remlem  23922  ply1rem  23923  plypf1  23968  aaliou3lem2  24098  aaliou3lem3  24099  taylfvallem1  24111  taylfval  24113  tayl0  24116  radcnvcl  24171  radcnvle  24174  pserulm  24176  psercnlem1  24179  pilem2  24206  sinhalfpilem  24215  sincosq1lem  24249  sincosq1sgn  24250  sincosq2sgn  24251  tangtx  24257  tanabsge  24258  sinq12gt0  24259  cosq14gt0  24262  sincos4thpi  24265  pige3  24269  cosordlem  24277  tanord1  24283  tanord  24284  efifo  24293  argimgt0  24358  argimlt0  24359  logccv  24409  loglesqrt  24499  atantan  24650  rlimcnp  24692  rlimcnp2  24693  scvxcvx  24712  basellem1  24807  dchrisum0lem2a  25206  pntibndlem1  25278  pntibnd  25282  pntlemc  25284  pntlem3  25298  abvcxp  25304  padicabvf  25320  padicabvcxp  25321  ostth2  25326  ttgcontlem1  25765  nmooge0  27622  nmoo0  27646  nmlnogt0  27652  nmopge0  28770  nmopgt0  28771  nmfnge0  28786  nmop0  28845  nmfn0  28846  xraddge02  29521  xlt2addrd  29523  xrge0infss  29525  dfrp2  29532  elxrge02  29640  xrs0  29675  xrge00  29686  xrge0addass  29690  xrge0addgt0  29691  xrge0adddir  29692  fsumrp0cl  29695  metider  29937  unitssxrge0  29946  xrge0iifcnv  29979  xrge0iifcv  29980  xrge0iifiso  29981  xrge0iifhom  29983  xrge0mulc1cn  29987  pnfneige0  29997  lmxrge0  29998  esumgsum  30107  esumnul  30110  esum0  30111  esumle  30120  esumlef  30124  esumcst  30125  esumsnf  30126  esumpr2  30129  esumpinfval  30135  esumpinfsum  30139  esumpcvgval  30140  esumpmono  30141  hashf2  30146  esumcvg  30148  measle0  30271  voliune  30292  volfiniune  30293  ddemeas  30299  aean  30307  oms0  30359  prob01  30475  probmeasb  30492  dstfrvclim1  30539  sgncl  30600  sgn3da  30603  signsply0  30628  chtvalz  30707  hgt750lemf  30731  cvmliftlem10  31276  cvmliftlem13  31278  sinccvglem  31566  dnizeq0  32465  sin2h  33399  tan2h  33401  broucube  33443  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  mbfposadd  33457  itg2addnclem2  33462  itg2gt0cn  33465  ftc1anclem5  33489  ftc1anclem8  33492  dvasin  33496  areacirc  33505  rrnequiv  33634  idomrootle  37773  imo72b2  38475  absfico  39410  xadd0ge  39536  xrge0nemnfd  39548  xralrple2  39570  pnfel0pnf  39754  ge0nemnf2  39755  ge0xrre  39758  sqrlearg  39780  fsumge0cl  39805  limsup10ex  40005  liminf10ex  40006  sinaover2ne0  40079  itgsin0pilem1  40165  iblsplit  40182  stoweidlem46  40263  fourierdlem43  40367  fourierdlem44  40368  fourierdlem60  40383  fourierdlem61  40384  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  etransclem23  40474  salexct2  40557  fge0npnf  40584  fge0iccico  40587  gsumge0cl  40588  sge0z  40592  sge00  40593  sge0sn  40596  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0ge0  40601  sge0repnf  40603  sge0fsum  40604  sge0pr  40611  sge0ssre  40614  sge0prle  40618  sge0p1  40631  sge0iunmptlemre  40632  sge0rpcpnf  40638  sge0rernmpt  40639  sge0isum  40644  sge0ad2en  40648  sge0xaddlem2  40651  sge0uzfsumgt  40661  sge0seq  40663  sge0reuz  40664  voliunsge0lem  40689  meage0  40692  meassre  40694  meale0eq0  40695  meaiuninclem  40697  omessre  40724  omeiunltfirp  40733  carageniuncllem2  40736  carageniuncl  40737  omege0  40747  omess0  40748  hoiprodcl  40761  ovnlerp  40776  ovnf  40777  ovn0lem  40779  ovnsubaddlem1  40784  hoiprodcl3  40794  hoidmvcl  40796  hoidmv1lelem3  40807  hoidmvlelem5  40813  ovnhoilem1  40815  ovolval5lem1  40866  pimrecltneg  40933  mod42tp1mod8  41519