Theorem recni 11068

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

Syntax hints:   ∈ wcel 2105  ℂcc 10948  ℝcr 10949

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-resscn 11007

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3442  df-in 3903  df-ss 3913

This theorem is referenced by:  0cnALT  11288  renegcli  11361  resubcli  11362  recgt0ii  11960  ledivp1i  11979  ltdivp1i  11980  2cnALT  12128  8th4div3  12272  numltc  12542  sqge0i  13984  lt2sqi  13985  le2sqi  13986  sq11i  13987  crreczi  14022  faclbnd4lem1  14086  sqrtmsq2i  15175  abs3lemi  15198  0.999...  15669  bpoly4  15845  ef01bndlem  15969  sin4lt0  15980  eirrlem  15989  rpnnen2lem3  16001  rpnnen2lem9  16007  rpnnen2lem11  16009  dvdslelem  16094  divalglem1  16179  divalglem2  16180  divalglem5  16182  divalglem6  16183  divalglem9  16186  prmreclem6  16696  modsubi  16847  pcoass  24267  aaliou3lem7  25589  picn  25696  sinhalfpilem  25700  cosneghalfpi  25707  sinhalfpip  25729  sinhalfpim  25730  coshalfpip  25731  coshalfpim  25732  sincosq1sgn  25735  sincosq2sgn  25736  sincosq3sgn  25737  sincosq4sgn  25738  sincos4thpi  25750  tan4thpi  25751  sincos6thpi  25752  pige3ALT  25756  cosne0  25765  sinord  25770  resinf1o  25772  efif1olem2  25779  efif1olem4  25781  efifo  25783  logimul  25849  ecxp  25908  cxpsqrtlem  25937  2irrexpq  25965  elogb  26000  logblog  26022  sqrt2cxp2logb9e3  26029  ang180lem1  26039  ang180lem2  26040  1cubrlem  26071  quartlem3  26089  asinsin  26122  acoscos  26123  asin1  26124  reasinsin  26126  acosbnd  26130  atanlogsublem  26145  atanbnd  26156  atan1  26158  log2tlbnd  26175  log2ublem1  26176  log2le1  26180  birthday  26184  basellem8  26317  basellem9  26318  cht2  26401  mumullem2  26409  chtublem  26439  chtub  26440  bposlem6  26517  bposlem7  26518  bposlem8  26519  bposlem9  26520  chebbnd1lem3  26699  chebbnd1  26700  chto1ub  26704  mulogsumlem  26759  mulog2sumlem1  26762  mulog2sumlem2  26763  mulog2sumlem3  26764  pntibndlem3  26820  ex-ceil  28944  nmblolbii  29293  ip0i  29319  ip1ilem  29320  ipasslem10  29333  siilem1  29345  siii  29347  normlem1  29604  normlem3  29606  normlem5  29608  normlem6  29609  norm-ii-i  29631  normsubi  29635  norm3adifii  29642  norm3lem  29643  normpar2i  29650  bcsiALT  29673  pjneli  30217  lnophmlem2  30511  nmbdoplbi  30518  nmcoplbi  30522  nmophmi  30525  nmbdfnlbi  30543  nmcfnlbi  30546  cnlnadjlem2  30562  cnlnadjlem7  30567  nmopadjlem  30583  nmopcoi  30589  nmopcoadji  30595  nmopcoadj0i  30597  unierri  30598  opsqrlem1  30634  dfdec100  31275  dp20u  31283  dp2ltsuc  31291  dpfrac1  31297  dpmul10  31300  decdiv10  31301  dpmul100  31302  dp3mul10  31303  dpmul1000  31304  dpexpp1  31313  dpadd2  31315  dpadd3  31317  dpmul  31318  dpmul4  31319  threehalves  31320  hgt750lemd  32764  hgt750lem  32767  hgt750lem2  32768  subfaclim  33285  subfacval3  33286  problem2  33759  problem3  33760  problem4  33761  problem5  33762  circum  33767  logi  33831  iexpire  33832  taupilem1  35569  dvacos  35939  fdc  35980  lcmineqlem23  40285  aks4d1p1p4  40305  aks4d1p1p7  40308  acos1half  40399  0cnALT3  40511  re1m1e0m0  40601  ipiiie0  40640  arearect  41268  areaquad  41269  sineq0ALT  42796  wallispilem2  43862  stirlinglem3  43872  stirlinglem4  43873  stirlinglem13  43882  stirlinglem15  43884  dirkerper  43892  fourierdlem24  43927  fourierdlem103  44005  fourierdlem104  44006  sqwvfoura  44024  sqwvfourb  44025  fourierswlem  44026  fouriersw  44027  etransclem18  44048  etransclem23  44053  etransclem46  44076  etransclem47  44077  etransclem48  44078  etransc  44079  tgoldbach  45539