Theorem 1xr 11223

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

Syntax hints:   ∈ wcel 2106  1c1 11061  ℝ^*cxr 11197

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 2702  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-mulcl 11122  ax-mulrcl 11123  ax-i2m1 11128  ax-1ne0 11129  ax-rrecex 11132  ax-cnre 11133

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 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-xr 11202

This theorem is referenced by:  xmulrid  13208  xmullid  13209  xmulm1  13210  x2times  13228  xov1plusxeqvd  13425  ico01fl0  13734  hashge1  14299  hashgt12el  14332  hashgt12el2  14333  hashgt23el  14334  sgn1  14989  fprodge1  15889  halfleoddlt  16255  isnzr2hash  20208  0ringnnzr  20212  xrsnsgrp  20870  leordtval2  22600  unirnblps  23809  unirnbl  23810  mopnex  23912  dscopn  23966  nmoid  24143  xrsmopn  24212  zdis  24216  metnrmlem1a  24258  metnrmlem1  24259  icopnfcnv  24342  icopnfhmeo  24343  iccpnfcnv  24344  iccpnfhmeo  24345  cncmet  24723  itg2monolem1  25152  itg2monolem3  25154  abelthlem2  25828  abelthlem3  25829  abelthlem5  25831  abelthlem7  25834  abelth  25837  dvlog2lem  26044  dvlog2  26045  logtayl  26052  logtayl2  26054  scvxcvx  26372  pntibndlem1  26974  pntibndlem2  26976  pntibnd  26978  pntlemc  26980  pnt  26999  padicabvf  27016  padicabvcxp  27017  elntg2  27997  nmopun  31019  pjnmopi  31153  xlt2addrd  31731  xdivrec  31853  xrsmulgzz  31939  xrnarchi  32090  unitssxrge0  32570  xrge0iifcnv  32603  xrge0iifiso  32605  xrge0iifhom  32607  hasheuni  32773  ddemeas  32924  omssubadd  32989  prob01  33102  lfuhgr2  33799  dnizeq0  35014  iccioo01  35871  broucube  36185  asindmre  36234  dvasin  36235  areacirclem1  36239  imo72b2  42567  cvgdvgrat  42715  supxrgelem  43692  xrlexaddrp  43707  infxr  43722  infleinflem2  43726  limsup10exlem  44133  limsup10ex  44134  liminf10ex  44135  salexct2  44700  salgencntex  44704  ovn0lem  44926  expnegico01  46719  regt1loggt0  46742  rege1logbrege0  46764  rege1logbzge0  46765  dignnld  46809  eenglngeehlnmlem1  46943  eenglngeehlnmlem2  46944  iooii  47070  i0oii  47072  sepfsepc  47080  seppcld  47082