Theorem recni 8174

Description: A real number is a complex number. (Contributed by NM, 1-Mar-1995.)

Hypothesis

Ref	Expression
recni.1	⊢ 𝐴 ∈ ℝ

Assertion

Ref	Expression
recni	⊢ 𝐴 ∈ ℂ

Proof of Theorem recni

Step	Hyp	Ref	Expression
1		ax-resscn 8107	. 2 ⊢ ℝ ⊆ ℂ
2		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
3	1, 2	sselii 3221	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2200  ℂcc 8013  ℝcr 8014

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8107

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  resubcli  8425  ltapii  8798  nncni  9136  2cn  9197  3cn  9201  4cn  9204  5cn  9206  6cn  9208  7cn  9210  8cn  9212  9cn  9214  halfcn  9341  8th4div3  9346  nn0cni  9397  numltc  9619  sqge0i  10865  lt2sqi  10866  le2sqi  10867  sq11i  10868  sqrtmsq2i  11667  0.999...  12053  ef01bndlem  12288  sin4lt0  12299  eirraplem  12309  eirr  12311  egt2lt3  12312  sqrt2irraplemnn  12722  modsubi  12963  picn  15482  sinhalfpilem  15486  cosneghalfpi  15493  sinhalfpip  15515  sinhalfpim  15516  coshalfpip  15517  coshalfpim  15518  sincosq1sgn  15521  sincosq2sgn  15522  sincosq3sgn  15523  sincosq4sgn  15524  cosq23lt0  15528  coseq00topi  15530  sincosq1eq  15534  sincos4thpi  15535  tan4thpi  15536  sincos6thpi  15537  2logb9irrALT  15669  taupi  16555