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

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

Proof of Theorem 0xr
StepHypRef Expression
1 ressxr 10121 . 2 ℝ ⊆ ℝ*
2 0re 10078 . 2 0 ∈ ℝ
31, 2sselii 3633 1 0 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  cr 9973  0cc0 9974  *cxr 10111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-xr 10116
This theorem is referenced by:  0lepnf  12004  ge0gtmnf  12041  max0sub  12065  xlt0neg1  12088  xlt0neg2  12089  xle0neg1  12090  xle0neg2  12091  xaddf  12093  xaddid1  12110  xaddid2  12111  xnn0xadd0  12115  xaddge0  12126  xsubge0  12129  xposdif  12130  xmullem  12132  xmullem2  12133  xmul01  12135  xmul02  12136  xmulneg1  12137  xmulf  12140  xmulpnf1  12142  xmulasslem2  12150  xmulge0  12152  xmulasslem  12153  xlemul1a  12156  xadddi  12163  xadddi2  12165  ioopos  12288  ioorebas  12313  xrge0neqmnf  12314  elxrge0  12319  0e0iccpnf  12321  xov1plusxeqvd  12356  xnn0xrge0  12363  ico01fl0  12660  rpsup  12705  addmodid  12758  hashgt0  13215  hashle00  13226  hashgt0elex  13227  sgn0  13873  sgnp  13874  sgnn  13878  fprodge0  14768  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  cos1bnd  14961  sinltx  14963  sin01gt0  14964  cos01gt0  14965  sin02gt0  14966  sincos1sgn  14967  sincos2sgn  14968  halfleoddlt  15133  xrsmgm  19829  leordtval2  21064  pnfnei  21072  mnfnei  21073  psmetge0  22164  isxmet2d  22179  xmetge0  22196  xmetgt0  22210  prdsdsf  22219  prdsxmetlem  22220  xpsdsval  22233  blgt0  22251  xblss2ps  22253  xblss2  22254  xbln0  22266  prdsbl  22343  stdbdxmet  22367  stdbdmopn  22370  metustto  22405  metustid  22406  metustexhalf  22408  cfilucfil  22411  blval2  22414  metuel2  22417  nmoge0  22572  nmo0  22586  cnblcld  22625  blssioo  22645  blcvx  22648  xrsxmet  22659  metdsf  22698  metds0  22700  metdseq0  22704  metnrmlem1a  22708  iccpnfcnv  22790  iccpnfhmeo  22791  xrhmeo  22792  pcoass  22870  iscfil2  23110  ovolmge0  23291  ovolge0  23295  ovolf  23296  ovolssnul  23301  ovolctb  23304  ovoliunnul  23321  ovolicopnf  23338  voliunlem3  23366  volsup  23370  ioorf  23387  volivth  23421  vitalilem4  23425  vitalilem5  23426  itg2ge0  23547  itg2const2  23553  itg2seq  23554  itg2monolem1  23562  itg2monolem2  23563  itg2monolem3  23564  itg2gt0  23572  dvne0  23819  mdegle0  23882  ply1remlem  23967  ply1rem  23968  plypf1  24013  aaliou3lem2  24143  aaliou3lem3  24144  taylfvallem1  24156  taylfval  24158  tayl0  24161  radcnvcl  24216  radcnvle  24219  pserulm  24221  psercnlem1  24224  pilem2  24251  sinhalfpilem  24260  sincosq1lem  24294  sincosq1sgn  24295  sincosq2sgn  24296  tangtx  24302  tanabsge  24303  sinq12gt0  24304  cosq14gt0  24307  sincos4thpi  24310  pige3  24314  cosordlem  24322  tanord1  24328  tanord  24329  efifo  24338  argimgt0  24403  argimlt0  24404  logccv  24454  loglesqrt  24544  atantan  24695  rlimcnp  24737  rlimcnp2  24738  scvxcvx  24757  basellem1  24852  dchrisum0lem2a  25251  pntibndlem1  25323  pntibnd  25327  pntlemc  25329  pntlem3  25343  abvcxp  25349  padicabvf  25365  padicabvcxp  25366  ostth2  25371  ttgcontlem1  25810  nmooge0  27750  nmoo0  27774  nmlnogt0  27780  nmopge0  28898  nmopgt0  28899  nmfnge0  28914  nmop0  28973  nmfn0  28974  xraddge02  29649  xlt2addrd  29651  xrge0infss  29653  dfrp2  29660  elxrge02  29768  xrs0  29803  xrge00  29814  xrge0addass  29818  xrge0addgt0  29819  xrge0adddir  29820  fsumrp0cl  29823  metider  30065  unitssxrge0  30074  xrge0iifcnv  30107  xrge0iifcv  30108  xrge0iifiso  30109  xrge0iifhom  30111  xrge0mulc1cn  30115  pnfneige0  30125  lmxrge0  30126  esumgsum  30235  esumnul  30238  esum0  30239  esumle  30248  esumlef  30252  esumcst  30253  esumsnf  30254  esumpr2  30257  esumpinfval  30263  esumpinfsum  30267  esumpcvgval  30268  esumpmono  30269  hashf2  30274  esumcvg  30276  measle0  30399  voliune  30420  volfiniune  30421  ddemeas  30427  aean  30435  oms0  30487  prob01  30603  probmeasb  30620  dstfrvclim1  30667  sgncl  30728  sgn3da  30731  signsply0  30756  chtvalz  30835  hgt750lemf  30859  cvmliftlem10  31402  cvmliftlem13  31404  sinccvglem  31692  dnizeq0  32590  sin2h  33529  tan2h  33531  broucube  33573  mblfinlem2  33577  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  mbfposadd  33587  itg2addnclem2  33592  itg2gt0cn  33595  ftc1anclem5  33619  ftc1anclem8  33622  dvasin  33626  areacirc  33635  rrnequiv  33764  idomrootle  38090  imo72b2  38792  absfico  39724  xadd0ge  39849  xrge0nemnfd  39861  xralrple2  39883  xrpnf  40029  pnfel0pnf  40072  ge0nemnf2  40073  ge0xrre  40076  sqrlearg  40098  fsumge0cl  40123  limsup10ex  40323  liminf10ex  40324  sinaover2ne0  40397  itgsin0pilem1  40483  iblsplit  40500  stoweidlem46  40581  fourierdlem43  40685  fourierdlem44  40686  fourierdlem60  40701  fourierdlem61  40702  fourierdlem87  40728  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  etransclem23  40792  salexct2  40875  fge0npnf  40902  fge0iccico  40905  gsumge0cl  40906  sge0z  40910  sge00  40911  sge0sn  40914  sge0tsms  40915  sge0cl  40916  sge0f1o  40917  sge0ge0  40919  sge0repnf  40921  sge0fsum  40922  sge0pr  40929  sge0ssre  40932  sge0prle  40936  sge0p1  40949  sge0iunmptlemre  40950  sge0rpcpnf  40956  sge0rernmpt  40957  sge0isum  40962  sge0ad2en  40966  sge0xaddlem2  40969  sge0uzfsumgt  40979  sge0seq  40981  sge0reuz  40982  voliunsge0lem  41007  meage0  41010  meassre  41012  meale0eq0  41013  meaiuninclem  41015  omessre  41045  omeiunltfirp  41054  carageniuncllem2  41057  carageniuncl  41058  omege0  41068  omess0  41069  hoiprodcl  41082  ovnlerp  41097  ovnf  41098  ovn0lem  41100  ovnsubaddlem1  41105  hoiprodcl3  41115  hoidmvcl  41117  hoidmv1lelem3  41128  hoidmvlelem5  41134  ovnhoilem1  41136  ovolval5lem1  41187  pimrecltneg  41254  mod42tp1mod8  41844
  Copyright terms: Public domain W3C validator