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

Theorem recni 7742
Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
Hypothesis
Ref Expression
recni.1  |-  A  e.  RR
Assertion
Ref Expression
recni  |-  A  e.  CC

Proof of Theorem recni
StepHypRef Expression
1 ax-resscn 7676 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3062 1  |-  A  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1463   CCcc 7582   RRcr 7583
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-resscn 7676
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  resubcli  7989  ltapii  8360  nncni  8690  2cn  8751  3cn  8755  4cn  8758  5cn  8760  6cn  8762  7cn  8764  8cn  8766  9cn  8768  halfcn  8888  8th4div3  8893  nn0cni  8943  numltc  9161  sqge0i  10330  lt2sqi  10331  le2sqi  10332  sq11i  10333  sqrtmsq2i  10858  0.999...  11241  ef01bndlem  11373  sin4lt0  11383  eirraplem  11390  eirr  11392  egt2lt3  11393  sqrt2irraplemnn  11763
  Copyright terms: Public domain W3C validator