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

Theorem recni 9398
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 9339 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3353 1  |-  A  e.  CC
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   CCcc 9280   RRcr 9281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-resscn 9339
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3335  df-ss 3342
This theorem is referenced by:  renegcli  9670  resubcli  9671  recgt0ii  10238  ledivp1i  10258  ltdivp1i  10259  nncni  10332  2cn  10392  3cn  10396  4cn  10399  5cn  10401  6cn  10403  7cn  10405  8cn  10407  9cn  10409  8th4div3  10545  nn0cni  10591  numltc  10775  sqge0i  11953  lt2sqi  11954  le2sqi  11955  sq11i  11956  crreczi  11989  faclbnd4lem1  12069  sqrmsq2i  12875  abs3lemi  12897  0.999...  13341  ef01bndlem  13468  sin4lt0  13479  eirrlem  13486  rpnnen2lem3  13499  rpnnen2lem9  13505  rpnnen2lem11  13507  dvdslelem  13577  divalglem1  13598  divalglem2  13599  divalglem5  13601  divalglem6  13602  divalglem9  13605  prmreclem6  13982  modsubi  14101  pcoass  20596  aaliou3lem7  21815  picn  21922  sinhalfpilem  21925  cosneghalfpi  21932  sincosq1sgn  21960  sincosq2sgn  21961  sincosq3sgn  21962  sincosq4sgn  21963  sincos4thpi  21975  tan4thpi  21976  sincos6thpi  21977  pige3  21979  cosne0  21986  sinord  21990  resinf1o  21992  efif1olem2  21999  efif1olem4  22001  efifo  22003  logimul  22063  ecxp  22118  cxpsqrlem  22147  ang180lem1  22205  ang180lem2  22206  1cubrlem  22236  quartlem3  22254  asinsin  22287  acoscos  22288  asin1  22289  reasinsin  22291  acosbnd  22295  atanlogsublem  22310  atanbnd  22321  atan1  22323  log2tlbnd  22340  log2ublem1  22341  birthday  22348  basellem8  22425  basellem9  22426  cht2  22510  mumullem2  22518  chtublem  22550  chtub  22551  bposlem6  22628  bposlem7  22629  bposlem8  22630  bposlem9  22631  chebbnd1lem3  22720  chebbnd1  22721  chto1ub  22725  mulogsumlem  22780  mulog2sumlem1  22783  mulog2sumlem2  22784  mulog2sumlem3  22785  pntibndlem3  22841  nmblolbii  24199  ip0i  24225  ip1ilem  24226  ipasslem10  24239  siilem1  24251  siii  24253  normlem1  24512  normlem3  24514  normlem5  24516  normlem6  24517  norm-ii-i  24539  normsubi  24543  norm3adifii  24550  norm3lem  24551  normpar2i  24558  bcsiALT  24581  pjneli  25126  lnophmlem2  25421  nmbdoplbi  25428  nmcoplbi  25432  nmophmi  25435  nmbdfnlbi  25453  nmcfnlbi  25456  cnlnadjlem2  25472  cnlnadjlem7  25477  nmopadjlem  25493  nmopcoi  25499  nmopcoadji  25505  nmopcoadj0i  25507  unierri  25508  opsqrlem1  25544  log2le1  26466  subfaclim  27076  subfacval3  27077  problem2  27299  problem3  27300  problem4  27301  problem5  27302  circum  27319  bpoly4  28202  cos2h  28423  tan2h  28424  dvtanlem  28441  dvacos  28481  areacirc  28489  fdc  28641  rmspecsqrnq  29247  proot1ex  29569  arearect  29591  areaquad  29592  itgsinexplem1  29794  wallispilem2  29861  wallispilem4  29863  wallispi  29865  stirlinglem3  29871  stirlinglem4  29872  stirlinglem13  29881  stirlinglem15  29883  dpfrac1  31107  elogb  31110  sineq0ALT  31673  taupilem1  35615
  Copyright terms: Public domain W3C validator