Theorem 1xr 11398

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

This proof depends on syntax axioms:   ∈ wcel 2147  1c1 11231  ℝ^*cxr 11372

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-mulcl 11292  ax-mulrcl 11293  ax-i2m1 11298  ax-1ne0 11299  ax-rrecex 11302  ax-cnre 11303

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6515  df-fv 6569  df-ov 7449  df-xr 11377

This theorem is used by:  xmulrid  13439  xmullid  13440  xmulm1  13441  x2times  13459  xov1plusxeqvd  13659  nnge2recico01  13668  ico01fl0  13989  hashge1  14563  hashgt12el  14597  hashgt12el2  14598  hashgt23el  14599  sgn1  15277  sgnrn  15283  fprodge1  16194  halfleoddlt  16564  isnzr2hash  20803  0ringnnzr  20809  xrsnsgrp  21747  leordtval2  23563  unirnblps  24771  unirnbl  24772  mopnex  24871  dscopn  24925  nmoid  25094  xrsmopn  25165  zdis  25169  metnrmlem1a  25211  metnrmlem1  25212  icopnfcnv  25296  icopnfhmeo  25297  iccpnfcnv  25298  iccpnfhmeo  25299  cncmet  25676  itg2monolem1  26104  itg2monolem3  26106  abelthlem2  26792  abelthlem3  26793  abelthlem5  26795  abelthlem7  26798  abelth  26801  cos0pilt1  26893  dvlog2lem  27013  dvlog2  27014  logtayl  27021  logtayl2  27023  scvxcvx  27346  pntibndlem1  27949  pntibndlem2  27951  pntibnd  27953  pntlemc  27955  pnt  27974  padicabvf  27991  padicabvcxp  27992  elntg2  29596  lfuhgr2  29760  nmopun  32649  pjnmopi  32783  xlt2addrd  33424  xdivrec  33566  xrsmulgzz  33646  xrnarchi  33821  vietadeg1  34293  rtelextdg2lem  34441  unitssxrge0  34615  xrge0iifcnv  34648  xrge0iifiso  34650  xrge0iifhom  34652  hasheuni  34800  ddemeas  34952  omssubadd  35015  prob01  35128  dnizeq0  37532  iccioo01  38455  broucube  38777  asindmre  38826  dvasin  38827  areacirclem1  38831  aks6d1c6lem1  43423  imo72b2  45375  cvgdvgrat  45500  supxrgelem  46564  xrlexaddrp  46579  infxr  46593  infleinflem2  46597  limsup10exlem  46997  limsup10ex  46998  liminf10ex  46999  salexct2  47564  salgencntex  47568  ovn0lem  47790  flmrecm1  48628  expnegico01  49845  regt1loggt0  49863  rege1logbrege0  49885  rege1logbzge0  49886  dignnld  49930  eenglngeehlnmlem1  50065  eenglngeehlnmlem2  50066  iooii  50247  i0oii  50249  sepfsepc  50257  seppcld  50259