Theorem recni 8285

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

Syntax hints:   ∈ wcel 2203  ℂcc 8124  ℝcr 8125

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 8218

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 3216  df-ss 3223

This theorem is referenced by:  resubcli  8535  ltapii  8908  nncni  9246  2cn  9307  3cn  9311  4cn  9314  5cn  9316  6cn  9318  7cn  9320  8cn  9322  9cn  9324  halfcn  9451  8th4div3  9456  nn0cni  9507  numltc  9733  sqge0i  10987  lt2sqi  10988  le2sqi  10989  sq11i  10990  sqrtmsq2i  11816  0.999...  12203  ef01bndlem  12438  sin4lt0  12449  eirraplem  12459  eirr  12461  egt2lt3  12462  sqrt2irraplemnn  12872  modsubi  13113  picn  15644  sinhalfpilem  15648  cosneghalfpi  15655  sinhalfpip  15677  sinhalfpim  15678  coshalfpip  15679  coshalfpim  15680  sincosq1sgn  15683  sincosq2sgn  15684  sincosq3sgn  15685  sincosq4sgn  15686  cosq23lt0  15690  coseq00topi  15692  sincosq1eq  15696  sincos4thpi  15697  tan4thpi  15698  sincos6thpi  15699  2logb9irrALT  15831  taupi  16850