Theorem recni 11224

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

Syntax hints:   ∈ wcel 2143  ℂcc 11099  ℝcr 11100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-resscn 11158

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3923

This theorem is referenced by:  0cnALT  11446  renegcli  11520  resubcli  11521  recgt0ii  12122  ledivp1i  12141  ltdivp1i  12142  2cnALT  12318  numltc  12743  sqge0i  14226  lt2sqi  14227  le2sqi  14228  sq11i  14229  crreczi  14266  faclbnd4lem1  14331  sqrtmsq2i  15441  abs3lemi  15464  0.999...  15937  bpoly4  16114  ef01bndlem  16241  sin4lt0  16252  eirrlem  16261  rpnnen2lem3  16273  rpnnen2lem9  16279  rpnnen2lem11  16281  dvdslelem  16368  divalglem1  16453  divalglem2  16454  divalglem5  16456  divalglem6  16457  divalglem9  16460  prmreclem6  16982  modsubi  17133  pcoass  25164  aaliou3lem7  26491  picn  26599  sinhalfpilem  26606  cosneghalfpi  26613  sinhalfpip  26635  sinhalfpim  26636  coshalfpip  26637  coshalfpim  26638  sincosq1sgn  26641  sincosq2sgn  26642  sincosq3sgn  26643  sincosq4sgn  26644  sincos4thpi  26656  tan4thpi  26657  tan4thpiOLD  26658  sincos6thpi  26659  pige3ALT  26663  cosne0  26672  sinord  26677  resinf1o  26679  efif1olem2  26686  efif1olem4  26688  efifo  26690  logi  26730  logimul  26757  ecxp  26816  cxpsqrtlem  26845  2irrexpq  26874  elogb  26913  logblog  26935  sqrt2cxp2logb9e3  26942  ang180lem1  26952  ang180lem2  26953  1cubrlem  26984  quartlem3  27002  asinsin  27035  acoscos  27036  asin1  27037  reasinsin  27039  acosbnd  27043  atanlogsublem  27058  atanbnd  27069  atan1  27071  log2tlbnd  27088  log2ublem1  27089  log2le1  27093  birthday  27097  basellem8  27230  basellem9  27231  cht2  27314  mumullem2  27322  chtublem  27353  chtub  27354  bposlem6  27431  bposlem7  27432  bposlem8  27433  bposlem9  27434  chebbnd1lem3  27613  chebbnd1  27614  chto1ub  27618  mulogsumlem  27673  mulog2sumlem1  27676  mulog2sumlem2  27677  mulog2sumlem3  27678  pntibndlem3  27734  ex-ceil  30777  nmblolbii  31129  ip0i  31155  ip1ilem  31156  ipasslem10  31169  siilem1  31181  siii  31183  normlem1  31440  normlem3  31442  normlem5  31444  normlem6  31445  norm-ii-i  31467  normsubi  31471  norm3adifii  31478  norm3lem  31479  normpar2i  31486  bcsiALT  31509  pjneli  32053  lnophmlem2  32347  nmbdoplbi  32354  nmcoplbi  32358  nmophmi  32361  nmbdfnlbi  32379  nmcfnlbi  32382  cnlnadjlem2  32398  cnlnadjlem7  32403  nmopadjlem  32419  nmopcoi  32425  nmopcoadji  32431  nmopcoadj0i  32433  unierri  32434  opsqrlem1  32470  dfdec100  33152  dp20u  33175  dp2ltsuc  33183  dpfrac1  33189  dpmul10  33192  decdiv10  33193  dpmul100  33194  dp3mul10  33195  dpmul1000  33196  dpexpp1  33205  dpadd2  33207  dpadd3  33209  dpmul  33210  dpmul4  33211  threehalves  33212  hgt750lemd  35013  hgt750lem  35016  hgt750lem2  35017  subfaclim  35658  subfacval3  35659  problem2  36136  problem3  36137  problem4  36138  problem5  36139  circum  36144  iexpire  36205  taupilem1  37943  dvacos  38334  fdc  38374  lcmineqlem23  42796  aks4d1p1p4  42816  aks4d1p1p7  42819  0cnALT3  42999  acos1half  43097  re1m1e0m0  43136  ipiiie0  43177  arearect  43922  areaquad  43923  sineq0ALT  45625  wallispilem2  46760  stirlinglem3  46770  stirlinglem4  46771  stirlinglem13  46780  stirlinglem15  46782  dirkerper  46790  fourierdlem24  46825  fourierdlem103  46903  fourierdlem104  46904  sqwvfoura  46922  sqwvfourb  46923  fourierswlem  46924  fouriersw  46925  etransclem18  46946  etransclem23  46951  etransclem46  46974  etransclem47  46975  etransclem48  46976  etransc  46977  goldrasin  47596  goldratmolem2  47600  tgoldbach  48559