Theorem 1xr 11292

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

Syntax hints:   ∈ wcel 2108  1c1 11128  ℝ^*cxr 11266

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-xr 11271

This theorem is referenced by:  xmulrid  13293  xmullid  13294  xmulm1  13295  x2times  13313  xov1plusxeqvd  13513  ico01fl0  13834  hashge1  14405  hashgt12el  14438  hashgt12el2  14439  hashgt23el  14440  sgn1  15109  fprodge1  16009  halfleoddlt  16379  isnzr2hash  20477  0ringnnzr  20483  xrsnsgrp  21368  leordtval2  23148  unirnblps  24356  unirnbl  24357  mopnex  24456  dscopn  24510  nmoid  24679  xrsmopn  24750  zdis  24754  metnrmlem1a  24796  metnrmlem1  24797  icopnfcnv  24889  icopnfhmeo  24890  iccpnfcnv  24891  iccpnfhmeo  24892  cncmet  25272  itg2monolem1  25701  itg2monolem3  25703  abelthlem2  26392  abelthlem3  26393  abelthlem5  26395  abelthlem7  26398  abelth  26401  dvlog2lem  26611  dvlog2  26612  logtayl  26619  logtayl2  26621  scvxcvx  26946  pntibndlem1  27550  pntibndlem2  27552  pntibnd  27554  pntlemc  27556  pnt  27575  padicabvf  27592  padicabvcxp  27593  elntg2  28910  nmopun  31941  pjnmopi  32075  xlt2addrd  32682  xdivrec  32847  xrsmulgzz  32947  xrnarchi  33128  rtelextdg2lem  33706  unitssxrge0  33877  xrge0iifcnv  33910  xrge0iifiso  33912  xrge0iifhom  33914  hasheuni  34062  ddemeas  34213  omssubadd  34278  prob01  34391  lfuhgr2  35087  dnizeq0  36439  iccioo01  37291  broucube  37624  asindmre  37673  dvasin  37674  areacirclem1  37678  aks6d1c6lem1  42129  imo72b2  44143  cvgdvgrat  44285  supxrgelem  45312  xrlexaddrp  45327  infxr  45342  infleinflem2  45346  limsup10exlem  45749  limsup10ex  45750  liminf10ex  45751  salexct2  46316  salgencntex  46320  ovn0lem  46542  expnegico01  48442  regt1loggt0  48464  rege1logbrege0  48486  rege1logbzge0  48487  dignnld  48531  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  iooii  48840  i0oii  48842  sepfsepc  48850  seppcld  48852