Theorem 1xr 10498

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

Syntax hints:   ∈ wcel 2051  1c1 10334  ℝ^*cxr 10471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743  ax-1cn 10391  ax-icn 10392  ax-addcl 10393  ax-mulcl 10395  ax-mulrcl 10396  ax-i2m1 10401  ax-1ne0 10402  ax-rrecex 10405  ax-cnre 10406

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-ral 3086  df-rex 3087  df-rab 3090  df-v 3410  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-iota 6149  df-fv 6193  df-ov 6977  df-xr 10476

This theorem is referenced by:  xmulid1  12486  xmulid2  12487  xmulm1  12488  x2times  12506  xov1plusxeqvd  12698  ico01fl0  13002  hashge1  13561  hashgt12el  13594  hashgt12el2  13595  hashgt23el  13596  sgn1  14310  fprodge1  15207  halfleoddlt  15569  isnzr2hash  19770  0ringnnzr  19775  xrsnsgrp  20298  leordtval2  21539  unirnblps  22747  unirnbl  22748  mopnex  22847  dscopn  22901  nmoid  23069  xrsmopn  23138  zdis  23142  metnrmlem1a  23184  metnrmlem1  23185  icopnfcnv  23264  icopnfhmeo  23265  iccpnfcnv  23266  iccpnfhmeo  23267  cncmet  23643  itg2monolem1  24069  itg2monolem3  24071  abelthlem2  24738  abelthlem3  24739  abelthlem5  24741  abelthlem7  24744  abelth  24747  dvlog2lem  24951  dvlog2  24952  logtayl  24959  logtayl2  24961  scvxcvx  25280  pntibndlem1  25882  pntibndlem2  25884  pntibnd  25886  pntlemc  25888  pnt  25907  padicabvf  25924  padicabvcxp  25925  elntg2  26489  nmopun  29587  pjnmopi  29721  xlt2addrd  30258  xdivrec  30373  xrsmulgzz  30423  xrnarchi  30511  unitssxrge0  30819  xrge0iifcnv  30852  xrge0iifiso  30854  xrge0iifhom  30856  hasheuni  31020  ddemeas  31172  omssubadd  31235  prob01  31349  dnizeq0  33371  broucube  34404  asindmre  34455  dvasin  34456  areacirclem1  34460  imo72b2  39928  cvgdvgrat  40099  supxrgelem  41068  xrlexaddrp  41083  infxr  41098  infleinflem2  41102  limsup10exlem  41518  limsup10ex  41519  liminf10ex  41520  salexct2  42087  salgencntex  42091  ovn0lem  42312  expnegico01  43975  regt1loggt0  43998  rege1logbrege0  44020  rege1logbzge0  44021  dignnld  44065  eenglngeehlnmlem1  44126  eenglngeehlnmlem2  44127