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

Theorem recn 6812
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
Assertion
Ref Expression
recn (A ℝ → A ℂ)

Proof of Theorem recn
StepHypRef Expression
1 ax-resscn 6775 . 2 ℝ ⊆ ℂ
21sseli 2935 1 (A ℝ → A ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1390  cc 6709  cr 6710
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-resscn 6775
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-in 2918  df-ss 2925
This theorem is referenced by:  mulid1  6822  recnd  6851  pnfnre  6864  mnfnre  6865  cnegexlem1  6983  cnegexlem2  6984  cnegexlem3  6985  cnegex  6986  renegcl  7068  resubcl  7071  mul02lem2  7181  ltaddsub2  7227  leaddsub2  7229  leltadd  7237  ltaddpos  7242  ltaddpos2  7243  posdif  7245  lenegcon1  7256  lenegcon2  7257  addge01  7262  addge02  7263  leaddle0  7267  mullt0  7270  recexre  7362  msqge0  7400  mulge0  7403  recexap  7416  ltm1  7593  prodgt02  7600  prodge02  7602  ltmul2  7603  lemul2  7604  lemul2a  7606  ltmulgt12  7612  lemulge12  7614  gt0div  7617  ge0div  7618  ltmuldiv2  7622  ltdivmul  7623  ltdivmul2  7625  ledivmul2  7627  lemuldiv2  7629  cju  7694  nnge1  7718  halfpos  7933  lt2halves  7937  addltmul  7938  avgle1  7942  avgle2  7943  nnrecl  7955  elznn0  8036  elznn  8037  zmulcl  8073  elz2  8088  gtndiv  8111  zeo  8119  eqreznegel  8325  negm  8326  irradd  8355  irrmul  8356  xnegneg  8516  divelunit  8640  fzonmapblen  8813  expgt1  8947  mulexpzap  8949  leexp1a  8963  expubnd  8965  sqgt0ap  8975  lt2sq  8980  le2sq  8981  sqge0  8983  sumsqeq0  8985  bernneq  9022  bernneq2  9023  crre  9085  crim  9086  reim0  9089  mulreap  9092  rere  9093  remul2  9101  redivap  9102  immul2  9108  imdivap  9109  cjre  9110  cjreim  9131  rennim  9211  sqrt0rlem  9212  absnid  9227  absre  9228
  Copyright terms: Public domain W3C validator