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

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

Proof of Theorem 0xr
StepHypRef Expression
1 ressxr 9658 . 2
2 0re 9617 . 2
31, 2sselii 3500 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cr 9512  0cc0 9513   cxr 9648
This theorem is referenced by:  0lepnf  11369  ge0gtmnf  11402  max0sub  11424  xlt0neg1  11447  xlt0neg2  11448  xle0neg1  11449  xle0neg2  11450  xaddf  11452  xaddid1  11467  xaddid2  11468  xaddge0  11479  xsubge0  11482  xposdif  11483  xmullem  11485  xmullem2  11486  xmul01  11488  xmul02  11489  xmulneg1  11490  xmulf  11493  xmulpnf1  11495  xmulasslem2  11503  xmulge0  11505  xmulasslem  11506  xlemul1a  11509  xadddi  11516  xadddi2  11518  ioopos  11630  ioorebas  11655  elxrge0  11658  0e0iccpnf  11660  xov1plusxeqvd  11695  rpsup  11993  hashgt0  12456  hashle00  12465  hashgt0elex  12466  sgn0  12922  sgnp  12923  sgnn  12927  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  cos1bnd  13922  sinltx  13924  sin01gt0  13925  cos01gt0  13926  sin02gt0  13927  sincos1sgn  13928  sincos2sgn  13929  xrsmgm  18453  leordtval2  19713  pnfnei  19721  mnfnei  19722  psmetge0  20816  isxmet2d  20830  xmetge0  20847  xmetgt0  20861  prdsdsf  20870  prdsxmetlem  20871  xpsdsval  20884  blgt0  20902  xblss2ps  20904  xblss2  20905  xbln0  20917  prdsbl  20994  stdbdxmet  21018  stdbdmopn  21021  metusttoOLD  21060  metustto  21061  metustidOLD  21062  metustid  21063  metustexhalfOLD  21066  metustexhalf  21067  cfilucfilOLD  21072  cfilucfil  21073  blval2  21078  metuel2  21082  nmoge0  21228  nmo0  21242  cnblcld  21282  blssioo  21300  blcvx  21303  xrsxmet  21314  metdsf  21352  metds0  21354  metdseq0  21358  metnrmlem1a  21362  iccpnfcnv  21444  iccpnfhmeo  21445  xrhmeo  21446  pcoass  21524  iscfil2  21705  ovolmge0  21888  ovolge0  21892  ovolf  21893  ovolssnul  21898  ovolctb  21901  ovoliunnul  21918  ovolicopnf  21935  voliunlem3  21962  volsup  21966  ioorf  21982  volivth  22016  vitalilem4  22020  vitalilem5  22021  itg2ge0  22142  itg2const2  22148  itg2seq  22149  itg2monolem1  22157  itg2monolem2  22158  itg2monolem3  22159  itg2gt0  22167  dvne0  22412  mdegle0  22477  ply1remlem  22563  ply1rem  22564  plypf1  22609  aaliou3lem2  22739  aaliou3lem3  22740  taylfvallem1  22752  taylfval  22754  tayl0  22757  radcnvcl  22812  radcnvle  22815  pserulm  22817  psercnlem1  22820  pilem2  22847  sinhalfpilem  22856  sincosq1lem  22890  sincosq1sgn  22891  sincosq2sgn  22892  tangtx  22898  tanabsge  22899  sinq12gt0  22900  cosq14gt0  22903  sincos4thpi  22906  pige3  22910  cosordlem  22918  tanord1  22924  tanord  22925  efifo  22934  argimgt0  22997  argimlt0  22998  logccv  23044  loglesqrt  23132  atantan  23254  rlimcnp  23295  rlimcnp2  23296  scvxcvx  23315  basellem1  23354  dchrisum0lem2a  23702  pntibndlem1  23774  pntibnd  23778  pntlemc  23780  pntlem3  23794  abvcxp  23800  padicabvf  23816  padicabvcxp  23817  ostth2  23822  ttgcontlem1  24188  nmooge0  25682  nmoo0  25706  nmlnogt0  25712  nmopge0  26830  nmopgt0  26831  nmfnge0  26846  nmop0  26905  nmfn0  26906  xraddge02  27577  xlt2addrd  27578  xrge0infss  27580  elxrge02  27628  xrs0  27663  xrge00  27674  xrge0addass  27678  xrge0neqmnf  27679  xrge0addgt0  27681  xrge0adddir  27682  fsumrp0cl  27685  metider  27873  unitssxrge0  27882  xrge0iifcnv  27915  xrge0iifcv  27916  xrge0iifiso  27917  xrge0iifhom  27919  xrge0mulc1cn  27923  pnfneige0  27933  lmxrge0  27934  esumnul  28059  esum0  28060  esumle  28065  esumlef  28070  esumcst  28071  esumsn  28072  esumpr2  28074  esumpinfval  28079  esumpinfsum  28083  esumpcvgval  28084  esumpmono  28085  hashf2  28090  esumcvg  28092  measle0  28179  voliune  28201  volfiniune  28202  ddemeas  28208  aean  28216  oms0  28266  prob01  28352  probmeasb  28369  dstfrvclim1  28416  sgncl  28477  sgn3da  28480  signsply0  28508  cvmliftlem10  28739  cvmliftlem13  28741  sinccvglem  29038  sin2h  30045  tan2h  30047  mblfinlem2  30052  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  mbfposadd  30062  itg2addnclem2  30067  itg2gt0cn  30070  ftc1anclem5  30094  ftc1anclem8  30097  dvasin  30103  areacirc  30112  rrnequiv  30331  idomrootle  31152  fprodge0  31597  sinaover2ne0  31668  itgsin0pilem1  31748  iblsplit  31765  stoweidlem46  31828  fourierdlem43  31932  fourierdlem44  31933  fourierdlem60  31949  fourierdlem61  31950  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  etransclem23  32040  bj-flbi3  34608  imo72b2  37993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-xr 9653
  Copyright terms: Public domain W3C validator