Theorem 1xr 11233

Description: 1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)

Assertion

Ref	Expression
1xr	⊢ 1 ∈ ℝ*

Proof of Theorem 1xr

Step	Hyp	Ref	Expression
1		1re 11174	. 2 ⊢ 1 ∈ ℝ
2	1	rexri 11232	1 ⊢ 1 ∈ ℝ*

Syntax hints:   ∈ wcel 2109  1c1 11069  ℝ^*cxr 11207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-xr 11212

This theorem is referenced by:  xmulrid  13239  xmullid  13240  xmulm1  13241  x2times  13259  xov1plusxeqvd  13459  ico01fl0  13781  hashge1  14354  hashgt12el  14387  hashgt12el2  14388  hashgt23el  14389  sgn1  15058  fprodge1  15961  halfleoddlt  16332  isnzr2hash  20428  0ringnnzr  20434  xrsnsgrp  21319  leordtval2  23099  unirnblps  24307  unirnbl  24308  mopnex  24407  dscopn  24461  nmoid  24630  xrsmopn  24701  zdis  24705  metnrmlem1a  24747  metnrmlem1  24748  icopnfcnv  24840  icopnfhmeo  24841  iccpnfcnv  24842  iccpnfhmeo  24843  cncmet  25222  itg2monolem1  25651  itg2monolem3  25653  abelthlem2  26342  abelthlem3  26343  abelthlem5  26345  abelthlem7  26348  abelth  26351  dvlog2lem  26561  dvlog2  26562  logtayl  26569  logtayl2  26571  scvxcvx  26896  pntibndlem1  27500  pntibndlem2  27502  pntibnd  27504  pntlemc  27506  pnt  27525  padicabvf  27542  padicabvcxp  27543  elntg2  28912  nmopun  31943  pjnmopi  32077  xlt2addrd  32682  xdivrec  32847  xrsmulgzz  32947  xrnarchi  33138  rtelextdg2lem  33716  unitssxrge0  33890  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  hasheuni  34075  ddemeas  34226  omssubadd  34291  prob01  34404  lfuhgr2  35106  dnizeq0  36463  iccioo01  37315  broucube  37648  asindmre  37697  dvasin  37698  areacirclem1  37702  aks6d1c6lem1  42158  imo72b2  44161  cvgdvgrat  44302  supxrgelem  45333  xrlexaddrp  45348  infxr  45363  infleinflem2  45367  limsup10exlem  45770  limsup10ex  45771  liminf10ex  45772  salexct2  46337  salgencntex  46341  ovn0lem  46563  expnegico01  48507  regt1loggt0  48525  rege1logbrege0  48547  rege1logbzge0  48548  dignnld  48592  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  iooii  48906  i0oii  48908  sepfsepc  48916  seppcld  48918