Theorem 1xr 11202

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

Syntax hints:   ∈ wcel 2119  1c1 11037  ℝ^*cxr 11176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-mulcl 11098  ax-mulrcl 11099  ax-i2m1 11104  ax-1ne0 11105  ax-rrecex 11108  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-xr 11181

This theorem is referenced by:  xmulrid  13229  xmullid  13230  xmulm1  13231  x2times  13249  xov1plusxeqvd  13449  nnge2recico01  13458  ico01fl0  13776  hashge1  14349  hashgt12el  14382  hashgt12el2  14383  hashgt23el  14384  sgn1  15052  fprodge1  15958  halfleoddlt  16329  isnzr2hash  20498  0ringnnzr  20504  xrsnsgrp  21390  leordtval2  23202  unirnblps  24409  unirnbl  24410  mopnex  24509  dscopn  24563  nmoid  24732  xrsmopn  24803  zdis  24807  metnrmlem1a  24849  metnrmlem1  24850  icopnfcnv  24934  icopnfhmeo  24935  iccpnfcnv  24936  iccpnfhmeo  24937  cncmet  25314  itg2monolem1  25742  itg2monolem3  25744  abelthlem2  26422  abelthlem3  26423  abelthlem5  26425  abelthlem7  26428  abelth  26431  dvlog2lem  26641  dvlog2  26642  logtayl  26649  logtayl2  26651  scvxcvx  26974  pntibndlem1  27577  pntibndlem2  27579  pntibnd  27581  pntlemc  27583  pnt  27602  padicabvf  27619  padicabvcxp  27620  elntg2  29079  nmopun  32110  pjnmopi  32244  xlt2addrd  32858  xdivrec  33012  xrsmulgzz  33095  xrnarchi  33272  vietadeg1  33769  rtelextdg2lem  33917  unitssxrge0  34091  xrge0iifcnv  34124  xrge0iifiso  34126  xrge0iifhom  34128  hasheuni  34276  ddemeas  34427  omssubadd  34491  prob01  34604  lfuhgr2  35354  dnizeq0  36788  iccioo01  37696  broucube  38028  asindmre  38077  dvasin  38078  areacirclem1  38082  aks6d1c6lem1  42662  imo72b2  44623  cvgdvgrat  44764  supxrgelem  45789  xrlexaddrp  45804  infxr  45818  infleinflem2  45822  limsup10exlem  46222  limsup10ex  46223  liminf10ex  46224  salexct2  46789  salgencntex  46793  ovn0lem  47015  flmrecm1  47813  expnegico01  49016  regt1loggt0  49034  rege1logbrege0  49056  rege1logbzge0  49057  dignnld  49101  eenglngeehlnmlem1  49235  eenglngeehlnmlem2  49236  iooii  49415  i0oii  49417  sepfsepc  49425  seppcld  49427