Theorem 1xr 11369

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

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

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 11259  ax-icn 11260  ax-addcl 11261  ax-mulcl 11263  ax-mulrcl 11264  ax-i2m1 11269  ax-1ne0 11270  ax-rrecex 11273  ax-cnre 11274

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 3900  df-un 3902  df-ss 3915  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6495  df-fv 6547  df-ov 7424  df-xr 11348

This theorem is used by:  xmulrid  13410  xmullid  13411  xmulm1  13412  x2times  13430  xov1plusxeqvd  13630  nnge2recico01  13639  ico01fl0  13960  hashge1  14534  hashgt12el  14568  hashgt12el2  14569  hashgt23el  14570  sgn1  15246  sgnrn  15252  fprodge1  16163  halfleoddlt  16533  isnzr2hash  20771  0ringnnzr  20777  xrsnsgrp  21715  leordtval2  23531  unirnblps  24739  unirnbl  24740  mopnex  24839  dscopn  24893  nmoid  25062  xrsmopn  25133  zdis  25137  metnrmlem1a  25179  metnrmlem1  25180  icopnfcnv  25264  icopnfhmeo  25265  iccpnfcnv  25266  iccpnfhmeo  25267  cncmet  25644  itg2monolem1  26072  itg2monolem3  26074  abelthlem2  26760  abelthlem3  26761  abelthlem5  26763  abelthlem7  26766  abelth  26769  dvlog2lem  26981  dvlog2  26982  logtayl  26989  logtayl2  26991  scvxcvx  27314  pntibndlem1  27917  pntibndlem2  27919  pntibnd  27921  pntlemc  27923  pnt  27942  padicabvf  27959  padicabvcxp  27960  elntg2  29564  lfuhgr2  29728  nmopun  32617  pjnmopi  32751  xlt2addrd  33352  xdivrec  33494  xrsmulgzz  33571  xrnarchi  33746  vietadeg1  34211  rtelextdg2lem  34359  unitssxrge0  34533  xrge0iifcnv  34566  xrge0iifiso  34568  xrge0iifhom  34570  hasheuni  34718  ddemeas  34870  omssubadd  34933  prob01  35046  dnizeq0  37342  iccioo01  38252  broucube  38574  asindmre  38623  dvasin  38624  areacirclem1  38628  aks6d1c6lem1  43222  imo72b2  45173  cvgdvgrat  45298  supxrgelem  46350  xrlexaddrp  46365  infxr  46379  infleinflem2  46383  limsup10exlem  46783  limsup10ex  46784  liminf10ex  46785  salexct2  47350  salgencntex  47354  ovn0lem  47576  flmrecm1  48414  expnegico01  49631  regt1loggt0  49649  rege1logbrege0  49671  rege1logbzge0  49672  dignnld  49716  eenglngeehlnmlem1  49850  eenglngeehlnmlem2  49851  iooii  50027  i0oii  50029  sepfsepc  50037  seppcld  50039