Theorem recni 8097

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

Syntax hints:   ∈ wcel 2177  ℂcc 7936  ℝcr 7937

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8030

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3174  df-ss 3181

This theorem is referenced by:  resubcli  8348  ltapii  8721  nncni  9059  2cn  9120  3cn  9124  4cn  9127  5cn  9129  6cn  9131  7cn  9133  8cn  9135  9cn  9137  halfcn  9264  8th4div3  9269  nn0cni  9320  numltc  9542  sqge0i  10784  lt2sqi  10785  le2sqi  10786  sq11i  10787  sqrtmsq2i  11496  0.999...  11882  ef01bndlem  12117  sin4lt0  12128  eirraplem  12138  eirr  12140  egt2lt3  12141  sqrt2irraplemnn  12551  modsubi  12792  picn  15309  sinhalfpilem  15313  cosneghalfpi  15320  sinhalfpip  15342  sinhalfpim  15343  coshalfpip  15344  coshalfpim  15345  sincosq1sgn  15348  sincosq2sgn  15349  sincosq3sgn  15350  sincosq4sgn  15351  cosq23lt0  15355  coseq00topi  15357  sincosq1eq  15361  sincos4thpi  15362  tan4thpi  15363  sincos6thpi  15364  2logb9irrALT  15496  taupi  16127