Theorem 1xr 11168

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

Syntax hints:   ∈ wcel 2111  1c1 11004  ℝ^*cxr 11142

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 2113  ax-9 2121  ax-ext 2703  ax-1cn 11061  ax-icn 11062  ax-addcl 11063  ax-mulcl 11065  ax-mulrcl 11066  ax-i2m1 11071  ax-1ne0 11072  ax-rrecex 11075  ax-cnre 11076

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-xr 11147

This theorem is referenced by:  xmulrid  13175  xmullid  13176  xmulm1  13177  x2times  13195  xov1plusxeqvd  13395  ico01fl0  13720  hashge1  14293  hashgt12el  14326  hashgt12el2  14327  hashgt23el  14328  sgn1  14996  fprodge1  15899  halfleoddlt  16270  isnzr2hash  20432  0ringnnzr  20438  xrsnsgrp  21342  leordtval2  23125  unirnblps  24332  unirnbl  24333  mopnex  24432  dscopn  24486  nmoid  24655  xrsmopn  24726  zdis  24730  metnrmlem1a  24772  metnrmlem1  24773  icopnfcnv  24865  icopnfhmeo  24866  iccpnfcnv  24867  iccpnfhmeo  24868  cncmet  25247  itg2monolem1  25676  itg2monolem3  25678  abelthlem2  26367  abelthlem3  26368  abelthlem5  26370  abelthlem7  26373  abelth  26376  dvlog2lem  26586  dvlog2  26587  logtayl  26594  logtayl2  26596  scvxcvx  26921  pntibndlem1  27525  pntibndlem2  27527  pntibnd  27529  pntlemc  27531  pnt  27550  padicabvf  27567  padicabvcxp  27568  elntg2  28961  nmopun  31989  pjnmopi  32123  xlt2addrd  32737  xdivrec  32902  xrsmulgzz  32985  xrnarchi  33148  rtelextdg2lem  33734  unitssxrge0  33908  xrge0iifcnv  33941  xrge0iifiso  33943  xrge0iifhom  33945  hasheuni  34093  ddemeas  34244  omssubadd  34308  prob01  34421  lfuhgr2  35151  dnizeq0  36508  iccioo01  37360  broucube  37693  asindmre  37742  dvasin  37743  areacirclem1  37747  aks6d1c6lem1  42202  imo72b2  44204  cvgdvgrat  44345  supxrgelem  45375  xrlexaddrp  45390  infxr  45404  infleinflem2  45408  limsup10exlem  45809  limsup10ex  45810  liminf10ex  45811  salexct2  46376  salgencntex  46380  ovn0lem  46602  expnegico01  48549  regt1loggt0  48567  rege1logbrege0  48589  rege1logbzge0  48590  dignnld  48634  eenglngeehlnmlem1  48768  eenglngeehlnmlem2  48769  iooii  48948  i0oii  48950  sepfsepc  48958  seppcld  48960