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

Theorem recn 9015
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
Assertion
Ref Expression
recn  |-  ( A  e.  RR  ->  A  e.  CC )

Proof of Theorem recn
StepHypRef Expression
1 ax-resscn 8982 . 2  |-  RR  C_  CC
21sseli 3289 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   CCcc 8923   RRcr 8924
This theorem is referenced by:  mulid1  9023  recnd  9049  pnfnre  9062  mnfnre  9063  mul02  9178  renegcli  9296  resubcl  9299  ltaddsub2  9437  leaddsub2  9439  leltadd  9446  ltaddpos  9452  ltaddpos2  9453  posdif  9455  lenegcon1  9466  lenegcon2  9467  addge01  9472  addge02  9473  mullt0  9481  recex  9588  ltm1  9784  prodgt02  9790  prodge02  9792  ltmul2  9795  lemul1  9796  lemul2  9797  lemul1a  9798  lemul2a  9799  ltmulgt12  9805  lemulge12  9807  gt0div  9810  ge0div  9811  ltmuldiv2  9815  ltdivmul  9816  ledivmul  9817  ledivmulOLD  9818  ltdivmul2  9819  lt2mul2div  9820  ledivmul2  9821  ledivmul2OLD  9822  lemuldiv2  9824  ltdiv2  9829  ltrec1  9831  lerec2  9832  ledivdiv  9833  lediv2  9834  ltdiv23  9835  lediv23  9836  lediv12a  9837  recp1lt1  9842  ledivp1  9846  infm3lem  9900  supmul  9910  riotaneg  9917  negiso  9918  cju  9930  nnge1  9960  halfpos  10132  lt2halves  10136  addltmul  10137  avgle1  10141  avgle2  10142  avgle  10143  nnrecl  10153  elznn0  10230  elznn  10231  elz2  10232  zmulcl  10258  gtndiv  10281  zeo  10289  uzindOLD  10298  eqreznegel  10495  negn0  10496  supminf  10497  rebtwnz  10507  irradd  10532  irrmul  10533  max0sub  10716  xnegneg  10734  rexsub  10753  xnegid  10756  xaddcom  10758  xaddid1  10759  xnegdi  10761  xaddass  10762  rexmul  10784  xmulasslem3  10799  xadddilem  10807  flzadd  11157  intfrac2  11168  fldiv2  11171  mod0  11184  negmod0  11185  modlt  11187  modfrac  11190  flmod  11191  intfrac  11192  modmulnn  11194  modid  11199  modcyc  11205  modcyc2  11206  modadd1  11207  modmul1  11208  moddi  11213  modsubdir  11214  modirr  11215  expgt1  11347  mulexpz  11349  leexp1a  11367  expubnd  11369  sqgt0  11379  lt2sq  11384  le2sq  11385  sqge0  11387  sumsqeq0  11389  sqlecan  11416  bernneq  11434  bernneq2  11435  expnbnd  11437  digit2  11441  digit1  11442  crre  11848  crim  11849  reim0  11852  mulre  11855  rere  11856  remul2  11864  rediv  11865  immul2  11871  imdiv  11872  cjre  11873  cjreim  11894  rennim  11973  resqrex  11985  resqreu  11987  resqrcl  11988  resqrthlem  11989  sqrneglem  12001  sqrneg  12002  absreimsq  12026  absreim  12027  absnid  12032  leabs  12033  absre  12035  absresq  12036  sqabs  12041  max0add  12044  absz  12045  absdiflt  12050  absdifle  12051  lenegsq  12053  abssuble0  12061  absmax  12062  rddif  12073  absrdbnd  12074  o1rlimmul  12341  caurcvg2  12400  reefcl  12618  efgt0  12633  reeftlcl  12638  resinval  12665  recosval  12666  resin4p  12668  recos4p  12669  resincl  12670  recoscl  12671  retancl  12672  resinhcl  12686  rpcoshcl  12687  retanhcl  12689  tanhlt1  12690  tanhbnd  12691  efieq  12693  sinbnd  12710  cosbnd  12711  absefi  12726  odd2np1  12837  bezoutlem1  12967  xrsdsreclb  16670  resubdrg  16675  remetdval  18693  bl2ioo  18696  ioo2bl  18697  cnperf  18724  icccvx  18848  tchcph  19067  shft2rab  19273  volsup2  19366  volcn  19367  c1lip1  19750  plyreres  20069  aalioulem3  20120  taylthlem2  20159  reeff1o  20232  reefgim  20235  sincosq1sgn  20275  sincosq2sgn  20276  sincosq3sgn  20277  sincosq4sgn  20278  sinq12gt0  20284  pige3  20294  efif1olem4  20316  efifo  20318  relogrn  20328  logrnaddcl  20341  relogoprlem  20354  advlog  20414  advlogexp  20415  logtayl  20420  recxpcl  20435  rpcxpcl  20436  cxpge0  20443  dvcxp1  20495  logreclem  20529  angpieqvd  20541  atanre  20594  basellem9  20740  log2sumbnd  21107  readdsubgo  21791  nvsge0  22002  nmoub3i  22124  nmlnoubi  22147  isblo3i  22152  ipasslem3  22184  ipasslem9  22189  ipasslem11  22191  hmopm  23374  riesz1  23418  leopmuli  23486  leopmul  23487  leopmul2i  23488  leopnmid  23491  nmopleid  23492  cdj1i  23786  cdj3lem1  23787  cdj3i  23794  addltmulALT  23799  rexdiv  24012  xdivid  24014  xdiv0  24015  remulg  24088  rmulccn  24120  modaddabs  24896  lediv2aALT  24898  divelunit  24966  mulge0b  24972  mulle0b  24973  brbtwn2  25560  colinearalglem4  25564  colinearalg  25565  nndivlub  25924  itg2addnclem  25959  itg2addnclem2  25960  dvreasin  25982  areacirclem2  25984  areacirclem3  25985  areacirclem4  25986  areacirclem5  25988  areacirclem6  25989  areacirc  25990  expmordi  26703  lhe4.4ex1a  27217  expgrowthi  27221  mulltgt0  27363  refsum2cnlem1  27378  fmul01lt1lem1  27384  dvcosre  27411  itgsin0pilem1  27414  itgsinexplem1  27418  stoweidlem7  27426  stoweidlem10  27429  stoweidlem19  27438  stoweidlem34  27453  stoweid  27482  reseccl  27844  recsccl  27845  recotcl  27846  dpfrac1  27863
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-resscn 8982
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-in 3272  df-ss 3279
  Copyright terms: Public domain W3C validator