Theorem 0xr 9551

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 9548	. 2 |- RR C_ RR*
2		0re 9507	. 2 |- 0 e. RR
3	1, 2	sselii 3414	1 |- 0 e. RR*

Syntax hints:   e. wcel 1826   RRcr 9402   0cc0 9403   RR*cxr 9538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-addrcl 9464  ax-mulcl 9465  ax-mulrcl 9466  ax-i2m1 9471  ax-1ne0 9472  ax-rnegex 9474  ax-rrecex 9475  ax-cnre 9476

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199  df-xr 9543

This theorem is referenced by:  0lepnf  11261  ge0gtmnf  11294  max0sub  11316  xlt0neg1  11339  xlt0neg2  11340  xle0neg1  11341  xle0neg2  11342  xaddf  11344  xaddid1  11359  xaddid2  11360  xaddge0  11371  xsubge0  11374  xposdif  11375  xmullem  11377  xmullem2  11378  xmul01  11380  xmul02  11381  xmulneg1  11382  xmulf  11385  xmulpnf1  11387  xmulasslem2  11395  xmulge0  11397  xmulasslem  11398  xlemul1a  11401  xadddi  11408  xadddi2  11410  ioopos  11522  ioorebas  11547  elxrge0  11550  0e0iccpnf  11552  xov1plusxeqvd  11587  ico01fl0  11853  rpsup  11893  addmodid  11939  hashgt0  12359  hashle00  12369  hashgt0elex  12370  sgn0  12924  sgnp  12925  sgnn  12929  ef01bndlem  13921  sin01bnd  13922  cos01bnd  13923  cos1bnd  13924  sinltx  13926  sin01gt0  13927  cos01gt0  13928  sin02gt0  13929  sincos1sgn  13930  sincos2sgn  13931  xrsmgm  18566  leordtval2  19799  pnfnei  19807  mnfnei  19808  psmetge0  20901  isxmet2d  20915  xmetge0  20932  xmetgt0  20946  prdsdsf  20955  prdsxmetlem  20956  xpsdsval  20969  blgt0  20987  xblss2ps  20989  xblss2  20990  xbln0  21002  prdsbl  21079  stdbdxmet  21103  stdbdmopn  21106  metusttoOLD  21145  metustto  21146  metustidOLD  21147  metustid  21148  metustexhalfOLD  21151  metustexhalf  21152  cfilucfilOLD  21157  cfilucfil  21158  blval2  21163  metuel2  21167  nmoge0  21313  nmo0  21327  cnblcld  21367  blssioo  21385  blcvx  21388  xrsxmet  21399  metdsf  21437  metds0  21439  metdseq0  21443  metnrmlem1a  21447  iccpnfcnv  21529  iccpnfhmeo  21530  xrhmeo  21531  pcoass  21609  iscfil2  21790  ovolmge0  21973  ovolge0  21977  ovolf  21978  ovolssnul  21983  ovolctb  21986  ovoliunnul  22003  ovolicopnf  22020  voliunlem3  22047  volsup  22051  ioorf  22067  volivth  22101  vitalilem4  22105  vitalilem5  22106  itg2ge0  22227  itg2const2  22233  itg2seq  22234  itg2monolem1  22242  itg2monolem2  22243  itg2monolem3  22244  itg2gt0  22252  dvne0  22497  mdegle0  22562  ply1remlem  22648  ply1rem  22649  plypf1  22694  aaliou3lem2  22824  aaliou3lem3  22825  taylfvallem1  22837  taylfval  22839  tayl0  22842  radcnvcl  22897  radcnvle  22900  pserulm  22902  psercnlem1  22905  pilem2  22932  sinhalfpilem  22941  sincosq1lem  22975  sincosq1sgn  22976  sincosq2sgn  22977  tangtx  22983  tanabsge  22984  sinq12gt0  22985  cosq14gt0  22988  sincos4thpi  22991  pige3  22995  cosordlem  23003  tanord1  23009  tanord  23010  efifo  23019  argimgt0  23084  argimlt0  23085  logccv  23131  loglesqrt  23219  atantan  23370  rlimcnp  23412  rlimcnp2  23413  scvxcvx  23432  basellem1  23471  dchrisum0lem2a  23819  pntibndlem1  23891  pntibnd  23895  pntlemc  23897  pntlem3  23911  abvcxp  23917  padicabvf  23933  padicabvcxp  23934  ostth2  23939  ttgcontlem1  24309  nmooge0  25799  nmoo0  25823  nmlnogt0  25829  nmopge0  26946  nmopgt0  26947  nmfnge0  26962  nmop0  27021  nmfn0  27022  xraddge02  27727  xlt2addrd  27728  xrge0infss  27730  dfrp2  27734  elxrge02  27781  xrs0  27816  xrge00  27827  xrge0addass  27831  xrge0neqmnf  27832  xrge0addgt0  27834  xrge0adddir  27835  fsumrp0cl  27838  metider  28027  unitssxrge0  28036  xrge0iifcnv  28069  xrge0iifcv  28070  xrge0iifiso  28071  xrge0iifhom  28073  xrge0mulc1cn  28077  pnfneige0  28087  lmxrge0  28088  esumgsum  28193  esumnul  28196  esum0  28197  esumle  28206  esumlef  28210  esumcst  28211  esumsnf  28212  esumpr2  28215  esumpinfval  28221  esumpinfsum  28225  esumpcvgval  28226  esumpmono  28227  hashf2  28232  esumcvg  28234  measle0  28335  voliune  28357  volfiniune  28358  ddemeas  28364  aean  28372  oms0  28424  prob01  28535  probmeasb  28552  dstfrvclim1  28599  sgncl  28660  sgn3da  28663  signsply0  28691  cvmliftlem10  28928  cvmliftlem13  28930  sinccvglem  29227  sin2h  30210  tan2h  30212  mblfinlem2  30217  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  mbfposadd  30227  itg2addnclem2  30233  itg2gt0cn  30236  ftc1anclem5  30260  ftc1anclem8  30263  dvasin  30269  areacirc  30278  rrnequiv  30497  idomrootle  31320  fprodge0  31763  sinaover2ne0  31834  itgsin0pilem1  31914  iblsplit  31931  stoweidlem46  31994  fourierdlem43  32098  fourierdlem44  32099  fourierdlem60  32115  fourierdlem61  32116  fourierdlem87  32142  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  sqwvfourb  32178  fourierswlem  32179  fouriersw  32180  etransclem23  32206  imo72b2  38522