Theorem 1xr 11084

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

Syntax hints:   ∈ wcel 2104  1c1 10922  ℝ^*cxr 11058

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-1cn 10979  ax-icn 10980  ax-addcl 10981  ax-mulcl 10983  ax-mulrcl 10984  ax-i2m1 10989  ax-1ne0 10990  ax-rrecex 10993  ax-cnre 10994

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3306  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310  df-xr 11063

This theorem is referenced by:  xmulid1  13063  xmulid2  13064  xmulm1  13065  x2times  13083  xov1plusxeqvd  13280  ico01fl0  13589  hashge1  14153  hashgt12el  14186  hashgt12el2  14187  hashgt23el  14188  sgn1  14852  fprodge1  15754  halfleoddlt  16120  isnzr2hash  20584  0ringnnzr  20589  xrsnsgrp  20683  leordtval2  22412  unirnblps  23621  unirnbl  23622  mopnex  23724  dscopn  23778  nmoid  23955  xrsmopn  24024  zdis  24028  metnrmlem1a  24070  metnrmlem1  24071  icopnfcnv  24154  icopnfhmeo  24155  iccpnfcnv  24156  iccpnfhmeo  24157  cncmet  24535  itg2monolem1  24964  itg2monolem3  24966  abelthlem2  25640  abelthlem3  25641  abelthlem5  25643  abelthlem7  25646  abelth  25649  dvlog2lem  25856  dvlog2  25857  logtayl  25864  logtayl2  25866  scvxcvx  26184  pntibndlem1  26786  pntibndlem2  26788  pntibnd  26790  pntlemc  26792  pnt  26811  padicabvf  26828  padicabvcxp  26829  elntg2  27402  nmopun  30425  pjnmopi  30559  xlt2addrd  31130  xdivrec  31250  xrsmulgzz  31336  xrnarchi  31487  unitssxrge0  31899  xrge0iifcnv  31932  xrge0iifiso  31934  xrge0iifhom  31936  hasheuni  32102  ddemeas  32253  omssubadd  32316  prob01  32429  lfuhgr2  33129  dnizeq0  34704  iccioo01  35546  broucube  35859  asindmre  35908  dvasin  35909  areacirclem1  35913  imo72b2  41996  cvgdvgrat  42144  supxrgelem  43104  xrlexaddrp  43119  infxr  43134  infleinflem2  43138  limsup10exlem  43542  limsup10ex  43543  liminf10ex  43544  salexct2  44107  salgencntex  44111  ovn0lem  44333  expnegico01  46103  regt1loggt0  46126  rege1logbrege0  46148  rege1logbzge0  46149  dignnld  46193  eenglngeehlnmlem1  46327  eenglngeehlnmlem2  46328  iooii  46455  i0oii  46457  sepfsepc  46465  seppcld  46467