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  15131  sinhalfpilem  15135  cosneghalfpi  15142  sinhalfpip  15164  sinhalfpim  15165  coshalfpip  15166  coshalfpim  15167  sincosq1sgn  15170  sincosq2sgn  15171  sincosq3sgn  15172  sincosq4sgn  15173  cosq23lt0  15177  coseq00topi  15179  sincosq1eq  15183  sincos4thpi  15184  tan4thpi  15185  sincos6thpi  15186  2logb9irrALT  15318  taupi  15830