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

Theorem 0xr 9123
Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
Assertion
Ref Expression
0xr  |-  0  e.  RR*

Proof of Theorem 0xr
StepHypRef Expression
1 ressxr 9121 . 2  |-  RR  C_  RR*
2 0re 9083 . 2  |-  0  e.  RR
31, 2sselii 3337 1  |-  0  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   RRcr 8981   0cc0 8982   RR*cxr 9111
This theorem is referenced by:  nn0pnfge0  10720  ge0gtmnf  10752  max0sub  10774  xlt0neg1  10797  xlt0neg2  10798  xle0neg1  10799  xle0neg2  10800  xaddf  10802  xaddid1  10817  xaddid2  10818  xaddge0  10829  xsubge0  10832  xposdif  10833  xmullem  10835  xmullem2  10836  xmul01  10838  xmul02  10839  xmulneg1  10840  xmulf  10843  xmulpnf1  10845  xmulasslem2  10853  xmulge0  10855  xmulasslem  10856  xlemul1a  10859  xadddi  10866  xadddi2  10868  ioopos  10979  ioorebas  10998  elxrge0  11000  xov1plusxeqvd  11033  rpsup  11239  hashgt0  11654  hashle00  11661  hashgt0elex  11662  ef01bndlem  12777  sin01bnd  12778  cos01bnd  12779  cos1bnd  12780  sinltx  12782  sin01gt0  12783  cos01gt0  12784  sin02gt0  12785  sincos1sgn  12786  sincos2sgn  12787  pcge0  13227  xrge0subm  16731  leordtval2  17268  pnfnei  17276  mnfnei  17277  psmetge0  18335  isxmet2d  18349  xmetge0  18366  xmetgt0  18380  prdsdsf  18389  prdsxmetlem  18390  xpsdsval  18403  blgt0  18421  xblss2ps  18423  xblss2  18424  xbln0  18436  prdsbl  18513  stdbdxmet  18537  stdbdmopn  18540  metusttoOLD  18579  metustto  18580  metustidOLD  18581  metustid  18582  metustexhalfOLD  18585  metustexhalf  18586  cfilucfilOLD  18591  cfilucfil  18592  blval2  18597  metuel2  18601  nmoge0  18747  nmo0  18761  cnblcld  18801  blssioo  18818  blcvx  18821  xrsxmet  18832  metdsf  18870  metds0  18872  metdseq0  18876  metnrmlem1a  18880  iccpnfcnv  18961  iccpnfhmeo  18962  xrhmeo  18963  pcoass  19041  iscfil2  19211  ovolmge0  19365  ovolge0  19369  ovolf  19370  ovolssnul  19375  ovolctb  19378  ovoliunnul  19395  ovolicopnf  19412  voliunlem3  19438  volsup  19442  ioorf  19457  volivth  19491  vitalilem4  19495  vitalilem5  19496  itg2ge0  19619  itg2const2  19625  itg2seq  19626  itg2splitlem  19632  itg2split  19633  itg2monolem1  19634  itg2monolem2  19635  itg2monolem3  19636  itg2gt0  19644  itg2cnlem2  19646  itg2cn  19647  iblss  19688  itgle  19693  itgeqa  19697  ibladdlem  19703  iblabs  19712  iblabsr  19713  iblmulc2  19714  bddmulibl  19722  dvne0  19887  mdegle0  19992  ply1remlem  20077  ply1rem  20078  plypf1  20123  aaliou3lem2  20252  aaliou3lem3  20253  taylfvallem1  20265  taylfval  20267  tayl0  20270  radcnvcl  20325  radcnvle  20328  pserulm  20330  psercnlem1  20333  pilem2  20360  sinhalfpilem  20366  sincosq1lem  20397  sincosq1sgn  20398  sincosq2sgn  20399  tangtx  20405  tanabsge  20406  sinq12gt0  20407  cosq14gt0  20410  sincos4thpi  20413  pige3  20417  cosordlem  20425  tanord1  20431  tanord  20432  efifo  20441  argimgt0  20499  argimlt0  20500  logccv  20546  loglesqr  20634  atantan  20755  rlimcnp  20796  rlimcnp2  20797  rlimcnp3  20798  scvxcvx  20816  basellem1  20855  dchrisum0lem2a  21203  pntibndlem1  21275  pntibnd  21279  pntlemc  21281  pntlem3  21295  abvcxp  21301  padicabvf  21317  padicabvcxp  21318  ostth2  21323  nmooge0  22260  nmoo0  22284  nmlnogt0  22290  nmopge0  23406  nmopgt0  23407  nmfnge0  23422  nmop0  23481  nmfn0  23482  xraddge02  24115  xlt2addrd  24116  elxrge02  24170  xrs0  24189  xrge00  24200  xrge0addass  24203  xrge0neqmnf  24204  xrge0addgt0  24206  xrge0adddir  24207  fsumrp0cl  24209  metider  24281  unitssxrge0  24290  xrge0iifcnv  24311  xrge0iifcv  24312  xrge0iifiso  24313  xrge0iifhom  24315  xrge0mulc1cn  24319  pnfneige0  24328  lmxrge0  24329  esumnul  24435  esum0  24436  esumle  24441  esumlef  24446  esumcst  24447  esumsn  24448  esumpr2  24450  esumpinfval  24455  esumpfinvallem  24456  esumpinfsum  24459  esumpcvgval  24460  esumpmono  24461  esummulc1  24463  hashf2  24466  esumcvg  24468  measle0  24554  voliune  24577  volfiniune  24578  aean  24587  prob01  24663  probmeasb  24680  dstfrvclim1  24727  cvmliftlem10  24973  cvmliftlem13  24975  sinccvglem  25101  mblfinlem  26234  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  mbfposadd  26244  itg2addnclem2  26247  itg2gt0cn  26250  ibladdnclem  26251  iblabsnc  26259  iblmulc2nc  26260  bddiblnc  26265  ftc1anclem5  26274  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  dvreasin  26280  areacirc  26288  rrnequiv  26535  idomrootle  27479  itgsin0pilem1  27711  stoweidlem46  27762  sgn0  28456  sgnp  28457  sgnn  28461
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  df-xr 9116
  Copyright terms: Public domain W3C validator