Theorem 1xr 11203

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

Syntax hints:   ∈ wcel 2114  1c1 11039  ℝ^*cxr 11177

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 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-xr 11182

This theorem is referenced by:  xmulrid  13206  xmullid  13207  xmulm1  13208  x2times  13226  xov1plusxeqvd  13426  ico01fl0  13751  hashge1  14324  hashgt12el  14357  hashgt12el2  14358  hashgt23el  14359  sgn1  15027  fprodge1  15930  halfleoddlt  16301  isnzr2hash  20464  0ringnnzr  20470  xrsnsgrp  21374  leordtval2  23168  unirnblps  24375  unirnbl  24376  mopnex  24475  dscopn  24529  nmoid  24698  xrsmopn  24769  zdis  24773  metnrmlem1a  24815  metnrmlem1  24816  icopnfcnv  24908  icopnfhmeo  24909  iccpnfcnv  24910  iccpnfhmeo  24911  cncmet  25290  itg2monolem1  25719  itg2monolem3  25721  abelthlem2  26410  abelthlem3  26411  abelthlem5  26413  abelthlem7  26416  abelth  26419  dvlog2lem  26629  dvlog2  26630  logtayl  26637  logtayl2  26639  scvxcvx  26964  pntibndlem1  27568  pntibndlem2  27570  pntibnd  27572  pntlemc  27574  pnt  27593  padicabvf  27610  padicabvcxp  27611  elntg2  29070  nmopun  32101  pjnmopi  32235  xlt2addrd  32849  xdivrec  33018  xrsmulgzz  33101  xrnarchi  33277  vietadeg1  33754  rtelextdg2lem  33903  unitssxrge0  34077  xrge0iifcnv  34110  xrge0iifiso  34112  xrge0iifhom  34114  hasheuni  34262  ddemeas  34413  omssubadd  34477  prob01  34590  lfuhgr2  35332  dnizeq0  36694  iccioo01  37576  broucube  37899  asindmre  37948  dvasin  37949  areacirclem1  37953  aks6d1c6lem1  42534  imo72b2  44522  cvgdvgrat  44663  supxrgelem  45690  xrlexaddrp  45705  infxr  45719  infleinflem2  45723  limsup10exlem  46124  limsup10ex  46125  liminf10ex  46126  salexct2  46691  salgencntex  46695  ovn0lem  46917  expnegico01  48872  regt1loggt0  48890  rege1logbrege0  48912  rege1logbzge0  48913  dignnld  48957  eenglngeehlnmlem1  49091  eenglngeehlnmlem2  49092  iooii  49271  i0oii  49273  sepfsepc  49281  seppcld  49283