Theorem 1xr 11240

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

Syntax hints:   ∈ wcel 2109  1c1 11076  ℝ^*cxr 11214

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-xr 11219

This theorem is referenced by:  xmulrid  13246  xmullid  13247  xmulm1  13248  x2times  13266  xov1plusxeqvd  13466  ico01fl0  13788  hashge1  14361  hashgt12el  14394  hashgt12el2  14395  hashgt23el  14396  sgn1  15065  fprodge1  15968  halfleoddlt  16339  isnzr2hash  20435  0ringnnzr  20441  xrsnsgrp  21326  leordtval2  23106  unirnblps  24314  unirnbl  24315  mopnex  24414  dscopn  24468  nmoid  24637  xrsmopn  24708  zdis  24712  metnrmlem1a  24754  metnrmlem1  24755  icopnfcnv  24847  icopnfhmeo  24848  iccpnfcnv  24849  iccpnfhmeo  24850  cncmet  25229  itg2monolem1  25658  itg2monolem3  25660  abelthlem2  26349  abelthlem3  26350  abelthlem5  26352  abelthlem7  26355  abelth  26358  dvlog2lem  26568  dvlog2  26569  logtayl  26576  logtayl2  26578  scvxcvx  26903  pntibndlem1  27507  pntibndlem2  27509  pntibnd  27511  pntlemc  27513  pnt  27532  padicabvf  27549  padicabvcxp  27550  elntg2  28919  nmopun  31950  pjnmopi  32084  xlt2addrd  32689  xdivrec  32854  xrsmulgzz  32954  xrnarchi  33145  rtelextdg2lem  33723  unitssxrge0  33897  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  hasheuni  34082  ddemeas  34233  omssubadd  34298  prob01  34411  lfuhgr2  35113  dnizeq0  36470  iccioo01  37322  broucube  37655  asindmre  37704  dvasin  37705  areacirclem1  37709  aks6d1c6lem1  42165  imo72b2  44168  cvgdvgrat  44309  supxrgelem  45340  xrlexaddrp  45355  infxr  45370  infleinflem2  45374  limsup10exlem  45777  limsup10ex  45778  liminf10ex  45779  salexct2  46344  salgencntex  46348  ovn0lem  46570  expnegico01  48511  regt1loggt0  48529  rege1logbrege0  48551  rege1logbzge0  48552  dignnld  48596  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  iooii  48910  i0oii  48912  sepfsepc  48920  seppcld  48922