Theorem 1xr 11018

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

Syntax hints:   ∈ wcel 2109  1c1 10856  ℝ^*cxr 10992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-mulcl 10917  ax-mulrcl 10918  ax-i2m1 10923  ax-1ne0 10924  ax-rrecex 10927  ax-cnre 10928

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271  df-xr 10997

This theorem is referenced by:  xmulid1  12995  xmulid2  12996  xmulm1  12997  x2times  13015  xov1plusxeqvd  13212  ico01fl0  13520  hashge1  14085  hashgt12el  14118  hashgt12el2  14119  hashgt23el  14120  sgn1  14784  fprodge1  15686  halfleoddlt  16052  isnzr2hash  20516  0ringnnzr  20521  xrsnsgrp  20615  leordtval2  22344  unirnblps  23553  unirnbl  23554  mopnex  23656  dscopn  23710  nmoid  23887  xrsmopn  23956  zdis  23960  metnrmlem1a  24002  metnrmlem1  24003  icopnfcnv  24086  icopnfhmeo  24087  iccpnfcnv  24088  iccpnfhmeo  24089  cncmet  24467  itg2monolem1  24896  itg2monolem3  24898  abelthlem2  25572  abelthlem3  25573  abelthlem5  25575  abelthlem7  25578  abelth  25581  dvlog2lem  25788  dvlog2  25789  logtayl  25796  logtayl2  25798  scvxcvx  26116  pntibndlem1  26718  pntibndlem2  26720  pntibnd  26722  pntlemc  26724  pnt  26743  padicabvf  26760  padicabvcxp  26761  elntg2  27334  nmopun  30355  pjnmopi  30489  xlt2addrd  31060  xdivrec  31180  xrsmulgzz  31266  xrnarchi  31417  unitssxrge0  31829  xrge0iifcnv  31862  xrge0iifiso  31864  xrge0iifhom  31866  hasheuni  32032  ddemeas  32183  omssubadd  32246  prob01  32359  lfuhgr2  33059  dnizeq0  34634  iccioo01  35477  broucube  35790  asindmre  35839  dvasin  35840  areacirclem1  35844  imo72b2  41736  cvgdvgrat  41884  supxrgelem  42830  xrlexaddrp  42845  infxr  42860  infleinflem2  42864  limsup10exlem  43267  limsup10ex  43268  liminf10ex  43269  salexct2  43832  salgencntex  43836  ovn0lem  44057  expnegico01  45811  regt1loggt0  45834  rege1logbrege0  45856  rege1logbzge0  45857  dignnld  45901  eenglngeehlnmlem1  46035  eenglngeehlnmlem2  46036  iooii  46163  i0oii  46165  sepfsepc  46173  seppcld  46175