Theorem recni 11158

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

Syntax hints:   ∈ wcel 2114  ℂcc 11036  ℝcr 11037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3920

This theorem is referenced by:  0cnALT  11380  renegcli  11454  resubcli  11455  recgt0ii  12060  ledivp1i  12079  ltdivp1i  12080  2cnALT  12233  8th4div3  12373  numltc  12645  sqge0i  14123  lt2sqi  14124  le2sqi  14125  sq11i  14126  crreczi  14163  faclbnd4lem1  14228  sqrtmsq2i  15323  abs3lemi  15346  0.999...  15816  bpoly4  15994  ef01bndlem  16121  sin4lt0  16132  eirrlem  16141  rpnnen2lem3  16153  rpnnen2lem9  16159  rpnnen2lem11  16161  dvdslelem  16248  divalglem1  16333  divalglem2  16334  divalglem5  16336  divalglem6  16337  divalglem9  16340  prmreclem6  16861  modsubi  17012  pcoass  24992  aaliou3lem7  26325  picn  26435  sinhalfpilem  26440  cosneghalfpi  26447  sinhalfpip  26469  sinhalfpim  26470  coshalfpip  26471  coshalfpim  26472  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  sincos4thpi  26490  tan4thpi  26491  tan4thpiOLD  26492  sincos6thpi  26493  pige3ALT  26497  cosne0  26506  sinord  26511  resinf1o  26513  efif1olem2  26520  efif1olem4  26522  efifo  26524  logi  26564  logimul  26591  ecxp  26650  cxpsqrtlem  26679  2irrexpq  26708  elogb  26748  logblog  26770  sqrt2cxp2logb9e3  26777  ang180lem1  26787  ang180lem2  26788  1cubrlem  26819  quartlem3  26837  asinsin  26870  acoscos  26871  asin1  26872  reasinsin  26874  acosbnd  26878  atanlogsublem  26893  atanbnd  26904  atan1  26906  log2tlbnd  26923  log2ublem1  26924  log2le1  26928  birthday  26932  basellem8  27066  basellem9  27067  cht2  27150  mumullem2  27158  chtublem  27190  chtub  27191  bposlem6  27268  bposlem7  27269  bposlem8  27270  bposlem9  27271  chebbnd1lem3  27450  chebbnd1  27451  chto1ub  27455  mulogsumlem  27510  mulog2sumlem1  27513  mulog2sumlem2  27514  mulog2sumlem3  27515  pntibndlem3  27571  ex-ceil  30535  nmblolbii  30886  ip0i  30912  ip1ilem  30913  ipasslem10  30926  siilem1  30938  siii  30940  normlem1  31197  normlem3  31199  normlem5  31201  normlem6  31202  norm-ii-i  31224  normsubi  31228  norm3adifii  31235  norm3lem  31236  normpar2i  31243  bcsiALT  31266  pjneli  31810  lnophmlem2  32104  nmbdoplbi  32111  nmcoplbi  32115  nmophmi  32118  nmbdfnlbi  32136  nmcfnlbi  32139  cnlnadjlem2  32155  cnlnadjlem7  32160  nmopadjlem  32176  nmopcoi  32182  nmopcoadji  32188  nmopcoadj0i  32190  unierri  32191  opsqrlem1  32227  dfdec100  32921  dp20u  32969  dp2ltsuc  32977  dpfrac1  32983  dpmul10  32986  decdiv10  32987  dpmul100  32988  dp3mul10  32989  dpmul1000  32990  dpexpp1  32999  dpadd2  33001  dpadd3  33003  dpmul  33004  dpmul4  33005  threehalves  33006  hgt750lemd  34825  hgt750lem  34828  hgt750lem2  34829  subfaclim  35401  subfacval3  35402  problem2  35879  problem3  35880  problem4  35881  problem5  35882  circum  35887  iexpire  35948  taupilem1  37570  dvacos  37950  fdc  37990  lcmineqlem23  42415  aks4d1p1p4  42435  aks4d1p1p7  42438  0cnALT3  42617  acos1half  42722  re1m1e0m0  42761  ipiiie0  42802  arearect  43566  areaquad  43567  sineq0ALT  45286  wallispilem2  46418  stirlinglem3  46428  stirlinglem4  46429  stirlinglem13  46438  stirlinglem15  46440  dirkerper  46448  fourierdlem24  46483  fourierdlem103  46561  fourierdlem104  46562  sqwvfoura  46580  sqwvfourb  46581  fourierswlem  46582  fouriersw  46583  etransclem18  46604  etransclem23  46609  etransclem46  46632  etransclem47  46633  etransclem48  46634  etransc  46635  tgoldbach  48171