Theorem 1xr 11238

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 11178	. 2 ⊢ 1 ∈ ℝ
2	1	rexri 11237	1 ⊢ 1 ∈ ℝ*

Syntax hints:   ∈ wcel 2141  1c1 11071  ℝ^*cxr 11212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11128  ax-icn 11129  ax-addcl 11130  ax-mulcl 11132  ax-mulrcl 11133  ax-i2m1 11138  ax-1ne0 11139  ax-rrecex 11142  ax-cnre 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6473  df-fv 6525  df-ov 7395  df-xr 11217

This theorem is referenced by:  xmulrid  13279  xmullid  13280  xmulm1  13281  x2times  13299  xov1plusxeqvd  13499  nnge2recico01  13508  ico01fl0  13826  hashge1  14399  hashgt12el  14432  hashgt12el2  14433  hashgt23el  14434  sgn1  15102  fprodge1  16008  halfleoddlt  16379  isnzr2hash  20548  0ringnnzr  20554  xrsnsgrp  21440  leordtval2  23252  unirnblps  24459  unirnbl  24460  mopnex  24559  dscopn  24613  nmoid  24782  xrsmopn  24853  zdis  24857  metnrmlem1a  24899  metnrmlem1  24900  icopnfcnv  24984  icopnfhmeo  24985  iccpnfcnv  24986  iccpnfhmeo  24987  cncmet  25364  itg2monolem1  25792  itg2monolem3  25794  abelthlem2  26472  abelthlem3  26473  abelthlem5  26475  abelthlem7  26478  abelth  26481  dvlog2lem  26694  dvlog2  26695  logtayl  26702  logtayl2  26704  scvxcvx  27027  pntibndlem1  27630  pntibndlem2  27632  pntibnd  27634  pntlemc  27636  pnt  27655  padicabvf  27672  padicabvcxp  27673  elntg2  29132  nmopun  32163  pjnmopi  32297  xlt2addrd  32911  xdivrec  33065  xrsmulgzz  33148  xrnarchi  33325  vietadeg1  33836  rtelextdg2lem  33984  unitssxrge0  34158  xrge0iifcnv  34191  xrge0iifiso  34193  xrge0iifhom  34195  hasheuni  34343  ddemeas  34494  omssubadd  34558  prob01  34671  lfuhgr2  35433  dnizeq0  36877  iccioo01  37785  broucube  38117  asindmre  38166  dvasin  38167  areacirclem1  38171  aks6d1c6lem1  42751  imo72b2  44712  cvgdvgrat  44853  supxrgelem  45877  xrlexaddrp  45892  infxr  45906  infleinflem2  45910  limsup10exlem  46310  limsup10ex  46311  liminf10ex  46312  salexct2  46877  salgencntex  46881  ovn0lem  47103  flmrecm1  47901  expnegico01  49104  regt1loggt0  49122  rege1logbrege0  49144  rege1logbzge0  49145  dignnld  49189  eenglngeehlnmlem1  49323  eenglngeehlnmlem2  49324  iooii  49503  i0oii  49505  sepfsepc  49513  seppcld  49515