Theorem recni 11275

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

Syntax hints:   ∈ wcel 2108  ℂcc 11153  ℝcr 11154

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 2007  ax-8 2110  ax-resscn 11212

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

This theorem is referenced by:  0cnALT  11496  renegcli  11570  resubcli  11571  recgt0ii  12174  ledivp1i  12193  ltdivp1i  12194  2cnALT  12342  8th4div3  12486  numltc  12759  sqge0i  14227  lt2sqi  14228  le2sqi  14229  sq11i  14230  crreczi  14267  faclbnd4lem1  14332  sqrtmsq2i  15426  abs3lemi  15449  0.999...  15917  bpoly4  16095  ef01bndlem  16220  sin4lt0  16231  eirrlem  16240  rpnnen2lem3  16252  rpnnen2lem9  16258  rpnnen2lem11  16260  dvdslelem  16346  divalglem1  16431  divalglem2  16432  divalglem5  16434  divalglem6  16435  divalglem9  16438  prmreclem6  16959  modsubi  17110  pcoass  25057  aaliou3lem7  26391  picn  26501  sinhalfpilem  26505  cosneghalfpi  26512  sinhalfpip  26534  sinhalfpim  26535  coshalfpip  26536  coshalfpim  26537  sincosq1sgn  26540  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  sincos4thpi  26555  tan4thpi  26556  tan4thpiOLD  26557  sincos6thpi  26558  pige3ALT  26562  cosne0  26571  sinord  26576  resinf1o  26578  efif1olem2  26585  efif1olem4  26587  efifo  26589  logi  26629  logimul  26656  ecxp  26715  cxpsqrtlem  26744  2irrexpq  26773  elogb  26813  logblog  26835  sqrt2cxp2logb9e3  26842  ang180lem1  26852  ang180lem2  26853  1cubrlem  26884  quartlem3  26902  asinsin  26935  acoscos  26936  asin1  26937  reasinsin  26939  acosbnd  26943  atanlogsublem  26958  atanbnd  26969  atan1  26971  log2tlbnd  26988  log2ublem1  26989  log2le1  26993  birthday  26997  basellem8  27131  basellem9  27132  cht2  27215  mumullem2  27223  chtublem  27255  chtub  27256  bposlem6  27333  bposlem7  27334  bposlem8  27335  bposlem9  27336  chebbnd1lem3  27515  chebbnd1  27516  chto1ub  27520  mulogsumlem  27575  mulog2sumlem1  27578  mulog2sumlem2  27579  mulog2sumlem3  27580  pntibndlem3  27636  ex-ceil  30467  nmblolbii  30818  ip0i  30844  ip1ilem  30845  ipasslem10  30858  siilem1  30870  siii  30872  normlem1  31129  normlem3  31131  normlem5  31133  normlem6  31134  norm-ii-i  31156  normsubi  31160  norm3adifii  31167  norm3lem  31168  normpar2i  31175  bcsiALT  31198  pjneli  31742  lnophmlem2  32036  nmbdoplbi  32043  nmcoplbi  32047  nmophmi  32050  nmbdfnlbi  32068  nmcfnlbi  32071  cnlnadjlem2  32087  cnlnadjlem7  32092  nmopadjlem  32108  nmopcoi  32114  nmopcoadji  32120  nmopcoadj0i  32122  unierri  32123  opsqrlem1  32159  dfdec100  32832  dp20u  32860  dp2ltsuc  32868  dpfrac1  32874  dpmul10  32877  decdiv10  32878  dpmul100  32879  dp3mul10  32880  dpmul1000  32881  dpexpp1  32890  dpadd2  32892  dpadd3  32894  dpmul  32895  dpmul4  32896  threehalves  32897  hgt750lemd  34663  hgt750lem  34666  hgt750lem2  34667  subfaclim  35193  subfacval3  35194  problem2  35671  problem3  35672  problem4  35673  problem5  35674  circum  35679  iexpire  35735  taupilem1  37322  dvacos  37712  fdc  37752  lcmineqlem23  42052  aks4d1p1p4  42072  aks4d1p1p7  42075  0cnALT3  42294  acos1half  42388  re1m1e0m0  42427  ipiiie0  42467  arearect  43227  areaquad  43228  sineq0ALT  44957  wallispilem2  46081  stirlinglem3  46091  stirlinglem4  46092  stirlinglem13  46101  stirlinglem15  46103  dirkerper  46111  fourierdlem24  46146  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  etransclem18  46267  etransclem23  46272  etransclem46  46295  etransclem47  46296  etransclem48  46297  etransc  46298  tgoldbach  47804