MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  recni Structured version   Visualization version   Unicode version

Theorem recni 9681
Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
Hypothesis
Ref Expression
recni.1  |-  A  e.  RR
Assertion
Ref Expression
recni  |-  A  e.  CC

Proof of Theorem recni
StepHypRef Expression
1 ax-resscn 9622 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3441 1  |-  A  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1898   CCcc 9563   RRcr 9564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-resscn 9622
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  renegcli  9961  resubcli  9962  recgt0ii  10540  ledivp1i  10560  ltdivp1i  10561  nncni  10647  2cn  10708  3cn  10712  4cn  10715  5cn  10717  6cn  10719  7cn  10721  8cn  10723  9cn  10725  8th4div3  10862  nn0cni  10910  numltc  11100  sqge0i  12394  lt2sqi  12395  le2sqi  12396  sq11i  12397  crreczi  12429  faclbnd4lem1  12510  sqrtmsq2i  13499  abs3lemi  13521  0.999...  13986  bpoly4  14161  ef01bndlem  14287  sin4lt0  14298  eirrlem  14305  rpnnen2lem3  14318  rpnnen2lem9  14324  rpnnen2lem11  14326  dvdslelem  14398  divalglem1  14421  divalglem2  14422  divalglem2OLD  14423  divalglem5OLD  14425  divalglem5  14426  divalglem6  14427  divalglem9  14430  divalglem9OLD  14431  prmreclem6  14914  modsubi  15093  pcoass  22104  aaliou3lem7  23354  picn  23463  sinhalfpilem  23467  cosneghalfpi  23474  sincosq1sgn  23502  sincosq2sgn  23503  sincosq3sgn  23504  sincosq4sgn  23505  sincos4thpi  23517  tan4thpi  23518  sincos6thpi  23519  pige3  23521  cosne0  23528  sinord  23532  resinf1o  23534  efif1olem2  23541  efif1olem4  23543  efifo  23545  logimul  23612  ecxp  23667  cxpsqrtlem  23696  elogb  23756  logblog  23778  ang180lem1  23787  ang180lem2  23788  1cubrlem  23816  quartlem3  23834  asinsin  23867  acoscos  23868  asin1  23869  reasinsin  23871  acosbnd  23875  atanlogsublem  23890  atanbnd  23901  atan1  23903  log2tlbnd  23920  log2ublem1  23921  log2le1  23925  birthday  23929  basellem8  24063  basellem9  24064  cht2  24148  mumullem2  24156  chtublem  24188  chtub  24189  bposlem6  24266  bposlem7  24267  bposlem8  24268  bposlem9  24269  chebbnd1lem3  24358  chebbnd1  24359  chto1ub  24363  mulogsumlem  24418  mulog2sumlem1  24421  mulog2sumlem2  24422  mulog2sumlem3  24423  pntibndlem3  24479  nmblolbii  26489  ip0i  26515  ip1ilem  26516  ipasslem10  26529  siilem1  26541  siii  26543  normlem1  26812  normlem3  26814  normlem5  26816  normlem6  26817  norm-ii-i  26839  normsubi  26843  norm3adifii  26850  norm3lem  26851  normpar2i  26858  bcsiALT  26881  pjneli  27425  lnophmlem2  27719  nmbdoplbi  27726  nmcoplbi  27730  nmophmi  27733  nmbdfnlbi  27751  nmcfnlbi  27754  cnlnadjlem2  27770  cnlnadjlem7  27775  nmopadjlem  27791  nmopcoi  27797  nmopcoadji  27803  nmopcoadj0i  27805  unierri  27806  opsqrlem1  27842  subfaclim  29960  subfacval3  29961  problem2  30347  problem3  30348  problem4  30349  problem5  30350  circum  30367  logi  30419  iexpire  30420  taupilem1  31767  dvtanlemOLD  32036  dvacos  32074  fdc  32119  rmspecsqrtnq  35799  arearect  36145  areaquad  36146  sineq0ALT  37374  wallispilem2  37966  stirlinglem3  37976  stirlinglem4  37977  stirlinglem13  37986  stirlinglem15  37988  dirkerper  37996  fourierdlem24  38031  fourierdlem103  38111  fourierdlem104  38112  sqwvfoura  38130  sqwvfourb  38131  fourierswlem  38132  fouriersw  38133  etransclem18  38155  etransclem23  38160  etransclem46  38183  etransclem47  38184  etransclem48OLD  38185  etransclem48  38186  etransc  38187  tgoldbach  38949  dpfrac1  40765
  Copyright terms: Public domain W3C validator