Theorem recni 11260

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

Syntax hints:   ∈ wcel 2098  ℂcc 11138  ℝcr 11139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-resscn 11197

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-clel 2802  df-ss 3961

This theorem is referenced by:  0cnALT  11480  renegcli  11553  resubcli  11554  recgt0ii  12153  ledivp1i  12172  ltdivp1i  12173  2cnALT  12321  8th4div3  12465  numltc  12736  sqge0i  14187  lt2sqi  14188  le2sqi  14189  sq11i  14190  crreczi  14226  faclbnd4lem1  14288  sqrtmsq2i  15370  abs3lemi  15393  0.999...  15863  bpoly4  16039  ef01bndlem  16164  sin4lt0  16175  eirrlem  16184  rpnnen2lem3  16196  rpnnen2lem9  16202  rpnnen2lem11  16204  dvdslelem  16289  divalglem1  16374  divalglem2  16375  divalglem5  16377  divalglem6  16378  divalglem9  16381  prmreclem6  16893  modsubi  17044  pcoass  24995  aaliou3lem7  26329  picn  26439  sinhalfpilem  26443  cosneghalfpi  26450  sinhalfpip  26472  sinhalfpim  26473  coshalfpip  26474  coshalfpim  26475  sincosq1sgn  26478  sincosq2sgn  26479  sincosq3sgn  26480  sincosq4sgn  26481  sincos4thpi  26493  tan4thpi  26494  sincos6thpi  26495  pige3ALT  26499  cosne0  26508  sinord  26513  resinf1o  26515  efif1olem2  26522  efif1olem4  26524  efifo  26526  logi  26566  logimul  26593  ecxp  26652  cxpsqrtlem  26681  2irrexpq  26710  elogb  26747  logblog  26769  sqrt2cxp2logb9e3  26776  ang180lem1  26786  ang180lem2  26787  1cubrlem  26818  quartlem3  26836  asinsin  26869  acoscos  26870  asin1  26871  reasinsin  26873  acosbnd  26877  atanlogsublem  26892  atanbnd  26903  atan1  26905  log2tlbnd  26922  log2ublem1  26923  log2le1  26927  birthday  26931  basellem8  27065  basellem9  27066  cht2  27149  mumullem2  27157  chtublem  27189  chtub  27190  bposlem6  27267  bposlem7  27268  bposlem8  27269  bposlem9  27270  chebbnd1lem3  27449  chebbnd1  27450  chto1ub  27454  mulogsumlem  27509  mulog2sumlem1  27512  mulog2sumlem2  27513  mulog2sumlem3  27514  pntibndlem3  27570  ex-ceil  30330  nmblolbii  30681  ip0i  30707  ip1ilem  30708  ipasslem10  30721  siilem1  30733  siii  30735  normlem1  30992  normlem3  30994  normlem5  30996  normlem6  30997  norm-ii-i  31019  normsubi  31023  norm3adifii  31030  norm3lem  31031  normpar2i  31038  bcsiALT  31061  pjneli  31605  lnophmlem2  31899  nmbdoplbi  31906  nmcoplbi  31910  nmophmi  31913  nmbdfnlbi  31931  nmcfnlbi  31934  cnlnadjlem2  31950  cnlnadjlem7  31955  nmopadjlem  31971  nmopcoi  31977  nmopcoadji  31983  nmopcoadj0i  31985  unierri  31986  opsqrlem1  32022  dfdec100  32678  dp20u  32686  dp2ltsuc  32694  dpfrac1  32700  dpmul10  32703  decdiv10  32704  dpmul100  32705  dp3mul10  32706  dpmul1000  32707  dpexpp1  32716  dpadd2  32718  dpadd3  32720  dpmul  32721  dpmul4  32722  threehalves  32723  hgt750lemd  34411  hgt750lem  34414  hgt750lem2  34415  subfaclim  34929  subfacval3  34930  problem2  35401  problem3  35402  problem4  35403  problem5  35404  circum  35409  iexpire  35460  taupilem1  36931  dvacos  37309  fdc  37349  lcmineqlem23  41654  aks4d1p1p4  41674  aks4d1p1p7  41677  0cnALT3  41970  re1m1e0m0  42087  ipiiie0  42127  acos1half  42233  arearect  42785  areaquad  42786  sineq0ALT  44518  wallispilem2  45592  stirlinglem3  45602  stirlinglem4  45603  stirlinglem13  45612  stirlinglem15  45614  dirkerper  45622  fourierdlem24  45657  fourierdlem103  45735  fourierdlem104  45736  sqwvfoura  45754  sqwvfourb  45755  fourierswlem  45756  fouriersw  45757  etransclem18  45778  etransclem23  45783  etransclem46  45806  etransclem47  45807  etransclem48  45808  etransc  45809  tgoldbach  47294