Theorem recni 8184

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

Syntax hints:   ∈ wcel 2200  ℂcc 8023  ℝcr 8024

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 8117

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 3204  df-ss 3211

This theorem is referenced by:  resubcli  8435  ltapii  8808  nncni  9146  2cn  9207  3cn  9211  4cn  9214  5cn  9216  6cn  9218  7cn  9220  8cn  9222  9cn  9224  halfcn  9351  8th4div3  9356  nn0cni  9407  numltc  9629  sqge0i  10881  lt2sqi  10882  le2sqi  10883  sq11i  10884  sqrtmsq2i  11689  0.999...  12075  ef01bndlem  12310  sin4lt0  12321  eirraplem  12331  eirr  12333  egt2lt3  12334  sqrt2irraplemnn  12744  modsubi  12985  picn  15504  sinhalfpilem  15508  cosneghalfpi  15515  sinhalfpip  15537  sinhalfpim  15538  coshalfpip  15539  coshalfpim  15540  sincosq1sgn  15543  sincosq2sgn  15544  sincosq3sgn  15545  sincosq4sgn  15546  cosq23lt0  15550  coseq00topi  15552  sincosq1eq  15556  sincos4thpi  15557  tan4thpi  15558  sincos6thpi  15559  2logb9irrALT  15691  taupi  16627