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

Theorem 1xr 11213
Description: 1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
Assertion
Ref Expression
1xr 1 ∈ ℝ*

Proof of Theorem 1xr
StepHypRef Expression
1 1re 11154 . 2 1 ∈ ℝ
21rexri 11212 1 1 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  1c1 11051  *cxr 11187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-1cn 11108  ax-icn 11109  ax-addcl 11110  ax-mulcl 11112  ax-mulrcl 11113  ax-i2m1 11118  ax-1ne0 11119  ax-rrecex 11122  ax-cnre 11123
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7359  df-xr 11192
This theorem is referenced by:  xmulid1  13197  xmulid2  13198  xmulm1  13199  x2times  13217  xov1plusxeqvd  13414  ico01fl0  13723  hashge1  14288  hashgt12el  14321  hashgt12el2  14322  hashgt23el  14323  sgn1  14976  fprodge1  15877  halfleoddlt  16243  isnzr2hash  20732  0ringnnzr  20737  xrsnsgrp  20831  leordtval2  22561  unirnblps  23770  unirnbl  23771  mopnex  23873  dscopn  23927  nmoid  24104  xrsmopn  24173  zdis  24177  metnrmlem1a  24219  metnrmlem1  24220  icopnfcnv  24303  icopnfhmeo  24304  iccpnfcnv  24305  iccpnfhmeo  24306  cncmet  24684  itg2monolem1  25113  itg2monolem3  25115  abelthlem2  25789  abelthlem3  25790  abelthlem5  25792  abelthlem7  25795  abelth  25798  dvlog2lem  26005  dvlog2  26006  logtayl  26013  logtayl2  26015  scvxcvx  26333  pntibndlem1  26935  pntibndlem2  26937  pntibnd  26939  pntlemc  26941  pnt  26960  padicabvf  26977  padicabvcxp  26978  elntg2  27932  nmopun  30954  pjnmopi  31088  xlt2addrd  31658  xdivrec  31778  xrsmulgzz  31864  xrnarchi  32015  unitssxrge0  32472  xrge0iifcnv  32505  xrge0iifiso  32507  xrge0iifhom  32509  hasheuni  32675  ddemeas  32826  omssubadd  32891  prob01  33004  lfuhgr2  33703  dnizeq0  34929  iccioo01  35789  broucube  36103  asindmre  36152  dvasin  36153  areacirclem1  36157  imo72b2  42427  cvgdvgrat  42575  supxrgelem  43547  xrlexaddrp  43562  infxr  43577  infleinflem2  43581  limsup10exlem  43985  limsup10ex  43986  liminf10ex  43987  salexct2  44552  salgencntex  44556  ovn0lem  44778  expnegico01  46571  regt1loggt0  46594  rege1logbrege0  46616  rege1logbzge0  46617  dignnld  46661  eenglngeehlnmlem1  46795  eenglngeehlnmlem2  46796  iooii  46922  i0oii  46924  sepfsepc  46932  seppcld  46934
  Copyright terms: Public domain W3C validator