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

Theorem recn 7721
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 7680 . 2  |-  RR  C_  CC
21sseli 3063 1  |-  ( A  e.  RR  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1465   CCcc 7586   RRcr 7587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-resscn 7680
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054
This theorem is referenced by:  mulid1  7731  recnd  7762  pnfnre  7775  mnfnre  7776  cnegexlem1  7905  cnegexlem2  7906  cnegexlem3  7907  cnegex  7908  renegcl  7991  resubcl  7994  negf1o  8112  mul02lem2  8118  ltaddneg  8154  ltaddnegr  8155  ltaddsub2  8167  leaddsub2  8169  leltadd  8177  ltaddpos  8182  ltaddpos2  8183  posdif  8185  lenegcon1  8196  lenegcon2  8197  addge01  8202  addge02  8203  leaddle0  8207  mullt0  8210  recexre  8308  msqge0  8346  mulge0  8349  aprcl  8376  recexap  8382  ltm1  8572  prodgt02  8579  prodge02  8581  ltmul2  8582  lemul2  8583  lemul2a  8585  ltmulgt12  8591  lemulge12  8593  gt0div  8596  ge0div  8597  ltmuldiv2  8601  ltdivmul  8602  ltdivmul2  8604  ledivmul2  8606  lemuldiv2  8608  negiso  8681  cju  8687  nnge1  8711  halfpos  8919  lt2halves  8923  addltmul  8924  avgle1  8928  avgle2  8929  div4p1lem1div2  8941  nnrecl  8943  elznn0  9037  elznn  9038  nzadd  9074  zmulcl  9075  elz2  9090  gtndiv  9114  zeo  9124  supminfex  9360  eqreznegel  9374  negm  9375  irradd  9406  irrmul  9407  divlt1lt  9479  divle1le  9480  xnegneg  9584  rexsub  9604  xnegid  9610  xaddcom  9612  xaddid1  9613  xnegdi  9619  xaddass  9620  xleaddadd  9638  divelunit  9753  fzonmapblen  9932  expgt1  10299  mulexpzap  10301  leexp1a  10316  expubnd  10318  sqgt0ap  10329  lt2sq  10334  le2sq  10335  sqge0  10337  sumsqeq0  10339  bernneq  10380  bernneq2  10381  crre  10597  crim  10598  reim0  10601  mulreap  10604  rere  10605  remul2  10613  redivap  10614  immul2  10620  imdivap  10621  cjre  10622  cjreim  10643  rennim  10742  sqrt0rlem  10743  resqrexlemover  10750  absreimsq  10807  absreim  10808  absnid  10813  leabs  10814  absre  10817  absresq  10818  sqabs  10822  ltabs  10827  absdiflt  10832  absdifle  10833  lenegsq  10835  abssuble0  10843  dfabsmax  10957  max0addsup  10959  negfi  10967  minclpr  10976  reefcl  11301  efgt0  11317  reeftlcl  11322  resinval  11349  recosval  11350  resin4p  11352  recos4p  11353  resincl  11354  recoscl  11355  retanclap  11356  efieq  11369  sinbnd  11386  cosbnd  11387  absefi  11402  odd2np1  11497  infssuzex  11569  remetdval  12635  bl2ioo  12638  ioo2bl  12639  sincosq1sgn  12834  sincosq2sgn  12835  sincosq3sgn  12836  sincosq4sgn  12837  sinq12gt0  12838  triap  13151
  Copyright terms: Public domain W3C validator