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

Theorem recn 7072
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 7034 . 2  |-  RR  C_  CC
21sseli 2969 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1409   CCcc 6945   RRcr 6946
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-resscn 7034
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2952  df-ss 2959
This theorem is referenced by:  mulid1  7082  recnd  7113  pnfnre  7126  mnfnre  7127  cnegexlem1  7249  cnegexlem2  7250  cnegexlem3  7251  cnegex  7252  renegcl  7335  resubcl  7338  mul02lem2  7457  ltaddneg  7493  ltaddnegr  7494  ltaddsub2  7506  leaddsub2  7508  leltadd  7516  ltaddpos  7521  ltaddpos2  7522  posdif  7524  lenegcon1  7535  lenegcon2  7536  addge01  7541  addge02  7542  leaddle0  7546  mullt0  7549  recexre  7643  msqge0  7681  mulge0  7684  recexap  7708  ltm1  7887  prodgt02  7894  prodge02  7896  ltmul2  7897  lemul2  7898  lemul2a  7900  ltmulgt12  7906  lemulge12  7908  gt0div  7911  ge0div  7912  ltmuldiv2  7916  ltdivmul  7917  ltdivmul2  7919  ledivmul2  7921  lemuldiv2  7923  cju  7989  nnge1  8013  halfpos  8213  lt2halves  8217  addltmul  8218  avgle1  8222  avgle2  8223  div4p1lem1div2  8235  nnrecl  8237  elznn0  8317  elznn  8318  nzadd  8354  zmulcl  8355  elz2  8370  gtndiv  8393  zeo  8402  eqreznegel  8646  negm  8647  irradd  8678  irrmul  8679  divlt1lt  8748  divle1le  8749  xnegneg  8847  divelunit  8971  fzonmapblen  9145  expgt1  9458  mulexpzap  9460  leexp1a  9475  expubnd  9477  sqgt0ap  9488  lt2sq  9493  le2sq  9494  sqge0  9496  sumsqeq0  9498  bernneq  9537  bernneq2  9538  crre  9685  crim  9686  reim0  9689  mulreap  9692  rere  9693  remul2  9701  redivap  9702  immul2  9708  imdivap  9709  cjre  9710  cjreim  9731  rennim  9829  sqrt0rlem  9830  resqrexlemover  9837  absreimsq  9894  absreim  9895  absnid  9900  leabs  9901  absre  9904  absresq  9905  sqabs  9909  ltabs  9914  absdiflt  9919  absdifle  9920  lenegsq  9922  abssuble0  9930  odd2np1  10184
  Copyright terms: Public domain W3C validator