ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  recn Unicode version

Theorem recn 7454
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 7416 . 2  |-  RR  C_  CC
21sseli 3019 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1438   CCcc 7327   RRcr 7328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-resscn 7416
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-in 3003  df-ss 3010
This theorem is referenced by:  mulid1  7464  recnd  7495  pnfnre  7508  mnfnre  7509  cnegexlem1  7636  cnegexlem2  7637  cnegexlem3  7638  cnegex  7639  renegcl  7722  resubcl  7725  negf1o  7839  mul02lem2  7845  ltaddneg  7881  ltaddnegr  7882  ltaddsub2  7894  leaddsub2  7896  leltadd  7904  ltaddpos  7909  ltaddpos2  7910  posdif  7912  lenegcon1  7923  lenegcon2  7924  addge01  7929  addge02  7930  leaddle0  7934  mullt0  7937  recexre  8031  msqge0  8069  mulge0  8072  recexap  8096  ltm1  8279  prodgt02  8286  prodge02  8288  ltmul2  8289  lemul2  8290  lemul2a  8292  ltmulgt12  8298  lemulge12  8300  gt0div  8303  ge0div  8304  ltmuldiv2  8308  ltdivmul  8309  ltdivmul2  8311  ledivmul2  8313  lemuldiv2  8315  negiso  8388  cju  8393  nnge1  8417  halfpos  8617  lt2halves  8621  addltmul  8622  avgle1  8626  avgle2  8627  div4p1lem1div2  8639  nnrecl  8641  elznn0  8735  elznn  8736  nzadd  8772  zmulcl  8773  elz2  8788  gtndiv  8811  zeo  8821  supminfex  9054  eqreznegel  9068  negm  9069  irradd  9100  irrmul  9101  divlt1lt  9170  divle1le  9171  xnegneg  9264  divelunit  9388  fzonmapblen  9563  expgt1  9958  mulexpzap  9960  leexp1a  9975  expubnd  9977  sqgt0ap  9988  lt2sq  9993  le2sq  9994  sqge0  9996  sumsqeq0  9998  bernneq  10039  bernneq2  10040  crre  10256  crim  10257  reim0  10260  mulreap  10263  rere  10264  remul2  10272  redivap  10273  immul2  10279  imdivap  10280  cjre  10281  cjreim  10302  rennim  10400  sqrt0rlem  10401  resqrexlemover  10408  absreimsq  10465  absreim  10466  absnid  10471  leabs  10472  absre  10475  absresq  10476  sqabs  10480  ltabs  10485  absdiflt  10490  absdifle  10491  lenegsq  10493  abssuble0  10501  dfabsmax  10615  max0addsup  10617  negfi  10623  odd2np1  10955  infssuzex  11027
  Copyright terms: Public domain W3C validator