Theorem 0xr 9422

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 9419	. 2 |- RR C_ RR*
2		0re 9378	. 2 |- 0 e. RR
3	1, 2	sselii 3348	1 |- 0 e. RR*

Syntax hints:   e. wcel 1756   RRcr 9273   0cc0 9274   RR*cxr 9409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-xr 9414

This theorem is referenced by:  0lepnf  11103  ge0gtmnf  11136  max0sub  11158  xlt0neg1  11181  xlt0neg2  11182  xle0neg1  11183  xle0neg2  11184  xaddf  11186  xaddid1  11201  xaddid2  11202  xaddge0  11213  xsubge0  11216  xposdif  11217  xmullem  11219  xmullem2  11220  xmul01  11222  xmul02  11223  xmulneg1  11224  xmulf  11227  xmulpnf1  11229  xmulasslem2  11237  xmulge0  11239  xmulasslem  11240  xlemul1a  11243  xadddi  11250  xadddi2  11252  ioopos  11364  ioorebas  11383  elxrge0  11386  0e0iccpnf  11388  xov1plusxeqvd  11423  rpsup  11697  hashgt0  12143  hashle00  12150  hashgt0elex  12151  sgn0  12570  sgnp  12571  sgnn  12575  ef01bndlem  13460  sin01bnd  13461  cos01bnd  13462  cos1bnd  13463  sinltx  13465  sin01gt0  13466  cos01gt0  13467  sin02gt0  13468  sincos1sgn  13469  sincos2sgn  13470  leordtval2  18791  pnfnei  18799  mnfnei  18800  psmetge0  19863  isxmet2d  19877  xmetge0  19894  xmetgt0  19908  prdsdsf  19917  prdsxmetlem  19918  xpsdsval  19931  blgt0  19949  xblss2ps  19951  xblss2  19952  xbln0  19964  prdsbl  20041  stdbdxmet  20065  stdbdmopn  20068  metusttoOLD  20107  metustto  20108  metustidOLD  20109  metustid  20110  metustexhalfOLD  20113  metustexhalf  20114  cfilucfilOLD  20119  cfilucfil  20120  blval2  20125  metuel2  20129  nmoge0  20275  nmo0  20289  cnblcld  20329  blssioo  20347  blcvx  20350  xrsxmet  20361  metdsf  20399  metds0  20401  metdseq0  20405  metnrmlem1a  20409  iccpnfcnv  20491  iccpnfhmeo  20492  xrhmeo  20493  pcoass  20571  iscfil2  20752  ovolmge0  20935  ovolge0  20939  ovolf  20940  ovolssnul  20945  ovolctb  20948  ovoliunnul  20965  ovolicopnf  20982  voliunlem3  21008  volsup  21012  ioorf  21028  volivth  21062  vitalilem4  21066  vitalilem5  21067  itg2ge0  21188  itg2const2  21194  itg2seq  21195  itg2monolem1  21203  itg2monolem2  21204  itg2monolem3  21205  itg2gt0  21213  dvne0  21458  mdegle0  21523  ply1remlem  21609  ply1rem  21610  plypf1  21655  aaliou3lem2  21784  aaliou3lem3  21785  taylfvallem1  21797  taylfval  21799  tayl0  21802  radcnvcl  21857  radcnvle  21860  pserulm  21862  psercnlem1  21865  pilem2  21892  sinhalfpilem  21900  sincosq1lem  21934  sincosq1sgn  21935  sincosq2sgn  21936  tangtx  21942  tanabsge  21943  sinq12gt0  21944  cosq14gt0  21947  sincos4thpi  21950  pige3  21954  cosordlem  21962  tanord1  21968  tanord  21969  efifo  21978  argimgt0  22036  argimlt0  22037  logccv  22083  loglesqr  22171  atantan  22293  rlimcnp  22334  rlimcnp2  22335  scvxcvx  22354  basellem1  22393  dchrisum0lem2a  22741  pntibndlem1  22813  pntibnd  22817  pntlemc  22819  pntlem3  22833  abvcxp  22839  padicabvf  22855  padicabvcxp  22856  ostth2  22861  ttgcontlem1  23082  nmooge0  24118  nmoo0  24142  nmlnogt0  24148  nmopge0  25266  nmopgt0  25267  nmfnge0  25282  nmop0  25341  nmfn0  25342  xraddge02  26001  xlt2addrd  26002  xrge0infss  26004  elxrge02  26058  xrs0  26087  xrge00  26098  xrge0addass  26102  xrge0neqmnf  26103  xrge0addgt0  26105  xrge0adddir  26106  fsumrp0cl  26109  metider  26273  unitssxrge0  26282  xrge0iifcnv  26315  xrge0iifcv  26316  xrge0iifiso  26317  xrge0iifhom  26319  xrge0mulc1cn  26323  pnfneige0  26333  lmxrge0  26334  esumnul  26454  esum0  26455  esumle  26460  esumlef  26465  esumcst  26466  esumsn  26467  esumpr2  26469  esumpinfval  26474  esumpinfsum  26478  esumpcvgval  26479  esumpmono  26480  hashf2  26485  esumcvg  26487  measle0  26574  voliune  26597  volfiniune  26598  ddemeas  26604  aean  26612  oms0  26662  prob01  26748  probmeasb  26765  dstfrvclim1  26812  sgncl  26873  sgn3da  26876  sgn0bi  26882  cvmliftlem10  27135  cvmliftlem13  27137  sinccvglem  27268  sin2h  28375  tan2h  28377  mblfinlem2  28382  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  mbfposadd  28392  itg2addnclem2  28397  itg2gt0cn  28400  ftc1anclem5  28424  ftc1anclem8  28427  dvasin  28433  areacirc  28442  rrnequiv  28687  idomrootle  29513  itgsin0pilem1  29743  stoweidlem46  29794  bj-flbi3  32374