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  37532  broucube  37855  asindmre  37904  dvasin  37905  areacirclem1  37909  aks6d1c6lem1  42424  imo72b2  44413  cvgdvgrat  44554  supxrgelem  45582  xrlexaddrp  45597  infxr  45611  infleinflem2  45615  limsup10exlem  46016  limsup10ex  46017  liminf10ex  46018  salexct2  46583  salgencntex  46587  ovn0lem  46809  expnegico01  48764  regt1loggt0  48782  rege1logbrege0  48804  rege1logbzge0  48805  dignnld  48849  eenglngeehlnmlem1  48983  eenglngeehlnmlem2  48984  iooii  49163  i0oii  49165  sepfsepc  49173  seppcld  49175