Theorem recni 11133

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

Syntax hints:   ∈ wcel 2113  ℂcc 11011  ℝcr 11012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-resscn 11070

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2808  df-ss 3915

This theorem is referenced by:  0cnALT  11355  renegcli  11429  resubcli  11430  recgt0ii  12035  ledivp1i  12054  ltdivp1i  12055  2cnALT  12208  8th4div3  12348  numltc  12620  sqge0i  14097  lt2sqi  14098  le2sqi  14099  sq11i  14100  crreczi  14137  faclbnd4lem1  14202  sqrtmsq2i  15297  abs3lemi  15320  0.999...  15790  bpoly4  15968  ef01bndlem  16095  sin4lt0  16106  eirrlem  16115  rpnnen2lem3  16127  rpnnen2lem9  16133  rpnnen2lem11  16135  dvdslelem  16222  divalglem1  16307  divalglem2  16308  divalglem5  16310  divalglem6  16311  divalglem9  16314  prmreclem6  16835  modsubi  16986  pcoass  24952  aaliou3lem7  26285  picn  26395  sinhalfpilem  26400  cosneghalfpi  26407  sinhalfpip  26429  sinhalfpim  26430  coshalfpip  26431  coshalfpim  26432  sincosq1sgn  26435  sincosq2sgn  26436  sincosq3sgn  26437  sincosq4sgn  26438  sincos4thpi  26450  tan4thpi  26451  tan4thpiOLD  26452  sincos6thpi  26453  pige3ALT  26457  cosne0  26466  sinord  26471  resinf1o  26473  efif1olem2  26480  efif1olem4  26482  efifo  26484  logi  26524  logimul  26551  ecxp  26610  cxpsqrtlem  26639  2irrexpq  26668  elogb  26708  logblog  26730  sqrt2cxp2logb9e3  26737  ang180lem1  26747  ang180lem2  26748  1cubrlem  26779  quartlem3  26797  asinsin  26830  acoscos  26831  asin1  26832  reasinsin  26834  acosbnd  26838  atanlogsublem  26853  atanbnd  26864  atan1  26866  log2tlbnd  26883  log2ublem1  26884  log2le1  26888  birthday  26892  basellem8  27026  basellem9  27027  cht2  27110  mumullem2  27118  chtublem  27150  chtub  27151  bposlem6  27228  bposlem7  27229  bposlem8  27230  bposlem9  27231  chebbnd1lem3  27410  chebbnd1  27411  chto1ub  27415  mulogsumlem  27470  mulog2sumlem1  27473  mulog2sumlem2  27474  mulog2sumlem3  27475  pntibndlem3  27531  ex-ceil  30430  nmblolbii  30781  ip0i  30807  ip1ilem  30808  ipasslem10  30821  siilem1  30833  siii  30835  normlem1  31092  normlem3  31094  normlem5  31096  normlem6  31097  norm-ii-i  31119  normsubi  31123  norm3adifii  31130  norm3lem  31131  normpar2i  31138  bcsiALT  31161  pjneli  31705  lnophmlem2  31999  nmbdoplbi  32006  nmcoplbi  32010  nmophmi  32013  nmbdfnlbi  32031  nmcfnlbi  32034  cnlnadjlem2  32050  cnlnadjlem7  32055  nmopadjlem  32071  nmopcoi  32077  nmopcoadji  32083  nmopcoadj0i  32085  unierri  32086  opsqrlem1  32122  dfdec100  32818  dp20u  32865  dp2ltsuc  32873  dpfrac1  32879  dpmul10  32882  decdiv10  32883  dpmul100  32884  dp3mul10  32885  dpmul1000  32886  dpexpp1  32895  dpadd2  32897  dpadd3  32899  dpmul  32900  dpmul4  32901  threehalves  32902  hgt750lemd  34682  hgt750lem  34685  hgt750lem2  34686  subfaclim  35253  subfacval3  35254  problem2  35731  problem3  35732  problem4  35733  problem5  35734  circum  35739  iexpire  35800  taupilem1  37386  dvacos  37765  fdc  37805  lcmineqlem23  42164  aks4d1p1p4  42184  aks4d1p1p7  42187  0cnALT3  42371  acos1half  42476  re1m1e0m0  42515  ipiiie0  42556  arearect  43332  areaquad  43333  sineq0ALT  45053  wallispilem2  46188  stirlinglem3  46198  stirlinglem4  46199  stirlinglem13  46208  stirlinglem15  46210  dirkerper  46218  fourierdlem24  46253  fourierdlem103  46331  fourierdlem104  46332  sqwvfoura  46350  sqwvfourb  46351  fourierswlem  46352  fouriersw  46353  etransclem18  46374  etransclem23  46379  etransclem46  46402  etransclem47  46403  etransclem48  46404  etransc  46405  tgoldbach  47941