Theorem recni 11193

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

Syntax hints:   ∈ wcel 2141  ℂcc 11068  ℝcr 11069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-resscn 11127

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-ss 3921

This theorem is referenced by:  0cnALT  11415  renegcli  11489  resubcli  11490  recgt0ii  12095  ledivp1i  12114  ltdivp1i  12115  2cnALT  12291  8th4div3  12438  numltc  12716  sqge0i  14198  lt2sqi  14199  le2sqi  14200  sq11i  14201  crreczi  14238  faclbnd4lem1  14303  sqrtmsq2i  15398  abs3lemi  15421  0.999...  15894  bpoly4  16072  ef01bndlem  16199  sin4lt0  16210  eirrlem  16219  rpnnen2lem3  16231  rpnnen2lem9  16237  rpnnen2lem11  16239  dvdslelem  16326  divalglem1  16411  divalglem2  16412  divalglem5  16414  divalglem6  16415  divalglem9  16418  prmreclem6  16940  modsubi  17091  pcoass  25066  aaliou3lem7  26390  picn  26498  sinhalfpilem  26505  cosneghalfpi  26512  sinhalfpip  26534  sinhalfpim  26535  coshalfpip  26536  coshalfpim  26537  sincosq1sgn  26540  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  sincos4thpi  26555  tan4thpi  26556  tan4thpiOLD  26557  sincos6thpi  26558  pige3ALT  26562  cosne0  26571  sinord  26576  resinf1o  26578  efif1olem2  26585  efif1olem4  26587  efifo  26589  logi  26629  logimul  26656  ecxp  26715  cxpsqrtlem  26744  2irrexpq  26773  elogb  26812  logblog  26834  sqrt2cxp2logb9e3  26841  ang180lem1  26851  ang180lem2  26852  1cubrlem  26883  quartlem3  26901  asinsin  26934  acoscos  26935  asin1  26936  reasinsin  26938  acosbnd  26942  atanlogsublem  26957  atanbnd  26968  atan1  26970  log2tlbnd  26987  log2ublem1  26988  log2le1  26992  birthday  26996  basellem8  27129  basellem9  27130  cht2  27213  mumullem2  27221  chtublem  27252  chtub  27253  bposlem6  27330  bposlem7  27331  bposlem8  27332  bposlem9  27333  chebbnd1lem3  27512  chebbnd1  27513  chto1ub  27517  mulogsumlem  27572  mulog2sumlem1  27575  mulog2sumlem2  27576  mulog2sumlem3  27577  pntibndlem3  27633  ex-ceil  30596  nmblolbii  30948  ip0i  30974  ip1ilem  30975  ipasslem10  30988  siilem1  31000  siii  31002  normlem1  31259  normlem3  31261  normlem5  31263  normlem6  31264  norm-ii-i  31286  normsubi  31290  norm3adifii  31297  norm3lem  31298  normpar2i  31305  bcsiALT  31328  pjneli  31872  lnophmlem2  32166  nmbdoplbi  32173  nmcoplbi  32177  nmophmi  32180  nmbdfnlbi  32198  nmcfnlbi  32201  cnlnadjlem2  32217  cnlnadjlem7  32222  nmopadjlem  32238  nmopcoi  32244  nmopcoadji  32250  nmopcoadj0i  32252  unierri  32253  opsqrlem1  32289  dfdec100  32982  dp20u  33016  dp2ltsuc  33024  dpfrac1  33030  dpmul10  33033  decdiv10  33034  dpmul100  33035  dp3mul10  33036  dpmul1000  33037  dpexpp1  33046  dpadd2  33048  dpadd3  33050  dpmul  33051  dpmul4  33052  threehalves  33053  hgt750lemd  34906  hgt750lem  34909  hgt750lem2  34910  subfaclim  35502  subfacval3  35503  problem2  35980  problem3  35981  problem4  35982  problem5  35983  circum  35988  iexpire  36049  taupilem1  37777  dvacos  38168  fdc  38208  lcmineqlem23  42632  aks4d1p1p4  42652  aks4d1p1p7  42655  0cnALT3  42833  acos1half  42931  re1m1e0m0  42970  ipiiie0  43011  arearect  43756  areaquad  43757  sineq0ALT  45476  wallispilem2  46604  stirlinglem3  46614  stirlinglem4  46615  stirlinglem13  46624  stirlinglem15  46626  dirkerper  46634  fourierdlem24  46669  fourierdlem103  46747  fourierdlem104  46748  sqwvfoura  46766  sqwvfourb  46767  fourierswlem  46768  fouriersw  46769  etransclem18  46790  etransclem23  46795  etransclem46  46818  etransclem47  46819  etransclem48  46820  etransc  46821  goldrasin  47440  goldratmolem2  47444  tgoldbach  48403