Theorem 1xr 11349

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

Syntax hints:   ∈ wcel 2108  1c1 11185  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-xr 11328

This theorem is referenced by:  xmulrid  13341  xmullid  13342  xmulm1  13343  x2times  13361  xov1plusxeqvd  13558  ico01fl0  13870  hashge1  14438  hashgt12el  14471  hashgt12el2  14472  hashgt23el  14473  sgn1  15141  fprodge1  16043  halfleoddlt  16410  isnzr2hash  20545  0ringnnzr  20551  xrsnsgrp  21443  leordtval2  23241  unirnblps  24450  unirnbl  24451  mopnex  24553  dscopn  24607  nmoid  24784  xrsmopn  24853  zdis  24857  metnrmlem1a  24899  metnrmlem1  24900  icopnfcnv  24992  icopnfhmeo  24993  iccpnfcnv  24994  iccpnfhmeo  24995  cncmet  25375  itg2monolem1  25805  itg2monolem3  25807  abelthlem2  26494  abelthlem3  26495  abelthlem5  26497  abelthlem7  26500  abelth  26503  dvlog2lem  26712  dvlog2  26713  logtayl  26720  logtayl2  26722  scvxcvx  27047  pntibndlem1  27651  pntibndlem2  27653  pntibnd  27655  pntlemc  27657  pnt  27676  padicabvf  27693  padicabvcxp  27694  elntg2  29018  nmopun  32046  pjnmopi  32180  xlt2addrd  32765  xdivrec  32891  xrsmulgzz  32992  xrnarchi  33164  rtelextdg2lem  33717  unitssxrge0  33846  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  hasheuni  34049  ddemeas  34200  omssubadd  34265  prob01  34378  lfuhgr2  35086  dnizeq0  36441  iccioo01  37293  broucube  37614  asindmre  37663  dvasin  37664  areacirclem1  37668  aks6d1c6lem1  42127  imo72b2  44134  cvgdvgrat  44282  supxrgelem  45252  xrlexaddrp  45267  infxr  45282  infleinflem2  45286  limsup10exlem  45693  limsup10ex  45694  liminf10ex  45695  salexct2  46260  salgencntex  46264  ovn0lem  46486  expnegico01  48247  regt1loggt0  48270  rege1logbrege0  48292  rege1logbzge0  48293  dignnld  48337  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  iooii  48597  i0oii  48599  sepfsepc  48607  seppcld  48609