Theorem 1xr 11193

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

Syntax hints:   ∈ wcel 2109  1c1 11029  ℝ^*cxr 11167

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 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rrecex 11100  ax-cnre 11101

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 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-xr 11172

This theorem is referenced by:  xmulrid  13199  xmullid  13200  xmulm1  13201  x2times  13219  xov1plusxeqvd  13419  ico01fl0  13741  hashge1  14314  hashgt12el  14347  hashgt12el2  14348  hashgt23el  14349  sgn1  15017  fprodge1  15920  halfleoddlt  16291  isnzr2hash  20422  0ringnnzr  20428  xrsnsgrp  21332  leordtval2  23115  unirnblps  24323  unirnbl  24324  mopnex  24423  dscopn  24477  nmoid  24646  xrsmopn  24717  zdis  24721  metnrmlem1a  24763  metnrmlem1  24764  icopnfcnv  24856  icopnfhmeo  24857  iccpnfcnv  24858  iccpnfhmeo  24859  cncmet  25238  itg2monolem1  25667  itg2monolem3  25669  abelthlem2  26358  abelthlem3  26359  abelthlem5  26361  abelthlem7  26364  abelth  26367  dvlog2lem  26577  dvlog2  26578  logtayl  26585  logtayl2  26587  scvxcvx  26912  pntibndlem1  27516  pntibndlem2  27518  pntibnd  27520  pntlemc  27522  pnt  27541  padicabvf  27558  padicabvcxp  27559  elntg2  28948  nmopun  31976  pjnmopi  32110  xlt2addrd  32715  xdivrec  32880  xrsmulgzz  32976  xrnarchi  33136  rtelextdg2lem  33692  unitssxrge0  33866  xrge0iifcnv  33899  xrge0iifiso  33901  xrge0iifhom  33903  hasheuni  34051  ddemeas  34202  omssubadd  34267  prob01  34380  lfuhgr2  35091  dnizeq0  36448  iccioo01  37300  broucube  37633  asindmre  37682  dvasin  37683  areacirclem1  37687  aks6d1c6lem1  42143  imo72b2  44145  cvgdvgrat  44286  supxrgelem  45317  xrlexaddrp  45332  infxr  45347  infleinflem2  45351  limsup10exlem  45754  limsup10ex  45755  liminf10ex  45756  salexct2  46321  salgencntex  46325  ovn0lem  46547  expnegico01  48504  regt1loggt0  48522  rege1logbrege0  48544  rege1logbzge0  48545  dignnld  48589  eenglngeehlnmlem1  48723  eenglngeehlnmlem2  48724  iooii  48903  i0oii  48905  sepfsepc  48913  seppcld  48915