Theorem 1xr 11269

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

Syntax hints:   ∈ wcel 2143  1c1 11102  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-mulcl 11163  ax-mulrcl 11164  ax-i2m1 11169  ax-1ne0 11170  ax-rrecex 11173  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-xr 11248

This theorem is referenced by:  xmulrid  13306  xmullid  13307  xmulm1  13308  x2times  13326  xov1plusxeqvd  13526  nnge2recico01  13535  ico01fl0  13854  hashge1  14427  hashgt12el  14461  hashgt12el2  14462  hashgt23el  14463  sgn1  15131  sgnrn  15137  fprodge1  16051  halfleoddlt  16421  isnzr2hash  20604  0ringnnzr  20610  xrsnsgrp  21539  leordtval2  23350  unirnblps  24557  unirnbl  24558  mopnex  24657  dscopn  24711  nmoid  24880  xrsmopn  24951  zdis  24955  metnrmlem1a  24997  metnrmlem1  24998  icopnfcnv  25082  icopnfhmeo  25083  iccpnfcnv  25084  iccpnfhmeo  25085  cncmet  25462  itg2monolem1  25890  itg2monolem3  25892  abelthlem2  26576  abelthlem3  26577  abelthlem5  26579  abelthlem7  26582  abelth  26585  dvlog2lem  26798  dvlog2  26799  logtayl  26806  logtayl2  26808  scvxcvx  27131  pntibndlem1  27734  pntibndlem2  27736  pntibnd  27738  pntlemc  27740  pnt  27759  padicabvf  27776  padicabvcxp  27777  elntg2  29316  nmopun  32347  pjnmopi  32481  xlt2addrd  33085  xdivrec  33227  xrsmulgzz  33310  xrnarchi  33485  vietadeg1  33949  rtelextdg2lem  34097  unitssxrge0  34271  xrge0iifcnv  34304  xrge0iifiso  34306  xrge0iifhom  34308  hasheuni  34456  ddemeas  34607  omssubadd  34671  prob01  34784  lfuhgr2  35592  dnizeq0  37045  iccioo01  37954  broucube  38286  asindmre  38335  dvasin  38336  areacirclem1  38340  aks6d1c6lem1  42918  imo72b2  44881  cvgdvgrat  45006  supxrgelem  46036  xrlexaddrp  46051  infxr  46065  infleinflem2  46069  limsup10exlem  46469  limsup10ex  46470  liminf10ex  46471  salexct2  47036  salgencntex  47040  ovn0lem  47262  flmrecm1  48063  expnegico01  49281  regt1loggt0  49299  rege1logbrege0  49321  rege1logbzge0  49322  dignnld  49366  eenglngeehlnmlem1  49500  eenglngeehlnmlem2  49501  iooii  49679  i0oii  49681  sepfsepc  49689  seppcld  49691