Theorem 1xr 11371

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

This proof depends on syntax axioms:   ∈ wcel 2144  1c1 11204  ℝ^*cxr 11345

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-mulcl 11265  ax-mulrcl 11266  ax-i2m1 11271  ax-1ne0 11272  ax-rrecex 11275  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-xr 11350

This theorem is used by:  xmulrid  13412  xmullid  13413  xmulm1  13414  x2times  13432  xov1plusxeqvd  13632  nnge2recico01  13641  ico01fl0  13962  hashge1  14536  hashgt12el  14570  hashgt12el2  14571  hashgt23el  14572  sgn1  15250  sgnrn  15256  fprodge1  16167  halfleoddlt  16537  isnzr2hash  20775  0ringnnzr  20781  xrsnsgrp  21719  leordtval2  23535  unirnblps  24743  unirnbl  24744  mopnex  24843  dscopn  24897  nmoid  25066  xrsmopn  25137  zdis  25141  metnrmlem1a  25183  metnrmlem1  25184  icopnfcnv  25268  icopnfhmeo  25269  iccpnfcnv  25270  iccpnfhmeo  25271  cncmet  25648  itg2monolem1  26076  itg2monolem3  26078  abelthlem2  26764  abelthlem3  26765  abelthlem5  26767  abelthlem7  26770  abelth  26773  cos0pilt1  26865  dvlog2lem  26985  dvlog2  26986  logtayl  26993  logtayl2  26995  scvxcvx  27318  pntibndlem1  27921  pntibndlem2  27923  pntibnd  27925  pntlemc  27927  pnt  27946  padicabvf  27963  padicabvcxp  27964  elntg2  29568  lfuhgr2  29732  nmopun  32621  pjnmopi  32755  xlt2addrd  33397  xdivrec  33539  xrsmulgzz  33616  xrnarchi  33791  vietadeg1  34256  rtelextdg2lem  34404  unitssxrge0  34578  xrge0iifcnv  34611  xrge0iifiso  34613  xrge0iifhom  34615  hasheuni  34763  ddemeas  34915  omssubadd  34978  prob01  35091  dnizeq0  37433  iccioo01  38343  broucube  38665  asindmre  38714  dvasin  38715  areacirclem1  38719  aks6d1c6lem1  43313  imo72b2  45265  cvgdvgrat  45390  supxrgelem  46442  xrlexaddrp  46457  infxr  46471  infleinflem2  46475  limsup10exlem  46875  limsup10ex  46876  liminf10ex  46877  salexct2  47442  salgencntex  47446  ovn0lem  47668  flmrecm1  48506  expnegico01  49723  regt1loggt0  49741  rege1logbrege0  49763  rege1logbzge0  49764  dignnld  49808  eenglngeehlnmlem1  49943  eenglngeehlnmlem2  49944  iooii  50125  i0oii  50127  sepfsepc  50135  seppcld  50137