Theorem recni 11123

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

Syntax hints:   ∈ wcel 2111  ℂcc 11001  ℝcr 11002

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 2113  ax-resscn 11060

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

This theorem is referenced by:  0cnALT  11345  renegcli  11419  resubcli  11420  recgt0ii  12025  ledivp1i  12044  ltdivp1i  12045  2cnALT  12198  8th4div3  12338  numltc  12611  sqge0i  14092  lt2sqi  14093  le2sqi  14094  sq11i  14095  crreczi  14132  faclbnd4lem1  14197  sqrtmsq2i  15292  abs3lemi  15315  0.999...  15785  bpoly4  15963  ef01bndlem  16090  sin4lt0  16101  eirrlem  16110  rpnnen2lem3  16122  rpnnen2lem9  16128  rpnnen2lem11  16130  dvdslelem  16217  divalglem1  16302  divalglem2  16303  divalglem5  16305  divalglem6  16306  divalglem9  16309  prmreclem6  16830  modsubi  16981  pcoass  24949  aaliou3lem7  26282  picn  26392  sinhalfpilem  26397  cosneghalfpi  26404  sinhalfpip  26426  sinhalfpim  26427  coshalfpip  26428  coshalfpim  26429  sincosq1sgn  26432  sincosq2sgn  26433  sincosq3sgn  26434  sincosq4sgn  26435  sincos4thpi  26447  tan4thpi  26448  tan4thpiOLD  26449  sincos6thpi  26450  pige3ALT  26454  cosne0  26463  sinord  26468  resinf1o  26470  efif1olem2  26477  efif1olem4  26479  efifo  26481  logi  26521  logimul  26548  ecxp  26607  cxpsqrtlem  26636  2irrexpq  26665  elogb  26705  logblog  26727  sqrt2cxp2logb9e3  26734  ang180lem1  26744  ang180lem2  26745  1cubrlem  26776  quartlem3  26794  asinsin  26827  acoscos  26828  asin1  26829  reasinsin  26831  acosbnd  26835  atanlogsublem  26850  atanbnd  26861  atan1  26863  log2tlbnd  26880  log2ublem1  26881  log2le1  26885  birthday  26889  basellem8  27023  basellem9  27024  cht2  27107  mumullem2  27115  chtublem  27147  chtub  27148  bposlem6  27225  bposlem7  27226  bposlem8  27227  bposlem9  27228  chebbnd1lem3  27407  chebbnd1  27408  chto1ub  27412  mulogsumlem  27467  mulog2sumlem1  27470  mulog2sumlem2  27471  mulog2sumlem3  27472  pntibndlem3  27528  ex-ceil  30423  nmblolbii  30774  ip0i  30800  ip1ilem  30801  ipasslem10  30814  siilem1  30826  siii  30828  normlem1  31085  normlem3  31087  normlem5  31089  normlem6  31090  norm-ii-i  31112  normsubi  31116  norm3adifii  31123  norm3lem  31124  normpar2i  31131  bcsiALT  31154  pjneli  31698  lnophmlem2  31992  nmbdoplbi  31999  nmcoplbi  32003  nmophmi  32006  nmbdfnlbi  32024  nmcfnlbi  32027  cnlnadjlem2  32043  cnlnadjlem7  32048  nmopadjlem  32064  nmopcoi  32070  nmopcoadji  32076  nmopcoadj0i  32078  unierri  32079  opsqrlem1  32115  dfdec100  32808  dp20u  32853  dp2ltsuc  32861  dpfrac1  32867  dpmul10  32870  decdiv10  32871  dpmul100  32872  dp3mul10  32873  dpmul1000  32874  dpexpp1  32883  dpadd2  32885  dpadd3  32887  dpmul  32888  dpmul4  32889  threehalves  32890  hgt750lemd  34656  hgt750lem  34659  hgt750lem2  34660  subfaclim  35220  subfacval3  35221  problem2  35698  problem3  35699  problem4  35700  problem5  35701  circum  35706  iexpire  35767  taupilem1  37354  dvacos  37744  fdc  37784  lcmineqlem23  42083  aks4d1p1p4  42103  aks4d1p1p7  42106  0cnALT3  42285  acos1half  42390  re1m1e0m0  42429  ipiiie0  42470  arearect  43247  areaquad  43248  sineq0ALT  44968  wallispilem2  46103  stirlinglem3  46113  stirlinglem4  46114  stirlinglem13  46123  stirlinglem15  46125  dirkerper  46133  fourierdlem24  46168  fourierdlem103  46246  fourierdlem104  46247  sqwvfoura  46265  sqwvfourb  46266  fourierswlem  46267  fouriersw  46268  etransclem18  46289  etransclem23  46294  etransclem46  46317  etransclem47  46318  etransclem48  46319  etransc  46320  tgoldbach  47847