Theorem recni 11326

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

This proof depends on syntax axioms:   ∈ wcel 2144  ℂcc 11201  ℝcr 11202

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-resscn 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3896

This theorem is used by:  0cnALT  11548  renegcli  11622  resubcli  11623  recgt0ii  12226  ledivp1i  12245  ltdivp1i  12246  2cnALT  12422  numltc  12848  sqge0i  14334  lt2sqi  14335  le2sqi  14336  sq11i  14337  crreczi  14375  faclbnd4lem1  14440  sqrtmsq2i  15560  abs3lemi  15583  0.999...  16055  bpoly4  16230  ef01bndlem  16357  sin4lt0  16368  eirrlem  16377  rpnnen2lem3  16389  rpnnen2lem9  16395  rpnnen2lem11  16397  dvdslelem  16484  divalglem1  16569  divalglem2  16570  divalglem5  16572  divalglem6  16573  divalglem9  16576  prmreclem6  17104  modsubi  17255  pcoass  25350  aaliou3lem7  26681  picn  26790  sinhalfpilem  26797  cosneghalfpi  26804  sinhalfpip  26826  sinhalfpim  26827  coshalfpip  26828  coshalfpim  26829  sincosq1sgn  26832  sincosq2sgn  26833  sincosq3sgn  26834  sincosq4sgn  26835  sincos4thpi  26847  tan4thpi  26848  sincos6thpi  26849  pige3ALT  26853  cosne0  26862  sinord  26867  resinf1o  26869  efif1olem2  26876  efifo  26880  logi  26920  logimul  26947  ecxp  27006  cxpsqrtlem  27035  2irrexpq  27064  elogb  27103  logblog  27125  sqrt2cxp2logb9e3  27132  ang180lem1  27142  ang180lem2  27143  1cubrlem  27174  quartlem3  27192  asinsin  27225  acoscos  27226  asin1  27227  reasinsin  27229  acosbnd  27233  atanlogsublem  27248  atanbnd  27259  atan1  27261  log2tlbnd  27278  log2ublem1  27279  log2le1  27283  birthday  27287  basellem8  27420  basellem9  27421  cht2  27504  mumullem2  27512  chtublem  27543  chtub  27544  bposlem6  27621  bposlem7  27622  bposlem8  27623  bposlem9  27624  chebbnd1lem3  27803  chebbnd1  27804  chto1ub  27808  mulogsumlem  27863  mulog2sumlem1  27866  mulog2sumlem2  27867  mulog2sumlem3  27868  pntibndlem3  27924  ex-ceil  31054  nmblolbii  31406  ip0i  31432  ip1ilem  31433  ipasslem10  31446  siilem1  31458  siii  31460  normlem1  31717  normlem3  31719  normlem5  31721  normlem6  31722  norm-ii-i  31744  normsubi  31748  norm3adifii  31755  norm3lem  31756  normpar2i  31763  bcsiALT  31786  pjneli  32330  lnophmlem2  32624  nmbdoplbi  32631  nmcoplbi  32635  nmophmi  32638  nmbdfnlbi  32656  nmcfnlbi  32659  cnlnadjlem2  32675  cnlnadjlem7  32680  nmopadjlem  32696  nmopcoi  32702  nmopcoadji  32708  nmopcoadj0i  32710  unierri  32711  opsqrlem1  32747  dfdec100  33467  dp20u  33490  dp2ltsuc  33498  dpfrac1  33504  dpmul10  33507  decdiv10  33508  dpmul100  33509  dp3mul10  33510  dpmul1000  33511  dpexpp1  33520  dpadd2  33522  dpadd3  33524  dpmul  33525  dpmul4  33526  threehalves  33527  hgt750lemd  35323  hgt750lem  35326  hgt750lem2  35327  subfaclim  36039  subfacval3  36040  problem2  36517  problem3  36518  problem4  36519  problem5  36520  circum  36525  iexpire  36592  taupilem1  38335  dvacos  38716  fdc  38772  lcmineqlem23  43194  aks4d1p1p4  43214  aks4d1p1p7  43217  0cnALT3  43397  acos1half  43502  re1m1e0m0  43541  ipiiie0  43582  arearect  44310  areaquad  44311  sineq0ALT  46012  wallispilem2  47169  stirlinglem3  47179  stirlinglem4  47180  stirlinglem13  47189  stirlinglem15  47191  dirkerper  47199  fourierdlem24  47234  fourierdlem103  47312  fourierdlem104  47313  sqwvfoura  47331  sqwvfourb  47332  fourierswlem  47333  fouriersw  47334  etransclem18  47355  etransclem23  47360  etransclem46  47383  etransclem47  47384  etransclem48  47385  etransc  47386  goldrasin  48022  goldratmolem2  48026  goldratmolem3  48027  goldratmolem4  48028  goldratval  48029  tgoldbach  49008