Theorem recni 11188

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

Syntax hints:   ∈ wcel 2109  ℂcc 11066  ℝcr 11067

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 11125

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

This theorem is referenced by:  0cnALT  11409  renegcli  11483  resubcli  11484  recgt0ii  12089  ledivp1i  12108  ltdivp1i  12109  2cnALT  12262  8th4div3  12402  numltc  12675  sqge0i  14153  lt2sqi  14154  le2sqi  14155  sq11i  14156  crreczi  14193  faclbnd4lem1  14258  sqrtmsq2i  15354  abs3lemi  15377  0.999...  15847  bpoly4  16025  ef01bndlem  16152  sin4lt0  16163  eirrlem  16172  rpnnen2lem3  16184  rpnnen2lem9  16190  rpnnen2lem11  16192  dvdslelem  16279  divalglem1  16364  divalglem2  16365  divalglem5  16367  divalglem6  16368  divalglem9  16371  prmreclem6  16892  modsubi  17043  pcoass  24924  aaliou3lem7  26257  picn  26367  sinhalfpilem  26372  cosneghalfpi  26379  sinhalfpip  26401  sinhalfpim  26402  coshalfpip  26403  coshalfpim  26404  sincosq1sgn  26407  sincosq2sgn  26408  sincosq3sgn  26409  sincosq4sgn  26410  sincos4thpi  26422  tan4thpi  26423  tan4thpiOLD  26424  sincos6thpi  26425  pige3ALT  26429  cosne0  26438  sinord  26443  resinf1o  26445  efif1olem2  26452  efif1olem4  26454  efifo  26456  logi  26496  logimul  26523  ecxp  26582  cxpsqrtlem  26611  2irrexpq  26640  elogb  26680  logblog  26702  sqrt2cxp2logb9e3  26709  ang180lem1  26719  ang180lem2  26720  1cubrlem  26751  quartlem3  26769  asinsin  26802  acoscos  26803  asin1  26804  reasinsin  26806  acosbnd  26810  atanlogsublem  26825  atanbnd  26836  atan1  26838  log2tlbnd  26855  log2ublem1  26856  log2le1  26860  birthday  26864  basellem8  26998  basellem9  26999  cht2  27082  mumullem2  27090  chtublem  27122  chtub  27123  bposlem6  27200  bposlem7  27201  bposlem8  27202  bposlem9  27203  chebbnd1lem3  27382  chebbnd1  27383  chto1ub  27387  mulogsumlem  27442  mulog2sumlem1  27445  mulog2sumlem2  27446  mulog2sumlem3  27447  pntibndlem3  27503  ex-ceil  30377  nmblolbii  30728  ip0i  30754  ip1ilem  30755  ipasslem10  30768  siilem1  30780  siii  30782  normlem1  31039  normlem3  31041  normlem5  31043  normlem6  31044  norm-ii-i  31066  normsubi  31070  norm3adifii  31077  norm3lem  31078  normpar2i  31085  bcsiALT  31108  pjneli  31652  lnophmlem2  31946  nmbdoplbi  31953  nmcoplbi  31957  nmophmi  31960  nmbdfnlbi  31978  nmcfnlbi  31981  cnlnadjlem2  31997  cnlnadjlem7  32002  nmopadjlem  32018  nmopcoi  32024  nmopcoadji  32030  nmopcoadj0i  32032  unierri  32033  opsqrlem1  32069  dfdec100  32755  dp20u  32798  dp2ltsuc  32806  dpfrac1  32812  dpmul10  32815  decdiv10  32816  dpmul100  32817  dp3mul10  32818  dpmul1000  32819  dpexpp1  32828  dpadd2  32830  dpadd3  32832  dpmul  32833  dpmul4  32834  threehalves  32835  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  subfaclim  35175  subfacval3  35176  problem2  35653  problem3  35654  problem4  35655  problem5  35656  circum  35661  iexpire  35722  taupilem1  37309  dvacos  37699  fdc  37739  lcmineqlem23  42039  aks4d1p1p4  42059  aks4d1p1p7  42062  0cnALT3  42241  acos1half  42346  re1m1e0m0  42385  ipiiie0  42426  arearect  43204  areaquad  43205  sineq0ALT  44926  wallispilem2  46064  stirlinglem3  46074  stirlinglem4  46075  stirlinglem13  46084  stirlinglem15  46086  dirkerper  46094  fourierdlem24  46129  fourierdlem103  46207  fourierdlem104  46208  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  etransclem18  46250  etransclem23  46255  etransclem46  46278  etransclem47  46279  etransclem48  46280  etransc  46281  tgoldbach  47818