Theorem recni 11211

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

Syntax hints:   ∈ wcel 2145  ℂcc 11086  ℝcr 11087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-resscn 11145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clel 2840  df-ss 3924

This theorem is referenced by:  0cnALT  11433  renegcli  11507  resubcli  11508  recgt0ii  12112  ledivp1i  12131  ltdivp1i  12132  2cnALT  12308  8th4div3  12455  numltc  12733  sqge0i  14215  lt2sqi  14216  le2sqi  14217  sq11i  14218  crreczi  14255  faclbnd4lem1  14320  sqrtmsq2i  15429  abs3lemi  15452  0.999...  15925  bpoly4  16103  ef01bndlem  16230  sin4lt0  16241  eirrlem  16250  rpnnen2lem3  16262  rpnnen2lem9  16268  rpnnen2lem11  16270  dvdslelem  16357  divalglem1  16442  divalglem2  16443  divalglem5  16445  divalglem6  16446  divalglem9  16449  prmreclem6  16971  modsubi  17122  pcoass  25144  aaliou3lem7  26471  picn  26579  sinhalfpilem  26586  cosneghalfpi  26593  sinhalfpip  26615  sinhalfpim  26616  coshalfpip  26617  coshalfpim  26618  sincosq1sgn  26621  sincosq2sgn  26622  sincosq3sgn  26623  sincosq4sgn  26624  sincos4thpi  26636  tan4thpi  26637  tan4thpiOLD  26638  sincos6thpi  26639  pige3ALT  26643  cosne0  26652  sinord  26657  resinf1o  26659  efif1olem2  26666  efif1olem4  26668  efifo  26670  logi  26710  logimul  26737  ecxp  26796  cxpsqrtlem  26825  2irrexpq  26854  elogb  26893  logblog  26915  sqrt2cxp2logb9e3  26922  ang180lem1  26932  ang180lem2  26933  1cubrlem  26964  quartlem3  26982  asinsin  27015  acoscos  27016  asin1  27017  reasinsin  27019  acosbnd  27023  atanlogsublem  27038  atanbnd  27049  atan1  27051  log2tlbnd  27068  log2ublem1  27069  log2le1  27073  birthday  27077  basellem8  27210  basellem9  27211  cht2  27294  mumullem2  27302  chtublem  27333  chtub  27334  bposlem6  27411  bposlem7  27412  bposlem8  27413  bposlem9  27414  chebbnd1lem3  27593  chebbnd1  27594  chto1ub  27598  mulogsumlem  27653  mulog2sumlem1  27656  mulog2sumlem2  27657  mulog2sumlem3  27658  pntibndlem3  27714  ex-ceil  30708  nmblolbii  31060  ip0i  31086  ip1ilem  31087  ipasslem10  31100  siilem1  31112  siii  31114  normlem1  31371  normlem3  31373  normlem5  31375  normlem6  31376  norm-ii-i  31398  normsubi  31402  norm3adifii  31409  norm3lem  31410  normpar2i  31417  bcsiALT  31440  pjneli  31984  lnophmlem2  32278  nmbdoplbi  32285  nmcoplbi  32289  nmophmi  32292  nmbdfnlbi  32310  nmcfnlbi  32313  cnlnadjlem2  32329  cnlnadjlem7  32334  nmopadjlem  32350  nmopcoi  32356  nmopcoadji  32362  nmopcoadj0i  32364  unierri  32365  opsqrlem1  32401  dfdec100  33087  dp20u  33110  dp2ltsuc  33118  dpfrac1  33124  dpmul10  33127  decdiv10  33128  dpmul100  33129  dp3mul10  33130  dpmul1000  33131  dpexpp1  33140  dpadd2  33142  dpadd3  33144  dpmul  33145  dpmul4  33146  threehalves  33147  hgt750lemd  34952  hgt750lem  34955  hgt750lem2  34956  subfaclim  35551  subfacval3  35552  problem2  36029  problem3  36030  problem4  36031  problem5  36032  circum  36037  iexpire  36098  taupilem1  37825  dvacos  38216  fdc  38256  lcmineqlem23  42680  aks4d1p1p4  42700  aks4d1p1p7  42703  0cnALT3  42881  acos1half  42979  re1m1e0m0  43018  ipiiie0  43059  arearect  43804  areaquad  43805  sineq0ALT  45510  wallispilem2  46638  stirlinglem3  46648  stirlinglem4  46649  stirlinglem13  46658  stirlinglem15  46660  dirkerper  46668  fourierdlem24  46703  fourierdlem103  46781  fourierdlem104  46782  sqwvfoura  46800  sqwvfourb  46801  fourierswlem  46802  fouriersw  46803  etransclem18  46824  etransclem23  46829  etransclem46  46852  etransclem47  46853  etransclem48  46854  etransc  46855  goldrasin  47474  goldratmolem2  47478  tgoldbach  48437