Theorem recni 10973

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

Syntax hints:   ∈ wcel 2109  ℂcc 10853  ℝcr 10854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-resscn 10912

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  0cnALT  11192  renegcli  11265  resubcli  11266  recgt0ii  11864  ledivp1i  11883  ltdivp1i  11884  2cnALT  12032  8th4div3  12176  numltc  12445  sqge0i  13886  lt2sqi  13887  le2sqi  13888  sq11i  13889  crreczi  13924  faclbnd4lem1  13988  sqrtmsq2i  15080  abs3lemi  15103  0.999...  15574  bpoly4  15750  ef01bndlem  15874  sin4lt0  15885  eirrlem  15894  rpnnen2lem3  15906  rpnnen2lem9  15912  rpnnen2lem11  15914  dvdslelem  15999  divalglem1  16084  divalglem2  16085  divalglem5  16087  divalglem6  16088  divalglem9  16091  prmreclem6  16603  modsubi  16754  pcoass  24168  aaliou3lem7  25490  picn  25597  sinhalfpilem  25601  cosneghalfpi  25608  sinhalfpip  25630  sinhalfpim  25631  coshalfpip  25632  coshalfpim  25633  sincosq1sgn  25636  sincosq2sgn  25637  sincosq3sgn  25638  sincosq4sgn  25639  sincos4thpi  25651  tan4thpi  25652  sincos6thpi  25653  pige3ALT  25657  cosne0  25666  sinord  25671  resinf1o  25673  efif1olem2  25680  efif1olem4  25682  efifo  25684  logimul  25750  ecxp  25809  cxpsqrtlem  25838  2irrexpq  25866  elogb  25901  logblog  25923  sqrt2cxp2logb9e3  25930  ang180lem1  25940  ang180lem2  25941  1cubrlem  25972  quartlem3  25990  asinsin  26023  acoscos  26024  asin1  26025  reasinsin  26027  acosbnd  26031  atanlogsublem  26046  atanbnd  26057  atan1  26059  log2tlbnd  26076  log2ublem1  26077  log2le1  26081  birthday  26085  basellem8  26218  basellem9  26219  cht2  26302  mumullem2  26310  chtublem  26340  chtub  26341  bposlem6  26418  bposlem7  26419  bposlem8  26420  bposlem9  26421  chebbnd1lem3  26600  chebbnd1  26601  chto1ub  26605  mulogsumlem  26660  mulog2sumlem1  26663  mulog2sumlem2  26664  mulog2sumlem3  26665  pntibndlem3  26721  ex-ceil  28791  nmblolbii  29140  ip0i  29166  ip1ilem  29167  ipasslem10  29180  siilem1  29192  siii  29194  normlem1  29451  normlem3  29453  normlem5  29455  normlem6  29456  norm-ii-i  29478  normsubi  29482  norm3adifii  29489  norm3lem  29490  normpar2i  29497  bcsiALT  29520  pjneli  30064  lnophmlem2  30358  nmbdoplbi  30365  nmcoplbi  30369  nmophmi  30372  nmbdfnlbi  30390  nmcfnlbi  30393  cnlnadjlem2  30409  cnlnadjlem7  30414  nmopadjlem  30430  nmopcoi  30436  nmopcoadji  30442  nmopcoadj0i  30444  unierri  30445  opsqrlem1  30481  dfdec100  31123  dp20u  31131  dp2ltsuc  31139  dpfrac1  31145  dpmul10  31148  decdiv10  31149  dpmul100  31150  dp3mul10  31151  dpmul1000  31152  dpexpp1  31161  dpadd2  31163  dpadd3  31165  dpmul  31166  dpmul4  31167  threehalves  31168  hgt750lemd  32607  hgt750lem  32610  hgt750lem2  32611  subfaclim  33129  subfacval3  33130  problem2  33603  problem3  33604  problem4  33605  problem5  33606  circum  33611  logi  33679  iexpire  33680  taupilem1  35471  dvacos  35841  fdc  35882  lcmineqlem23  40039  aks4d1p1p4  40059  aks4d1p1p7  40062  acos1half  40150  0cnALT3  40270  re1m1e0m0  40360  ipiiie0  40399  arearect  41026  areaquad  41027  sineq0ALT  42510  wallispilem2  43561  stirlinglem3  43571  stirlinglem4  43572  stirlinglem13  43581  stirlinglem15  43583  dirkerper  43591  fourierdlem24  43626  fourierdlem103  43704  fourierdlem104  43705  sqwvfoura  43723  sqwvfourb  43724  fourierswlem  43725  fouriersw  43726  etransclem18  43747  etransclem23  43752  etransclem46  43775  etransclem47  43776  etransclem48  43777  etransc  43778  tgoldbach  45221