Theorem 1xr 11296

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

This proof depends on syntax axioms:   ∈ wcel 2145  1c1 11129  ℝ^*cxr 11270

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 2147  ax-9 2155  ax-ext 2734  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-mulcl 11190  ax-mulrcl 11191  ax-i2m1 11196  ax-1ne0 11197  ax-rrecex 11200  ax-cnre 11201

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-xr 11275

This theorem is used by:  xmulrid  13335  xmullid  13336  xmulm1  13337  x2times  13355  xov1plusxeqvd  13555  nnge2recico01  13564  ico01fl0  13884  hashge1  14457  hashgt12el  14491  hashgt12el2  14492  hashgt23el  14493  sgn1  15169  sgnrn  15175  fprodge1  16088  halfleoddlt  16458  isnzr2hash  20686  0ringnnzr  20692  xrsnsgrp  21627  leordtval2  23443  unirnblps  24651  unirnbl  24652  mopnex  24751  dscopn  24805  nmoid  24974  xrsmopn  25045  zdis  25049  metnrmlem1a  25091  metnrmlem1  25092  icopnfcnv  25176  icopnfhmeo  25177  iccpnfcnv  25178  iccpnfhmeo  25179  cncmet  25556  itg2monolem1  25984  itg2monolem3  25986  abelthlem2  26675  abelthlem3  26676  abelthlem5  26678  abelthlem7  26681  abelth  26684  dvlog2lem  26897  dvlog2  26898  logtayl  26905  logtayl2  26907  scvxcvx  27230  pntibndlem1  27833  pntibndlem2  27835  pntibnd  27837  pntlemc  27839  pnt  27858  padicabvf  27875  padicabvcxp  27876  elntg2  29450  lfuhgr2  29614  nmopun  32503  pjnmopi  32637  xlt2addrd  33238  xdivrec  33380  xrsmulgzz  33457  xrnarchi  33632  vietadeg1  34096  rtelextdg2lem  34244  unitssxrge0  34418  xrge0iifcnv  34451  xrge0iifiso  34453  xrge0iifhom  34455  hasheuni  34603  ddemeas  34755  omssubadd  34819  prob01  34932  dnizeq0  37180  iccioo01  38089  broucube  38411  asindmre  38460  dvasin  38461  areacirclem1  38465  aks6d1c6lem1  43044  imo72b2  45020  cvgdvgrat  45145  supxrgelem  46175  xrlexaddrp  46190  infxr  46204  infleinflem2  46208  limsup10exlem  46608  limsup10ex  46609  liminf10ex  46610  salexct2  47175  salgencntex  47179  ovn0lem  47401  flmrecm1  48239  expnegico01  49456  regt1loggt0  49474  rege1logbrege0  49496  rege1logbzge0  49497  dignnld  49541  eenglngeehlnmlem1  49675  eenglngeehlnmlem2  49676  iooii  49852  i0oii  49854  sepfsepc  49862  seppcld  49864