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

Theorem recni 9388
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 9329 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3343 1  |-  A  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1757   CCcc 9270   RRcr 9271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-resscn 9329
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3325  df-ss 3332
This theorem is referenced by:  renegcli  9660  resubcli  9661  recgt0ii  10228  ledivp1i  10248  ltdivp1i  10249  nncni  10322  2cn  10382  3cn  10386  4cn  10389  5cn  10391  6cn  10393  7cn  10395  8cn  10397  9cn  10399  8th4div3  10535  nn0cni  10581  numltc  10765  sqge0i  11939  lt2sqi  11940  le2sqi  11941  sq11i  11942  crreczi  11975  faclbnd4lem1  12055  sqrmsq2i  12861  abs3lemi  12883  0.999...  13326  ef01bndlem  13453  sin4lt0  13464  eirrlem  13471  rpnnen2lem3  13484  rpnnen2lem9  13490  rpnnen2lem11  13492  dvdslelem  13562  divalglem1  13583  divalglem2  13584  divalglem5  13586  divalglem6  13587  divalglem9  13590  prmreclem6  13967  modsubi  14086  pcoass  20440  aaliou3lem7  21702  picn  21809  sinhalfpilem  21812  cosneghalfpi  21819  sincosq1sgn  21847  sincosq2sgn  21848  sincosq3sgn  21849  sincosq4sgn  21850  sincos4thpi  21862  tan4thpi  21863  sincos6thpi  21864  pige3  21866  cosne0  21873  sinord  21877  resinf1o  21879  efif1olem2  21886  efif1olem4  21888  efifo  21890  logimul  21950  ecxp  22005  cxpsqrlem  22034  ang180lem1  22092  ang180lem2  22093  1cubrlem  22123  quartlem3  22141  asinsin  22174  acoscos  22175  asin1  22176  reasinsin  22178  acosbnd  22182  atanlogsublem  22197  atanbnd  22208  atan1  22210  log2tlbnd  22227  log2ublem1  22228  birthday  22235  basellem8  22312  basellem9  22313  cht2  22397  mumullem2  22405  chtublem  22437  chtub  22438  bposlem6  22515  bposlem7  22516  bposlem8  22517  bposlem9  22518  chebbnd1lem3  22607  chebbnd1  22608  chto1ub  22612  mulogsumlem  22667  mulog2sumlem1  22670  mulog2sumlem2  22671  mulog2sumlem3  22672  pntibndlem3  22728  nmblolbii  24024  ip0i  24050  ip1ilem  24051  ipasslem10  24064  siilem1  24076  siii  24078  normlem1  24337  normlem3  24339  normlem5  24341  normlem6  24342  norm-ii-i  24364  normsubi  24368  norm3adifii  24375  norm3lem  24376  normpar2i  24383  bcsiALT  24406  pjneli  24951  lnophmlem2  25246  nmbdoplbi  25253  nmcoplbi  25257  nmophmi  25260  nmbdfnlbi  25278  nmcfnlbi  25281  cnlnadjlem2  25297  cnlnadjlem7  25302  nmopadjlem  25318  nmopcoi  25324  nmopcoadji  25330  nmopcoadj0i  25332  unierri  25333  opsqrlem1  25369  log2le1  26322  subfaclim  26926  subfacval3  26927  problem2  27149  problem3  27150  problem4  27151  problem5  27152  circum  27168  bpoly4  28051  cos2h  28269  tan2h  28270  dvtanlem  28287  dvacos  28327  areacirc  28335  fdc  28487  rmspecsqrnq  29094  proot1ex  29416  arearect  29438  areaquad  29439  itgsinexplem1  29642  wallispilem2  29709  wallispilem4  29711  wallispi  29713  stirlinglem3  29719  stirlinglem4  29720  stirlinglem13  29729  stirlinglem15  29731  dpfrac1  30856  elogb  30859  sineq0ALT  31415  taupilem1  35228
  Copyright terms: Public domain W3C validator