Theorem 1xr 11320

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

Syntax hints:   ∈ wcel 2108  1c1 11156  ℝ^*cxr 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-xr 11299

This theorem is referenced by:  xmulrid  13321  xmullid  13322  xmulm1  13323  x2times  13341  xov1plusxeqvd  13538  ico01fl0  13859  hashge1  14428  hashgt12el  14461  hashgt12el2  14462  hashgt23el  14463  sgn1  15131  fprodge1  16031  halfleoddlt  16399  isnzr2hash  20519  0ringnnzr  20525  xrsnsgrp  21420  leordtval2  23220  unirnblps  24429  unirnbl  24430  mopnex  24532  dscopn  24586  nmoid  24763  xrsmopn  24834  zdis  24838  metnrmlem1a  24880  metnrmlem1  24881  icopnfcnv  24973  icopnfhmeo  24974  iccpnfcnv  24975  iccpnfhmeo  24976  cncmet  25356  itg2monolem1  25785  itg2monolem3  25787  abelthlem2  26476  abelthlem3  26477  abelthlem5  26479  abelthlem7  26482  abelth  26485  dvlog2lem  26694  dvlog2  26695  logtayl  26702  logtayl2  26704  scvxcvx  27029  pntibndlem1  27633  pntibndlem2  27635  pntibnd  27637  pntlemc  27639  pnt  27658  padicabvf  27675  padicabvcxp  27676  elntg2  29000  nmopun  32033  pjnmopi  32167  xlt2addrd  32762  xdivrec  32909  xrsmulgzz  33011  xrnarchi  33191  rtelextdg2lem  33767  unitssxrge0  33899  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  hasheuni  34086  ddemeas  34237  omssubadd  34302  prob01  34415  lfuhgr2  35124  dnizeq0  36476  iccioo01  37328  broucube  37661  asindmre  37710  dvasin  37711  areacirclem1  37715  aks6d1c6lem1  42171  imo72b2  44185  cvgdvgrat  44332  supxrgelem  45348  xrlexaddrp  45363  infxr  45378  infleinflem2  45382  limsup10exlem  45787  limsup10ex  45788  liminf10ex  45789  salexct2  46354  salgencntex  46358  ovn0lem  46580  expnegico01  48435  regt1loggt0  48457  rege1logbrege0  48479  rege1logbzge0  48480  dignnld  48524  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  iooii  48815  i0oii  48817  sepfsepc  48825  seppcld  48827