Theorem recni 11150

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

Syntax hints:   ∈ wcel 2114  ℂcc 11027  ℝcr 11028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-resscn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3907

This theorem is referenced by:  0cnALT  11372  renegcli  11446  resubcli  11447  recgt0ii  12053  ledivp1i  12072  ltdivp1i  12073  2cnALT  12248  8th4div3  12388  numltc  12661  sqge0i  14141  lt2sqi  14142  le2sqi  14143  sq11i  14144  crreczi  14181  faclbnd4lem1  14246  sqrtmsq2i  15341  abs3lemi  15364  0.999...  15837  bpoly4  16015  ef01bndlem  16142  sin4lt0  16153  eirrlem  16162  rpnnen2lem3  16174  rpnnen2lem9  16180  rpnnen2lem11  16182  dvdslelem  16269  divalglem1  16354  divalglem2  16355  divalglem5  16357  divalglem6  16358  divalglem9  16361  prmreclem6  16883  modsubi  17034  pcoass  25001  aaliou3lem7  26326  picn  26435  sinhalfpilem  26440  cosneghalfpi  26447  sinhalfpip  26469  sinhalfpim  26470  coshalfpip  26471  coshalfpim  26472  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  sincos4thpi  26490  tan4thpi  26491  tan4thpiOLD  26492  sincos6thpi  26493  pige3ALT  26497  cosne0  26506  sinord  26511  resinf1o  26513  efif1olem2  26520  efif1olem4  26522  efifo  26524  logi  26564  logimul  26591  ecxp  26650  cxpsqrtlem  26679  2irrexpq  26708  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  27188  chtub  27189  bposlem6  27266  bposlem7  27267  bposlem8  27268  bposlem9  27269  chebbnd1lem3  27448  chebbnd1  27449  chto1ub  27453  mulogsumlem  27508  mulog2sumlem1  27511  mulog2sumlem2  27512  mulog2sumlem3  27513  pntibndlem3  27569  ex-ceil  30533  nmblolbii  30885  ip0i  30911  ip1ilem  30912  ipasslem10  30925  siilem1  30937  siii  30939  normlem1  31196  normlem3  31198  normlem5  31200  normlem6  31201  norm-ii-i  31223  normsubi  31227  norm3adifii  31234  norm3lem  31235  normpar2i  31242  bcsiALT  31265  pjneli  31809  lnophmlem2  32103  nmbdoplbi  32110  nmcoplbi  32114  nmophmi  32117  nmbdfnlbi  32135  nmcfnlbi  32138  cnlnadjlem2  32154  cnlnadjlem7  32159  nmopadjlem  32175  nmopcoi  32181  nmopcoadji  32187  nmopcoadj0i  32189  unierri  32190  opsqrlem1  32226  dfdec100  32918  dp20u  32952  dp2ltsuc  32960  dpfrac1  32966  dpmul10  32969  decdiv10  32970  dpmul100  32971  dp3mul10  32972  dpmul1000  32973  dpexpp1  32982  dpadd2  32984  dpadd3  32986  dpmul  32987  dpmul4  32988  threehalves  32989  hgt750lemd  34808  hgt750lem  34811  hgt750lem2  34812  subfaclim  35386  subfacval3  35387  problem2  35864  problem3  35865  problem4  35866  problem5  35867  circum  35872  iexpire  35933  taupilem1  37651  dvacos  38040  fdc  38080  lcmineqlem23  42504  aks4d1p1p4  42524  aks4d1p1p7  42527  0cnALT3  42706  acos1half  42804  re1m1e0m0  42843  ipiiie0  42884  arearect  43661  areaquad  43662  sineq0ALT  45381  wallispilem2  46512  stirlinglem3  46522  stirlinglem4  46523  stirlinglem13  46532  stirlinglem15  46534  dirkerper  46542  fourierdlem24  46577  fourierdlem103  46655  fourierdlem104  46656  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  etransclem18  46698  etransclem23  46703  etransclem46  46726  etransclem47  46727  etransclem48  46728  etransc  46729  goldrasin  47344  tgoldbach  48305