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

Theorem recni 7905
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 7839 . 2  |-  RR  C_  CC
2 recni.1 . 2  |-  A  e.  RR
31, 2sselii 3137 1  |-  A  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 2135   CCcc 7745   RRcr 7746
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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146  ax-resscn 7839
This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-in 3120  df-ss 3127
This theorem is referenced by:  resubcli  8155  ltapii  8527  nncni  8861  2cn  8922  3cn  8926  4cn  8929  5cn  8931  6cn  8933  7cn  8935  8cn  8937  9cn  8939  halfcn  9065  8th4div3  9070  nn0cni  9120  numltc  9341  sqge0i  10535  lt2sqi  10536  le2sqi  10537  sq11i  10538  sqrtmsq2i  11071  0.999...  11456  ef01bndlem  11691  sin4lt0  11701  eirraplem  11711  eirr  11713  egt2lt3  11714  sqrt2irraplemnn  12105  picn  13306  sinhalfpilem  13310  cosneghalfpi  13317  sinhalfpip  13339  sinhalfpim  13340  coshalfpip  13341  coshalfpim  13342  sincosq1sgn  13345  sincosq2sgn  13346  sincosq3sgn  13347  sincosq4sgn  13348  cosq23lt0  13352  coseq00topi  13354  sincosq1eq  13358  sincos4thpi  13359  tan4thpi  13360  sincos6thpi  13361  2logb9irrALT  13490  taupi  13842
  Copyright terms: Public domain W3C validator