Theorem recni 11159

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

Syntax hints:   ∈ wcel 2114  ℂcc 11036  ℝcr 11037

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 11095

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

This theorem is referenced by:  0cnALT  11381  renegcli  11455  resubcli  11456  recgt0ii  12062  ledivp1i  12081  ltdivp1i  12082  2cnALT  12257  8th4div3  12397  numltc  12670  sqge0i  14150  lt2sqi  14151  le2sqi  14152  sq11i  14153  crreczi  14190  faclbnd4lem1  14255  sqrtmsq2i  15350  abs3lemi  15373  0.999...  15846  bpoly4  16024  ef01bndlem  16151  sin4lt0  16162  eirrlem  16171  rpnnen2lem3  16183  rpnnen2lem9  16189  rpnnen2lem11  16191  dvdslelem  16278  divalglem1  16363  divalglem2  16364  divalglem5  16366  divalglem6  16367  divalglem9  16370  prmreclem6  16892  modsubi  17043  pcoass  24991  aaliou3lem7  26315  picn  26422  sinhalfpilem  26427  cosneghalfpi  26434  sinhalfpip  26456  sinhalfpim  26457  coshalfpip  26458  coshalfpim  26459  sincosq1sgn  26462  sincosq2sgn  26463  sincosq3sgn  26464  sincosq4sgn  26465  sincos4thpi  26477  tan4thpi  26478  tan4thpiOLD  26479  sincos6thpi  26480  pige3ALT  26484  cosne0  26493  sinord  26498  resinf1o  26500  efif1olem2  26507  efif1olem4  26509  efifo  26511  logi  26551  logimul  26578  ecxp  26637  cxpsqrtlem  26666  2irrexpq  26695  elogb  26734  logblog  26756  sqrt2cxp2logb9e3  26763  ang180lem1  26773  ang180lem2  26774  1cubrlem  26805  quartlem3  26823  asinsin  26856  acoscos  26857  asin1  26858  reasinsin  26860  acosbnd  26864  atanlogsublem  26879  atanbnd  26890  atan1  26892  log2tlbnd  26909  log2ublem1  26910  log2le1  26914  birthday  26918  basellem8  27051  basellem9  27052  cht2  27135  mumullem2  27143  chtublem  27174  chtub  27175  bposlem6  27252  bposlem7  27253  bposlem8  27254  bposlem9  27255  chebbnd1lem3  27434  chebbnd1  27435  chto1ub  27439  mulogsumlem  27494  mulog2sumlem1  27497  mulog2sumlem2  27498  mulog2sumlem3  27499  pntibndlem3  27555  ex-ceil  30518  nmblolbii  30870  ip0i  30896  ip1ilem  30897  ipasslem10  30910  siilem1  30922  siii  30924  normlem1  31181  normlem3  31183  normlem5  31185  normlem6  31186  norm-ii-i  31208  normsubi  31212  norm3adifii  31219  norm3lem  31220  normpar2i  31227  bcsiALT  31250  pjneli  31794  lnophmlem2  32088  nmbdoplbi  32095  nmcoplbi  32099  nmophmi  32102  nmbdfnlbi  32120  nmcfnlbi  32123  cnlnadjlem2  32139  cnlnadjlem7  32144  nmopadjlem  32160  nmopcoi  32166  nmopcoadji  32172  nmopcoadj0i  32174  unierri  32175  opsqrlem1  32211  dfdec100  32903  dp20u  32937  dp2ltsuc  32945  dpfrac1  32951  dpmul10  32954  decdiv10  32955  dpmul100  32956  dp3mul10  32957  dpmul1000  32958  dpexpp1  32967  dpadd2  32969  dpadd3  32971  dpmul  32972  dpmul4  32973  threehalves  32974  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  subfaclim  35370  subfacval3  35371  problem2  35848  problem3  35849  problem4  35850  problem5  35851  circum  35856  iexpire  35917  taupilem1  37635  dvacos  38026  fdc  38066  lcmineqlem23  42490  aks4d1p1p4  42510  aks4d1p1p7  42513  0cnALT3  42692  acos1half  42790  re1m1e0m0  42829  ipiiie0  42870  arearect  43643  areaquad  43644  sineq0ALT  45363  wallispilem2  46494  stirlinglem3  46504  stirlinglem4  46505  stirlinglem13  46514  stirlinglem15  46516  dirkerper  46524  fourierdlem24  46559  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  etransclem18  46680  etransclem23  46685  etransclem46  46708  etransclem47  46709  etransclem48  46710  etransc  46711  goldrasin  47330  goldratmolem2  47334  tgoldbach  48293