Theorem 1xr 11256

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

Syntax hints:   ∈ wcel 2145  1c1 11089  ℝ^*cxr 11230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-mulcl 11150  ax-mulrcl 11151  ax-i2m1 11156  ax-1ne0 11157  ax-rrecex 11160  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-xr 11235

This theorem is referenced by:  xmulrid  13296  xmullid  13297  xmulm1  13298  x2times  13316  xov1plusxeqvd  13516  nnge2recico01  13525  ico01fl0  13843  hashge1  14416  hashgt12el  14449  hashgt12el2  14450  hashgt23el  14451  sgn1  15119  sgnrn  15125  fprodge1  16039  halfleoddlt  16410  isnzr2hash  20594  0ringnnzr  20600  xrsnsgrp  21518  leordtval2  23330  unirnblps  24537  unirnbl  24538  mopnex  24637  dscopn  24691  nmoid  24860  xrsmopn  24931  zdis  24935  metnrmlem1a  24977  metnrmlem1  24978  icopnfcnv  25062  icopnfhmeo  25063  iccpnfcnv  25064  iccpnfhmeo  25065  cncmet  25442  itg2monolem1  25870  itg2monolem3  25872  abelthlem2  26553  abelthlem3  26554  abelthlem5  26556  abelthlem7  26559  abelth  26562  dvlog2lem  26775  dvlog2  26776  logtayl  26783  logtayl2  26785  scvxcvx  27108  pntibndlem1  27711  pntibndlem2  27713  pntibnd  27715  pntlemc  27717  pnt  27736  padicabvf  27753  padicabvcxp  27754  elntg2  29244  nmopun  32275  pjnmopi  32409  xlt2addrd  33016  xdivrec  33159  xrsmulgzz  33242  xrnarchi  33417  vietadeg1  33885  rtelextdg2lem  34033  unitssxrge0  34207  xrge0iifcnv  34240  xrge0iifiso  34242  xrge0iifhom  34244  hasheuni  34392  ddemeas  34543  omssubadd  34607  prob01  34720  lfuhgr2  35482  dnizeq0  36926  iccioo01  37833  broucube  38165  asindmre  38214  dvasin  38215  areacirclem1  38219  aks6d1c6lem1  42799  imo72b2  44760  cvgdvgrat  44887  supxrgelem  45911  xrlexaddrp  45926  infxr  45940  infleinflem2  45944  limsup10exlem  46344  limsup10ex  46345  liminf10ex  46346  salexct2  46911  salgencntex  46915  ovn0lem  47137  flmrecm1  47935  expnegico01  49149  regt1loggt0  49167  rege1logbrege0  49189  rege1logbzge0  49190  dignnld  49234  eenglngeehlnmlem1  49368  eenglngeehlnmlem2  49369  iooii  49547  i0oii  49549  sepfsepc  49557  seppcld  49559