Theorem recni 7778

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

Syntax hints:   e. wcel 1480   CCcc 7618   RRcr 7619

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-resscn 7712

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  resubcli  8025  ltapii  8397  nncni  8730  2cn  8791  3cn  8795  4cn  8798  5cn  8800  6cn  8802  7cn  8804  8cn  8806  9cn  8808  halfcn  8934  8th4div3  8939  nn0cni  8989  numltc  9207  sqge0i  10379  lt2sqi  10380  le2sqi  10381  sq11i  10382  sqrtmsq2i  10907  0.999...  11290  ef01bndlem  11463  sin4lt0  11473  eirraplem  11483  eirr  11485  egt2lt3  11486  sqrt2irraplemnn  11857  picn  12868  sinhalfpilem  12872  cosneghalfpi  12879  sinhalfpip  12901  sinhalfpim  12902  coshalfpip  12903  coshalfpim  12904  sincosq1sgn  12907  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  cosq23lt0  12914  coseq00topi  12916  sincosq1eq  12920  sincos4thpi  12921  tan4thpi  12922  sincos6thpi  12923  taupi  13239