Theorem recni 8286

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 8219	. 2 |- RR C_ CC
2		recni.1	. 2 |- A e. RR
3	1, 2	sselii 3235	1 |- A e. CC

Syntax hints:   e. wcel 2203   CCcc 8125   RRcr 8126

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8219

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  resubcli  8536  ltapii  8909  nncni  9247  2cn  9308  3cn  9312  4cn  9315  5cn  9317  6cn  9319  7cn  9321  8cn  9323  9cn  9325  halfcn  9452  8th4div3  9457  nn0cni  9508  numltc  9734  sqge0i  10988  lt2sqi  10989  le2sqi  10990  sq11i  10991  sqrtmsq2i  11820  0.999...  12207  ef01bndlem  12442  sin4lt0  12453  eirraplem  12463  eirr  12465  egt2lt3  12466  sqrt2irraplemnn  12876  modsubi  13117  picn  15652  sinhalfpilem  15656  cosneghalfpi  15663  sinhalfpip  15685  sinhalfpim  15686  coshalfpip  15687  coshalfpim  15688  sincosq1sgn  15691  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  cosq23lt0  15698  coseq00topi  15700  sincosq1eq  15704  sincos4thpi  15705  tan4thpi  15706  sincos6thpi  15707  2logb9irrALT  15839  taupi  16859