Theorem 1xr 11178

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

Syntax hints:   ∈ wcel 2113  1c1 11014  ℝ^*cxr 11152

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 2705  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-mulcl 11075  ax-mulrcl 11076  ax-i2m1 11081  ax-1ne0 11082  ax-rrecex 11085  ax-cnre 11086

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 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-xr 11157

This theorem is referenced by:  xmulrid  13180  xmullid  13181  xmulm1  13182  x2times  13200  xov1plusxeqvd  13400  ico01fl0  13725  hashge1  14298  hashgt12el  14331  hashgt12el2  14332  hashgt23el  14333  sgn1  15001  fprodge1  15904  halfleoddlt  16275  isnzr2hash  20436  0ringnnzr  20442  xrsnsgrp  21346  leordtval2  23128  unirnblps  24335  unirnbl  24336  mopnex  24435  dscopn  24489  nmoid  24658  xrsmopn  24729  zdis  24733  metnrmlem1a  24775  metnrmlem1  24776  icopnfcnv  24868  icopnfhmeo  24869  iccpnfcnv  24870  iccpnfhmeo  24871  cncmet  25250  itg2monolem1  25679  itg2monolem3  25681  abelthlem2  26370  abelthlem3  26371  abelthlem5  26373  abelthlem7  26376  abelth  26379  dvlog2lem  26589  dvlog2  26590  logtayl  26597  logtayl2  26599  scvxcvx  26924  pntibndlem1  27528  pntibndlem2  27530  pntibnd  27532  pntlemc  27534  pnt  27553  padicabvf  27570  padicabvcxp  27571  elntg2  28965  nmopun  31996  pjnmopi  32130  xlt2addrd  32746  xdivrec  32914  xrsmulgzz  32997  xrnarchi  33160  rtelextdg2lem  33760  unitssxrge0  33934  xrge0iifcnv  33967  xrge0iifiso  33969  xrge0iifhom  33971  hasheuni  34119  ddemeas  34270  omssubadd  34334  prob01  34447  lfuhgr2  35184  dnizeq0  36540  iccioo01  37392  broucube  37714  asindmre  37763  dvasin  37764  areacirclem1  37768  aks6d1c6lem1  42283  imo72b2  44289  cvgdvgrat  44430  supxrgelem  45460  xrlexaddrp  45475  infxr  45489  infleinflem2  45493  limsup10exlem  45894  limsup10ex  45895  liminf10ex  45896  salexct2  46461  salgencntex  46465  ovn0lem  46687  expnegico01  48643  regt1loggt0  48661  rege1logbrege0  48683  rege1logbzge0  48684  dignnld  48728  eenglngeehlnmlem1  48862  eenglngeehlnmlem2  48863  iooii  49042  i0oii  49044  sepfsepc  49052  seppcld  49054