Theorem 1xr 11286

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

This proof depends on syntax axioms:   ∈ wcel 2146  1c1 11119  ℝ^*cxr 11260

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-mulcl 11180  ax-mulrcl 11181  ax-i2m1 11186  ax-1ne0 11187  ax-rrecex 11190  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426  df-xr 11265

This theorem is used by:  xmulrid  13323  xmullid  13324  xmulm1  13325  x2times  13343  xov1plusxeqvd  13543  nnge2recico01  13552  ico01fl0  13872  hashge1  14445  hashgt12el  14479  hashgt12el2  14480  hashgt23el  14481  sgn1  15155  sgnrn  15161  fprodge1  16075  halfleoddlt  16445  isnzr2hash  20654  0ringnnzr  20660  xrsnsgrp  21595  leordtval2  23406  unirnblps  24613  unirnbl  24614  mopnex  24713  dscopn  24767  nmoid  24936  xrsmopn  25007  zdis  25011  metnrmlem1a  25053  metnrmlem1  25054  icopnfcnv  25138  icopnfhmeo  25139  iccpnfcnv  25140  iccpnfhmeo  25141  cncmet  25518  itg2monolem1  25946  itg2monolem3  25948  abelthlem2  26632  abelthlem3  26633  abelthlem5  26635  abelthlem7  26638  abelth  26641  dvlog2lem  26854  dvlog2  26855  logtayl  26862  logtayl2  26864  scvxcvx  27187  pntibndlem1  27790  pntibndlem2  27792  pntibnd  27794  pntlemc  27796  pnt  27815  padicabvf  27832  padicabvcxp  27833  elntg2  29372  nmopun  32403  pjnmopi  32537  xlt2addrd  33141  xdivrec  33283  xrsmulgzz  33360  xrnarchi  33535  vietadeg1  33999  rtelextdg2lem  34147  unitssxrge0  34321  xrge0iifcnv  34354  xrge0iifiso  34356  xrge0iifhom  34358  hasheuni  34506  ddemeas  34658  omssubadd  34722  prob01  34835  lfuhgr2  35632  dnizeq0  37105  iccioo01  38014  broucube  38346  asindmre  38395  dvasin  38396  areacirclem1  38400  aks6d1c6lem1  42978  imo72b2  44939  cvgdvgrat  45064  supxrgelem  46094  xrlexaddrp  46109  infxr  46123  infleinflem2  46127  limsup10exlem  46527  limsup10ex  46528  liminf10ex  46529  salexct2  47094  salgencntex  47098  ovn0lem  47320  flmrecm1  48121  expnegico01  49339  regt1loggt0  49357  rege1logbrege0  49379  rege1logbzge0  49380  dignnld  49424  eenglngeehlnmlem1  49558  eenglngeehlnmlem2  49559  iooii  49737  i0oii  49739  sepfsepc  49747  seppcld  49749