Theorem recni 11194

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

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

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 11131

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

This theorem is referenced by:  0cnALT  11415  renegcli  11489  resubcli  11490  recgt0ii  12095  ledivp1i  12114  ltdivp1i  12115  2cnALT  12263  8th4div3  12408  numltc  12681  sqge0i  14159  lt2sqi  14160  le2sqi  14161  sq11i  14162  crreczi  14199  faclbnd4lem1  14264  sqrtmsq2i  15360  abs3lemi  15383  0.999...  15853  bpoly4  16031  ef01bndlem  16158  sin4lt0  16169  eirrlem  16178  rpnnen2lem3  16190  rpnnen2lem9  16196  rpnnen2lem11  16198  dvdslelem  16285  divalglem1  16370  divalglem2  16371  divalglem5  16373  divalglem6  16374  divalglem9  16377  prmreclem6  16898  modsubi  17049  pcoass  24930  aaliou3lem7  26263  picn  26373  sinhalfpilem  26378  cosneghalfpi  26385  sinhalfpip  26407  sinhalfpim  26408  coshalfpip  26409  coshalfpim  26410  sincosq1sgn  26413  sincosq2sgn  26414  sincosq3sgn  26415  sincosq4sgn  26416  sincos4thpi  26428  tan4thpi  26429  tan4thpiOLD  26430  sincos6thpi  26431  pige3ALT  26435  cosne0  26444  sinord  26449  resinf1o  26451  efif1olem2  26458  efif1olem4  26460  efifo  26462  logi  26502  logimul  26529  ecxp  26588  cxpsqrtlem  26617  2irrexpq  26646  elogb  26686  logblog  26708  sqrt2cxp2logb9e3  26715  ang180lem1  26725  ang180lem2  26726  1cubrlem  26757  quartlem3  26775  asinsin  26808  acoscos  26809  asin1  26810  reasinsin  26812  acosbnd  26816  atanlogsublem  26831  atanbnd  26842  atan1  26844  log2tlbnd  26861  log2ublem1  26862  log2le1  26866  birthday  26870  basellem8  27004  basellem9  27005  cht2  27088  mumullem2  27096  chtublem  27128  chtub  27129  bposlem6  27206  bposlem7  27207  bposlem8  27208  bposlem9  27209  chebbnd1lem3  27388  chebbnd1  27389  chto1ub  27393  mulogsumlem  27448  mulog2sumlem1  27451  mulog2sumlem2  27452  mulog2sumlem3  27453  pntibndlem3  27509  ex-ceil  30383  nmblolbii  30734  ip0i  30760  ip1ilem  30761  ipasslem10  30774  siilem1  30786  siii  30788  normlem1  31045  normlem3  31047  normlem5  31049  normlem6  31050  norm-ii-i  31072  normsubi  31076  norm3adifii  31083  norm3lem  31084  normpar2i  31091  bcsiALT  31114  pjneli  31658  lnophmlem2  31952  nmbdoplbi  31959  nmcoplbi  31963  nmophmi  31966  nmbdfnlbi  31984  nmcfnlbi  31987  cnlnadjlem2  32003  cnlnadjlem7  32008  nmopadjlem  32024  nmopcoi  32030  nmopcoadji  32036  nmopcoadj0i  32038  unierri  32039  opsqrlem1  32075  dfdec100  32761  dp20u  32804  dp2ltsuc  32812  dpfrac1  32818  dpmul10  32821  decdiv10  32822  dpmul100  32823  dp3mul10  32824  dpmul1000  32825  dpexpp1  32834  dpadd2  32836  dpadd3  32838  dpmul  32839  dpmul4  32840  threehalves  32841  hgt750lemd  34645  hgt750lem  34648  hgt750lem2  34649  subfaclim  35175  subfacval3  35176  problem2  35653  problem3  35654  problem4  35655  problem5  35656  circum  35661  iexpire  35717  taupilem1  37304  dvacos  37694  fdc  37734  lcmineqlem23  42034  aks4d1p1p4  42054  aks4d1p1p7  42057  0cnALT3  42236  acos1half  42341  re1m1e0m0  42380  ipiiie0  42421  arearect  43197  areaquad  43198  sineq0ALT  44919  wallispilem2  46057  stirlinglem3  46067  stirlinglem4  46068  stirlinglem13  46077  stirlinglem15  46079  dirkerper  46087  fourierdlem24  46122  fourierdlem103  46200  fourierdlem104  46201  sqwvfoura  46219  sqwvfourb  46220  fourierswlem  46221  fouriersw  46222  etransclem18  46243  etransclem23  46248  etransclem46  46271  etransclem47  46272  etransclem48  46273  etransc  46274  tgoldbach  47808