Theorem recni 8146

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

Syntax hints:   ∈ wcel 2200  ℂcc 7985  ℝcr 7986

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 8079

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  8397  ltapii  8770  nncni  9108  2cn  9169  3cn  9173  4cn  9176  5cn  9178  6cn  9180  7cn  9182  8cn  9184  9cn  9186  halfcn  9313  8th4div3  9318  nn0cni  9369  numltc  9591  sqge0i  10835  lt2sqi  10836  le2sqi  10837  sq11i  10838  sqrtmsq2i  11632  0.999...  12018  ef01bndlem  12253  sin4lt0  12264  eirraplem  12274  eirr  12276  egt2lt3  12277  sqrt2irraplemnn  12687  modsubi  12928  picn  15446  sinhalfpilem  15450  cosneghalfpi  15457  sinhalfpip  15479  sinhalfpim  15480  coshalfpip  15481  coshalfpim  15482  sincosq1sgn  15485  sincosq2sgn  15486  sincosq3sgn  15487  sincosq4sgn  15488  cosq23lt0  15492  coseq00topi  15494  sincosq1eq  15498  sincos4thpi  15499  tan4thpi  15500  sincos6thpi  15501  2logb9irrALT  15633  taupi  16372