Theorem 1xr 11317

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

Syntax hints:   ∈ wcel 2105  1c1 11153  ℝ^*cxr 11291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-xr 11296

This theorem is referenced by:  xmulrid  13317  xmullid  13318  xmulm1  13319  x2times  13337  xov1plusxeqvd  13534  ico01fl0  13855  hashge1  14424  hashgt12el  14457  hashgt12el2  14458  hashgt23el  14459  sgn1  15127  fprodge1  16027  halfleoddlt  16395  isnzr2hash  20535  0ringnnzr  20541  xrsnsgrp  21437  leordtval2  23235  unirnblps  24444  unirnbl  24445  mopnex  24547  dscopn  24601  nmoid  24778  xrsmopn  24847  zdis  24851  metnrmlem1a  24893  metnrmlem1  24894  icopnfcnv  24986  icopnfhmeo  24987  iccpnfcnv  24988  iccpnfhmeo  24989  cncmet  25369  itg2monolem1  25799  itg2monolem3  25801  abelthlem2  26490  abelthlem3  26491  abelthlem5  26493  abelthlem7  26496  abelth  26499  dvlog2lem  26708  dvlog2  26709  logtayl  26716  logtayl2  26718  scvxcvx  27043  pntibndlem1  27647  pntibndlem2  27649  pntibnd  27651  pntlemc  27653  pnt  27672  padicabvf  27689  padicabvcxp  27690  elntg2  29014  nmopun  32042  pjnmopi  32176  xlt2addrd  32768  xdivrec  32893  xrsmulgzz  32993  xrnarchi  33173  rtelextdg2lem  33731  unitssxrge0  33860  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhom  33897  hasheuni  34065  ddemeas  34216  omssubadd  34281  prob01  34394  lfuhgr2  35102  dnizeq0  36457  iccioo01  37309  broucube  37640  asindmre  37689  dvasin  37690  areacirclem1  37694  aks6d1c6lem1  42151  imo72b2  44161  cvgdvgrat  44308  supxrgelem  45286  xrlexaddrp  45301  infxr  45316  infleinflem2  45320  limsup10exlem  45727  limsup10ex  45728  liminf10ex  45729  salexct2  46294  salgencntex  46298  ovn0lem  46520  expnegico01  48363  regt1loggt0  48385  rege1logbrege0  48407  rege1logbzge0  48408  dignnld  48452  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  iooii  48713  i0oii  48715  sepfsepc  48723  seppcld  48725