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

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

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 2733  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-mulcl 11243  ax-mulrcl 11244  ax-i2m1 11249  ax-1ne0 11250  ax-rrecex 11253  ax-cnre 11254

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6487  df-fv 6539  df-ov 7415  df-xr 11328

This theorem is used by:  xmulrid  13390  xmullid  13391  xmulm1  13392  x2times  13410  xov1plusxeqvd  13610  nnge2recico01  13619  ico01fl0  13939  hashge1  14513  hashgt12el  14547  hashgt12el2  14548  hashgt23el  14549  sgn1  15225  sgnrn  15231  fprodge1  16142  halfleoddlt  16512  isnzr2hash  20750  0ringnnzr  20756  xrsnsgrp  21694  leordtval2  23510  unirnblps  24718  unirnbl  24719  mopnex  24818  dscopn  24872  nmoid  25041  xrsmopn  25112  zdis  25116  metnrmlem1a  25158  metnrmlem1  25159  icopnfcnv  25243  icopnfhmeo  25244  iccpnfcnv  25245  iccpnfhmeo  25246  cncmet  25623  itg2monolem1  26051  itg2monolem3  26053  abelthlem2  26741  abelthlem3  26742  abelthlem5  26744  abelthlem7  26747  abelth  26750  dvlog2lem  26962  dvlog2  26963  logtayl  26970  logtayl2  26972  scvxcvx  27295  pntibndlem1  27898  pntibndlem2  27900  pntibnd  27902  pntlemc  27904  pnt  27923  padicabvf  27940  padicabvcxp  27941  elntg2  29545  lfuhgr2  29709  nmopun  32598  pjnmopi  32732  xlt2addrd  33333  xdivrec  33475  xrsmulgzz  33552  xrnarchi  33727  vietadeg1  34192  rtelextdg2lem  34340  unitssxrge0  34514  xrge0iifcnv  34547  xrge0iifiso  34549  xrge0iifhom  34551  hasheuni  34699  ddemeas  34851  omssubadd  34915  prob01  35028  dnizeq0  37311  iccioo01  38218  broucube  38540  asindmre  38589  dvasin  38590  areacirclem1  38594  aks6d1c6lem1  43188  imo72b2  45131  cvgdvgrat  45256  supxrgelem  46293  xrlexaddrp  46308  infxr  46322  infleinflem2  46326  limsup10exlem  46726  limsup10ex  46727  liminf10ex  46728  salexct2  47293  salgencntex  47297  ovn0lem  47519  flmrecm1  48357  expnegico01  49574  regt1loggt0  49592  rege1logbrege0  49614  rege1logbzge0  49615  dignnld  49659  eenglngeehlnmlem1  49793  eenglngeehlnmlem2  49794  iooii  49970  i0oii  49972  sepfsepc  49980  seppcld  49982