Theorem recni 11157

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

Syntax hints:   ∈ wcel 2119  ℂcc 11034  ℝcr 11035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-resscn 11093

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2815  df-ss 3907

This theorem is referenced by:  0cnALT  11379  renegcli  11453  resubcli  11454  recgt0ii  12060  ledivp1i  12079  ltdivp1i  12080  2cnALT  12255  8th4div3  12395  numltc  12668  sqge0i  14148  lt2sqi  14149  le2sqi  14150  sq11i  14151  crreczi  14188  faclbnd4lem1  14253  sqrtmsq2i  15348  abs3lemi  15371  0.999...  15844  bpoly4  16022  ef01bndlem  16149  sin4lt0  16160  eirrlem  16169  rpnnen2lem3  16181  rpnnen2lem9  16187  rpnnen2lem11  16189  dvdslelem  16276  divalglem1  16361  divalglem2  16362  divalglem5  16364  divalglem6  16365  divalglem9  16368  prmreclem6  16890  modsubi  17041  pcoass  25016  aaliou3lem7  26340  picn  26447  sinhalfpilem  26452  cosneghalfpi  26459  sinhalfpip  26481  sinhalfpim  26482  coshalfpip  26483  coshalfpim  26484  sincosq1sgn  26487  sincosq2sgn  26488  sincosq3sgn  26489  sincosq4sgn  26490  sincos4thpi  26502  tan4thpi  26503  tan4thpiOLD  26504  sincos6thpi  26505  pige3ALT  26509  cosne0  26518  sinord  26523  resinf1o  26525  efif1olem2  26532  efif1olem4  26534  efifo  26536  logi  26576  logimul  26603  ecxp  26662  cxpsqrtlem  26691  2irrexpq  26720  elogb  26759  logblog  26781  sqrt2cxp2logb9e3  26788  ang180lem1  26798  ang180lem2  26799  1cubrlem  26830  quartlem3  26848  asinsin  26881  acoscos  26882  asin1  26883  reasinsin  26885  acosbnd  26889  atanlogsublem  26904  atanbnd  26915  atan1  26917  log2tlbnd  26934  log2ublem1  26935  log2le1  26939  birthday  26943  basellem8  27076  basellem9  27077  cht2  27160  mumullem2  27168  chtublem  27199  chtub  27200  bposlem6  27277  bposlem7  27278  bposlem8  27279  bposlem9  27280  chebbnd1lem3  27459  chebbnd1  27460  chto1ub  27464  mulogsumlem  27519  mulog2sumlem1  27522  mulog2sumlem2  27523  mulog2sumlem3  27524  pntibndlem3  27580  ex-ceil  30543  nmblolbii  30895  ip0i  30921  ip1ilem  30922  ipasslem10  30935  siilem1  30947  siii  30949  normlem1  31206  normlem3  31208  normlem5  31210  normlem6  31211  norm-ii-i  31233  normsubi  31237  norm3adifii  31244  norm3lem  31245  normpar2i  31252  bcsiALT  31275  pjneli  31819  lnophmlem2  32113  nmbdoplbi  32120  nmcoplbi  32124  nmophmi  32127  nmbdfnlbi  32145  nmcfnlbi  32148  cnlnadjlem2  32164  cnlnadjlem7  32169  nmopadjlem  32185  nmopcoi  32191  nmopcoadji  32197  nmopcoadj0i  32199  unierri  32200  opsqrlem1  32236  dfdec100  32929  dp20u  32963  dp2ltsuc  32971  dpfrac1  32977  dpmul10  32980  decdiv10  32981  dpmul100  32982  dp3mul10  32983  dpmul1000  32984  dpexpp1  32993  dpadd2  32995  dpadd3  32997  dpmul  32998  dpmul4  32999  threehalves  33000  hgt750lemd  34839  hgt750lem  34842  hgt750lem2  34843  subfaclim  35423  subfacval3  35424  problem2  35901  problem3  35902  problem4  35903  problem5  35904  circum  35909  iexpire  35970  taupilem1  37688  dvacos  38079  fdc  38119  lcmineqlem23  42543  aks4d1p1p4  42563  aks4d1p1p7  42566  0cnALT3  42744  acos1half  42842  re1m1e0m0  42881  ipiiie0  42922  arearect  43667  areaquad  43668  sineq0ALT  45387  wallispilem2  46516  stirlinglem3  46526  stirlinglem4  46527  stirlinglem13  46536  stirlinglem15  46538  dirkerper  46546  fourierdlem24  46581  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  etransclem18  46702  etransclem23  46707  etransclem46  46730  etransclem47  46731  etransclem48  46732  etransc  46733  goldrasin  47352  goldratmolem2  47356  tgoldbach  48315