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  8307  msqge0  8345  mulge0  8348  aprcl  8375  recexap  8381  ltm1  8568  prodgt02  8575  prodge02  8577  ltmul2  8578  lemul2  8579  lemul2a  8581  ltmulgt12  8587  lemulge12  8589  gt0div  8592  ge0div  8593  ltmuldiv2  8597  ltdivmul  8598  ltdivmul2  8600  ledivmul2  8602  lemuldiv2  8604  negiso  8677  cju  8683  nnge1  8707  halfpos  8909  lt2halves  8913  addltmul  8914  avgle1  8918  avgle2  8919  div4p1lem1div2  8931  nnrecl  8933  elznn0  9027  elznn  9028  nzadd  9064  zmulcl  9065  elz2  9080  gtndiv  9104  zeo  9114  supminfex  9348  eqreznegel  9362  negm  9363  irradd  9394  irrmul  9395  divlt1lt  9466  divle1le  9467  xnegneg  9571  rexsub  9591  xnegid  9597  xaddcom  9599  xaddid1  9600  xnegdi  9606  xaddass  9607  xleaddadd  9625  divelunit  9740  fzonmapblen  9919  expgt1  10286  mulexpzap  10288  leexp1a  10303  expubnd  10305  sqgt0ap  10316  lt2sq  10321  le2sq  10322  sqge0  10324  sumsqeq0  10326  bernneq  10367  bernneq2  10368  crre  10584  crim  10585  reim0  10588  mulreap  10591  rere  10592  remul2  10600  redivap  10601  immul2  10607  imdivap  10608  cjre  10609  cjreim  10630  rennim  10729  sqrt0rlem  10730  resqrexlemover  10737  absreimsq  10794  absreim  10795  absnid  10800  leabs  10801  absre  10804  absresq  10805  sqabs  10809  ltabs  10814  absdiflt  10819  absdifle  10820  lenegsq  10822  abssuble0  10830  dfabsmax  10944  max0addsup  10946  negfi  10954  minclpr  10963  reefcl  11288  efgt0  11304  reeftlcl  11309  resinval  11336  recosval  11337  resin4p  11339  recos4p  11340  resincl  11341  recoscl  11342  retanclap  11343  efieq  11356  sinbnd  11373  cosbnd  11374  absefi  11389  odd2np1  11482  infssuzex  11554  remetdval  12619  bl2ioo  12622  ioo2bl  12623  sincosq1sgn  12818  sincosq2sgn  12819  sincosq3sgn  12820  sincosq4sgn  12821  sinq12gt0  12822  triap  13120
  Copyright terms: Public domain W3C validator