Theorem 1xr 11204

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 11203	1 ⊢ 1 ∈ ℝ*

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

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-xr 11183

This theorem is referenced by:  xmulrid  13231  xmullid  13232  xmulm1  13233  x2times  13251  xov1plusxeqvd  13451  nnge2recico01  13460  ico01fl0  13778  hashge1  14351  hashgt12el  14384  hashgt12el2  14385  hashgt23el  14386  sgn1  15054  fprodge1  15960  halfleoddlt  16331  isnzr2hash  20496  0ringnnzr  20502  xrsnsgrp  21388  leordtval2  23177  unirnblps  24384  unirnbl  24385  mopnex  24484  dscopn  24538  nmoid  24707  xrsmopn  24778  zdis  24782  metnrmlem1a  24824  metnrmlem1  24825  icopnfcnv  24909  icopnfhmeo  24910  iccpnfcnv  24911  iccpnfhmeo  24912  cncmet  25289  itg2monolem1  25717  itg2monolem3  25719  abelthlem2  26397  abelthlem3  26398  abelthlem5  26400  abelthlem7  26403  abelth  26406  dvlog2lem  26616  dvlog2  26617  logtayl  26624  logtayl2  26626  scvxcvx  26949  pntibndlem1  27552  pntibndlem2  27554  pntibnd  27556  pntlemc  27558  pnt  27577  padicabvf  27594  padicabvcxp  27595  elntg2  29054  nmopun  32085  pjnmopi  32219  xlt2addrd  32832  xdivrec  32986  xrsmulgzz  33069  xrnarchi  33245  vietadeg1  33722  rtelextdg2lem  33870  unitssxrge0  34044  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  hasheuni  34229  ddemeas  34380  omssubadd  34444  prob01  34557  lfuhgr2  35301  dnizeq0  36735  iccioo01  37643  broucube  37975  asindmre  38024  dvasin  38025  areacirclem1  38029  aks6d1c6lem1  42609  imo72b2  44599  cvgdvgrat  44740  supxrgelem  45767  xrlexaddrp  45782  infxr  45796  infleinflem2  45800  limsup10exlem  46200  limsup10ex  46201  liminf10ex  46202  salexct2  46767  salgencntex  46771  ovn0lem  46993  flmrecm1  47791  expnegico01  48994  regt1loggt0  49012  rege1logbrege0  49034  rege1logbzge0  49035  dignnld  49079  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  iooii  49393  i0oii  49395  sepfsepc  49403  seppcld  49405