Theorem recni 8057

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 7990	. 2 ⊢ ℝ ⊆ ℂ
2		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
3	1, 2	sselii 3181	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2167  ℂcc 7896  ℝcr 7897

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 7990

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  8308  ltapii  8681  nncni  9019  2cn  9080  3cn  9084  4cn  9087  5cn  9089  6cn  9091  7cn  9093  8cn  9095  9cn  9097  halfcn  9224  8th4div3  9229  nn0cni  9280  numltc  9501  sqge0i  10737  lt2sqi  10738  le2sqi  10739  sq11i  10740  sqrtmsq2i  11319  0.999...  11705  ef01bndlem  11940  sin4lt0  11951  eirraplem  11961  eirr  11963  egt2lt3  11964  sqrt2irraplemnn  12374  modsubi  12615  picn  15109  sinhalfpilem  15113  cosneghalfpi  15120  sinhalfpip  15142  sinhalfpim  15143  coshalfpip  15144  coshalfpim  15145  sincosq1sgn  15148  sincosq2sgn  15149  sincosq3sgn  15150  sincosq4sgn  15151  cosq23lt0  15155  coseq00topi  15157  sincosq1eq  15161  sincos4thpi  15162  tan4thpi  15163  sincos6thpi  15164  2logb9irrALT  15296  taupi  15808