Theorem recni 8055

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

Step	Hyp	Ref	Expression
1		ax-resscn 7988	. 2 |- RR C_ CC
2		recni.1	. 2 |- A e. RR
3	1, 2	sselii 3181	1 |- A e. CC

Syntax hints:   e. wcel 2167   CCcc 7894   RRcr 7895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7988

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  resubcli  8306  ltapii  8679  nncni  9017  2cn  9078  3cn  9082  4cn  9085  5cn  9087  6cn  9089  7cn  9091  8cn  9093  9cn  9095  halfcn  9222  8th4div3  9227  nn0cni  9278  numltc  9499  sqge0i  10735  lt2sqi  10736  le2sqi  10737  sq11i  10738  sqrtmsq2i  11317  0.999...  11703  ef01bndlem  11938  sin4lt0  11949  eirraplem  11959  eirr  11961  egt2lt3  11962  sqrt2irraplemnn  12372  modsubi  12613  picn  15107  sinhalfpilem  15111  cosneghalfpi  15118  sinhalfpip  15140  sinhalfpim  15141  coshalfpip  15142  coshalfpim  15143  sincosq1sgn  15146  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  cosq23lt0  15153  coseq00topi  15155  sincosq1eq  15159  sincos4thpi  15160  tan4thpi  15161  sincos6thpi  15162  2logb9irrALT  15294  taupi  15804