Theorem recni 11304

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

This proof depends on syntax axioms:   ∈ wcel 2145  ℂcc 11179  ℝcr 11180

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-resscn 11238

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836  df-ss 3916

This theorem is used by:  0cnALT  11526  renegcli  11600  resubcli  11601  recgt0ii  12204  ledivp1i  12223  ltdivp1i  12224  2cnALT  12400  numltc  12826  sqge0i  14311  lt2sqi  14312  le2sqi  14313  sq11i  14314  crreczi  14352  faclbnd4lem1  14417  sqrtmsq2i  15535  abs3lemi  15558  0.999...  16030  bpoly4  16205  ef01bndlem  16332  sin4lt0  16343  eirrlem  16352  rpnnen2lem3  16364  rpnnen2lem9  16370  rpnnen2lem11  16372  dvdslelem  16459  divalglem1  16544  divalglem2  16545  divalglem5  16547  divalglem6  16548  divalglem9  16551  prmreclem6  17079  modsubi  17230  pcoass  25325  aaliou3lem7  26658  picn  26767  sinhalfpilem  26774  cosneghalfpi  26781  sinhalfpip  26803  sinhalfpim  26804  coshalfpip  26805  coshalfpim  26806  sincosq1sgn  26809  sincosq2sgn  26810  sincosq3sgn  26811  sincosq4sgn  26812  sincos4thpi  26824  tan4thpi  26825  sincos6thpi  26826  pige3ALT  26830  cosne0  26839  sinord  26844  resinf1o  26846  efif1olem2  26853  efifo  26857  logi  26897  logimul  26924  ecxp  26983  cxpsqrtlem  27012  2irrexpq  27041  elogb  27080  logblog  27102  sqrt2cxp2logb9e3  27109  ang180lem1  27119  ang180lem2  27120  1cubrlem  27151  quartlem3  27169  asinsin  27202  acoscos  27203  asin1  27204  reasinsin  27206  acosbnd  27210  atanlogsublem  27225  atanbnd  27236  atan1  27238  log2tlbnd  27255  log2ublem1  27256  log2le1  27260  birthday  27264  basellem8  27397  basellem9  27398  cht2  27481  mumullem2  27489  chtublem  27520  chtub  27521  bposlem6  27598  bposlem7  27599  bposlem8  27600  bposlem9  27601  chebbnd1lem3  27780  chebbnd1  27781  chto1ub  27785  mulogsumlem  27840  mulog2sumlem1  27843  mulog2sumlem2  27844  mulog2sumlem3  27845  pntibndlem3  27901  ex-ceil  31031  nmblolbii  31383  ip0i  31409  ip1ilem  31410  ipasslem10  31423  siilem1  31435  siii  31437  normlem1  31694  normlem3  31696  normlem5  31698  normlem6  31699  norm-ii-i  31721  normsubi  31725  norm3adifii  31732  norm3lem  31733  normpar2i  31740  bcsiALT  31763  pjneli  32307  lnophmlem2  32601  nmbdoplbi  32608  nmcoplbi  32612  nmophmi  32615  nmbdfnlbi  32633  nmcfnlbi  32636  cnlnadjlem2  32652  cnlnadjlem7  32657  nmopadjlem  32673  nmopcoi  32679  nmopcoadji  32685  nmopcoadj0i  32687  unierri  32688  opsqrlem1  32724  dfdec100  33403  dp20u  33426  dp2ltsuc  33434  dpfrac1  33440  dpmul10  33443  decdiv10  33444  dpmul100  33445  dp3mul10  33446  dpmul1000  33447  dpexpp1  33456  dpadd2  33458  dpadd3  33460  dpmul  33461  dpmul4  33462  threehalves  33463  hgt750lemd  35260  hgt750lem  35263  hgt750lem2  35264  subfaclim  35922  subfacval3  35923  problem2  36400  problem3  36401  problem4  36402  problem5  36403  circum  36408  iexpire  36469  taupilem1  38210  dvacos  38591  fdc  38647  lcmineqlem23  43069  aks4d1p1p4  43089  aks4d1p1p7  43092  0cnALT3  43272  acos1half  43377  re1m1e0m0  43416  ipiiie0  43457  arearect  44175  areaquad  44176  sineq0ALT  45878  wallispilem2  47020  stirlinglem3  47030  stirlinglem4  47031  stirlinglem13  47040  stirlinglem15  47042  dirkerper  47050  fourierdlem24  47085  fourierdlem103  47163  fourierdlem104  47164  sqwvfoura  47182  sqwvfourb  47183  fourierswlem  47184  fouriersw  47185  etransclem18  47206  etransclem23  47211  etransclem46  47234  etransclem47  47235  etransclem48  47236  etransc  47237  goldrasin  47873  goldratmolem2  47877  goldratmolem3  47878  goldratmolem4  47879  goldratval  47880  tgoldbach  48859