MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1xr Structured version   Visualization version   GIF version

Theorem 1xr 10688
Description: 1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
Assertion
Ref Expression
1xr 1 ∈ ℝ*

Proof of Theorem 1xr
StepHypRef Expression
1 1re 10629 . 2 1 ∈ ℝ
21rexri 10687 1 1 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  1c1 10526  *cxr 10662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-mulcl 10587  ax-mulrcl 10588  ax-i2m1 10593  ax-1ne0 10594  ax-rrecex 10597  ax-cnre 10598
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-xr 10667
This theorem is referenced by:  xmulid1  12660  xmulid2  12661  xmulm1  12662  x2times  12680  xov1plusxeqvd  12872  ico01fl0  13177  hashge1  13738  hashgt12el  13771  hashgt12el2  13772  hashgt23el  13773  sgn1  14439  fprodge1  15337  halfleoddlt  15699  isnzr2hash  19965  0ringnnzr  19970  xrsnsgrp  20509  leordtval2  21748  unirnblps  22956  unirnbl  22957  mopnex  23056  dscopn  23110  nmoid  23278  xrsmopn  23347  zdis  23351  metnrmlem1a  23393  metnrmlem1  23394  icopnfcnv  23473  icopnfhmeo  23474  iccpnfcnv  23475  iccpnfhmeo  23476  cncmet  23852  itg2monolem1  24278  itg2monolem3  24280  abelthlem2  24947  abelthlem3  24948  abelthlem5  24950  abelthlem7  24953  abelth  24956  dvlog2lem  25162  dvlog2  25163  logtayl  25170  logtayl2  25172  scvxcvx  25490  pntibndlem1  26092  pntibndlem2  26094  pntibnd  26096  pntlemc  26098  pnt  26117  padicabvf  26134  padicabvcxp  26135  elntg2  26698  nmopun  29718  pjnmopi  29852  xlt2addrd  30408  xdivrec  30530  xrsmulgzz  30592  xrnarchi  30740  unitssxrge0  31042  xrge0iifcnv  31075  xrge0iifiso  31077  xrge0iifhom  31079  hasheuni  31243  ddemeas  31394  omssubadd  31457  prob01  31570  lfuhgr2  32262  dnizeq0  33711  broucube  34807  asindmre  34858  dvasin  34859  areacirclem1  34863  imo72b2  40403  cvgdvgrat  40522  supxrgelem  41481  xrlexaddrp  41496  infxr  41511  infleinflem2  41515  limsup10exlem  41929  limsup10ex  41930  liminf10ex  41931  salexct2  42499  salgencntex  42503  ovn0lem  42724  expnegico01  44501  regt1loggt0  44524  rege1logbrege0  44546  rege1logbzge0  44547  dignnld  44591  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653
  Copyright terms: Public domain W3C validator