Theorem 1xr 11195

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

Syntax hints:   ∈ wcel 2114  1c1 11030  ℝ^*cxr 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6448  df-fv 6500  df-ov 7363  df-xr 11174

This theorem is referenced by:  xmulrid  13222  xmullid  13223  xmulm1  13224  x2times  13242  xov1plusxeqvd  13442  nnge2recico01  13451  ico01fl0  13769  hashge1  14342  hashgt12el  14375  hashgt12el2  14376  hashgt23el  14377  sgn1  15045  fprodge1  15951  halfleoddlt  16322  isnzr2hash  20487  0ringnnzr  20493  xrsnsgrp  21397  leordtval2  23187  unirnblps  24394  unirnbl  24395  mopnex  24494  dscopn  24548  nmoid  24717  xrsmopn  24788  zdis  24792  metnrmlem1a  24834  metnrmlem1  24835  icopnfcnv  24919  icopnfhmeo  24920  iccpnfcnv  24921  iccpnfhmeo  24922  cncmet  25299  itg2monolem1  25727  itg2monolem3  25729  abelthlem2  26410  abelthlem3  26411  abelthlem5  26413  abelthlem7  26416  abelth  26419  dvlog2lem  26629  dvlog2  26630  logtayl  26637  logtayl2  26639  scvxcvx  26963  pntibndlem1  27566  pntibndlem2  27568  pntibnd  27570  pntlemc  27572  pnt  27591  padicabvf  27608  padicabvcxp  27609  elntg2  29068  nmopun  32100  pjnmopi  32234  xlt2addrd  32847  xdivrec  33001  xrsmulgzz  33084  xrnarchi  33260  vietadeg1  33737  rtelextdg2lem  33886  unitssxrge0  34060  xrge0iifcnv  34093  xrge0iifiso  34095  xrge0iifhom  34097  hasheuni  34245  ddemeas  34396  omssubadd  34460  prob01  34573  lfuhgr2  35317  dnizeq0  36751  iccioo01  37657  broucube  37989  asindmre  38038  dvasin  38039  areacirclem1  38043  aks6d1c6lem1  42623  imo72b2  44617  cvgdvgrat  44758  supxrgelem  45785  xrlexaddrp  45800  infxr  45814  infleinflem2  45818  limsup10exlem  46218  limsup10ex  46219  liminf10ex  46220  salexct2  46785  salgencntex  46789  ovn0lem  47011  flmrecm1  47803  expnegico01  49006  regt1loggt0  49024  rege1logbrege0  49046  rege1logbzge0  49047  dignnld  49091  eenglngeehlnmlem1  49225  eenglngeehlnmlem2  49226  iooii  49405  i0oii  49407  sepfsepc  49415  seppcld  49417