Theorem recni 11195

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

Syntax hints:   ∈ wcel 2109  ℂcc 11073  ℝcr 11074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-resscn 11132

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2804  df-ss 3934

This theorem is referenced by:  0cnALT  11416  renegcli  11490  resubcli  11491  recgt0ii  12096  ledivp1i  12115  ltdivp1i  12116  2cnALT  12269  8th4div3  12409  numltc  12682  sqge0i  14160  lt2sqi  14161  le2sqi  14162  sq11i  14163  crreczi  14200  faclbnd4lem1  14265  sqrtmsq2i  15361  abs3lemi  15384  0.999...  15854  bpoly4  16032  ef01bndlem  16159  sin4lt0  16170  eirrlem  16179  rpnnen2lem3  16191  rpnnen2lem9  16197  rpnnen2lem11  16199  dvdslelem  16286  divalglem1  16371  divalglem2  16372  divalglem5  16374  divalglem6  16375  divalglem9  16378  prmreclem6  16899  modsubi  17050  pcoass  24931  aaliou3lem7  26264  picn  26374  sinhalfpilem  26379  cosneghalfpi  26386  sinhalfpip  26408  sinhalfpim  26409  coshalfpip  26410  coshalfpim  26411  sincosq1sgn  26414  sincosq2sgn  26415  sincosq3sgn  26416  sincosq4sgn  26417  sincos4thpi  26429  tan4thpi  26430  tan4thpiOLD  26431  sincos6thpi  26432  pige3ALT  26436  cosne0  26445  sinord  26450  resinf1o  26452  efif1olem2  26459  efif1olem4  26461  efifo  26463  logi  26503  logimul  26530  ecxp  26589  cxpsqrtlem  26618  2irrexpq  26647  elogb  26687  logblog  26709  sqrt2cxp2logb9e3  26716  ang180lem1  26726  ang180lem2  26727  1cubrlem  26758  quartlem3  26776  asinsin  26809  acoscos  26810  asin1  26811  reasinsin  26813  acosbnd  26817  atanlogsublem  26832  atanbnd  26843  atan1  26845  log2tlbnd  26862  log2ublem1  26863  log2le1  26867  birthday  26871  basellem8  27005  basellem9  27006  cht2  27089  mumullem2  27097  chtublem  27129  chtub  27130  bposlem6  27207  bposlem7  27208  bposlem8  27209  bposlem9  27210  chebbnd1lem3  27389  chebbnd1  27390  chto1ub  27394  mulogsumlem  27449  mulog2sumlem1  27452  mulog2sumlem2  27453  mulog2sumlem3  27454  pntibndlem3  27510  ex-ceil  30384  nmblolbii  30735  ip0i  30761  ip1ilem  30762  ipasslem10  30775  siilem1  30787  siii  30789  normlem1  31046  normlem3  31048  normlem5  31050  normlem6  31051  norm-ii-i  31073  normsubi  31077  norm3adifii  31084  norm3lem  31085  normpar2i  31092  bcsiALT  31115  pjneli  31659  lnophmlem2  31953  nmbdoplbi  31960  nmcoplbi  31964  nmophmi  31967  nmbdfnlbi  31985  nmcfnlbi  31988  cnlnadjlem2  32004  cnlnadjlem7  32009  nmopadjlem  32025  nmopcoi  32031  nmopcoadji  32037  nmopcoadj0i  32039  unierri  32040  opsqrlem1  32076  dfdec100  32762  dp20u  32805  dp2ltsuc  32813  dpfrac1  32819  dpmul10  32822  decdiv10  32823  dpmul100  32824  dp3mul10  32825  dpmul1000  32826  dpexpp1  32835  dpadd2  32837  dpadd3  32839  dpmul  32840  dpmul4  32841  threehalves  32842  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  subfaclim  35182  subfacval3  35183  problem2  35660  problem3  35661  problem4  35662  problem5  35663  circum  35668  iexpire  35729  taupilem1  37316  dvacos  37706  fdc  37746  lcmineqlem23  42046  aks4d1p1p4  42066  aks4d1p1p7  42069  0cnALT3  42248  acos1half  42353  re1m1e0m0  42392  ipiiie0  42433  arearect  43211  areaquad  43212  sineq0ALT  44933  wallispilem2  46071  stirlinglem3  46081  stirlinglem4  46082  stirlinglem13  46091  stirlinglem15  46093  dirkerper  46101  fourierdlem24  46136  fourierdlem103  46214  fourierdlem104  46215  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  etransclem18  46257  etransclem23  46262  etransclem46  46285  etransclem47  46286  etransclem48  46287  etransc  46288  tgoldbach  47822