Theorem 1xr 11191

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

Syntax hints:   ∈ wcel 2113  1c1 11027  ℝ^*cxr 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-xr 11170

This theorem is referenced by:  xmulrid  13194  xmullid  13195  xmulm1  13196  x2times  13214  xov1plusxeqvd  13414  ico01fl0  13739  hashge1  14312  hashgt12el  14345  hashgt12el2  14346  hashgt23el  14347  sgn1  15015  fprodge1  15918  halfleoddlt  16289  isnzr2hash  20452  0ringnnzr  20458  xrsnsgrp  21362  leordtval2  23156  unirnblps  24363  unirnbl  24364  mopnex  24463  dscopn  24517  nmoid  24686  xrsmopn  24757  zdis  24761  metnrmlem1a  24803  metnrmlem1  24804  icopnfcnv  24896  icopnfhmeo  24897  iccpnfcnv  24898  iccpnfhmeo  24899  cncmet  25278  itg2monolem1  25707  itg2monolem3  25709  abelthlem2  26398  abelthlem3  26399  abelthlem5  26401  abelthlem7  26404  abelth  26407  dvlog2lem  26617  dvlog2  26618  logtayl  26625  logtayl2  26627  scvxcvx  26952  pntibndlem1  27556  pntibndlem2  27558  pntibnd  27560  pntlemc  27562  pnt  27581  padicabvf  27598  padicabvcxp  27599  elntg2  29058  nmopun  32089  pjnmopi  32223  xlt2addrd  32839  xdivrec  33008  xrsmulgzz  33091  xrnarchi  33266  vietadeg1  33734  rtelextdg2lem  33883  unitssxrge0  34057  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  hasheuni  34242  ddemeas  34393  omssubadd  34457  prob01  34570  lfuhgr2  35313  dnizeq0  36675  iccioo01  37528  broucube  37851  asindmre  37900  dvasin  37901  areacirclem1  37905  aks6d1c6lem1  42420  imo72b2  44409  cvgdvgrat  44550  supxrgelem  45578  xrlexaddrp  45593  infxr  45607  infleinflem2  45611  limsup10exlem  46012  limsup10ex  46013  liminf10ex  46014  salexct2  46579  salgencntex  46583  ovn0lem  46805  expnegico01  48760  regt1loggt0  48778  rege1logbrege0  48800  rege1logbzge0  48801  dignnld  48845  eenglngeehlnmlem1  48979  eenglngeehlnmlem2  48980  iooii  49159  i0oii  49161  sepfsepc  49169  seppcld  49171