Theorem recni 10655

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

Syntax hints:   ∈ wcel 2114  ℂcc 10535  ℝcr 10536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-resscn 10594

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  0cnALT  10874  renegcli  10947  resubcli  10948  recgt0ii  11546  ledivp1i  11565  ltdivp1i  11566  2cnALT  11714  8th4div3  11858  numltc  12125  sqge0i  13552  lt2sqi  13553  le2sqi  13554  sq11i  13555  crreczi  13590  faclbnd4lem1  13654  sqrtmsq2i  14747  abs3lemi  14770  0.999...  15237  bpoly4  15413  ef01bndlem  15537  sin4lt0  15548  eirrlem  15557  rpnnen2lem3  15569  rpnnen2lem9  15575  rpnnen2lem11  15577  dvdslelem  15659  divalglem1  15745  divalglem2  15746  divalglem5  15748  divalglem6  15749  divalglem9  15752  prmreclem6  16257  modsubi  16408  pcoass  23628  aaliou3lem7  24938  picn  25045  sinhalfpilem  25049  cosneghalfpi  25056  sinhalfpip  25078  sinhalfpim  25079  coshalfpip  25080  coshalfpim  25081  sincosq1sgn  25084  sincosq2sgn  25085  sincosq3sgn  25086  sincosq4sgn  25087  sincos4thpi  25099  tan4thpi  25100  sincos6thpi  25101  pige3ALT  25105  cosne0  25114  sinord  25118  resinf1o  25120  efif1olem2  25127  efif1olem4  25129  efifo  25131  logimul  25197  ecxp  25256  cxpsqrtlem  25285  2irrexpq  25313  elogb  25348  logblog  25370  sqrt2cxp2logb9e3  25377  ang180lem1  25387  ang180lem2  25388  1cubrlem  25419  quartlem3  25437  asinsin  25470  acoscos  25471  asin1  25472  reasinsin  25474  acosbnd  25478  atanlogsublem  25493  atanbnd  25504  atan1  25506  log2tlbnd  25523  log2ublem1  25524  log2le1  25528  birthday  25532  basellem8  25665  basellem9  25666  cht2  25749  mumullem2  25757  chtublem  25787  chtub  25788  bposlem6  25865  bposlem7  25866  bposlem8  25867  bposlem9  25868  chebbnd1lem3  26047  chebbnd1  26048  chto1ub  26052  mulogsumlem  26107  mulog2sumlem1  26110  mulog2sumlem2  26111  mulog2sumlem3  26112  pntibndlem3  26168  ex-ceil  28227  nmblolbii  28576  ip0i  28602  ip1ilem  28603  ipasslem10  28616  siilem1  28628  siii  28630  normlem1  28887  normlem3  28889  normlem5  28891  normlem6  28892  norm-ii-i  28914  normsubi  28918  norm3adifii  28925  norm3lem  28926  normpar2i  28933  bcsiALT  28956  pjneli  29500  lnophmlem2  29794  nmbdoplbi  29801  nmcoplbi  29805  nmophmi  29808  nmbdfnlbi  29826  nmcfnlbi  29829  cnlnadjlem2  29845  cnlnadjlem7  29850  nmopadjlem  29866  nmopcoi  29872  nmopcoadji  29878  nmopcoadj0i  29880  unierri  29881  opsqrlem1  29917  dfdec100  30546  dp20u  30554  dp2ltsuc  30562  dpfrac1  30568  dpmul10  30571  decdiv10  30572  dpmul100  30573  dp3mul10  30574  dpmul1000  30575  dpexpp1  30584  dpadd2  30586  dpadd3  30588  dpmul  30589  dpmul4  30590  threehalves  30591  hgt750lemd  31919  hgt750lem  31922  hgt750lem2  31923  subfaclim  32435  subfacval3  32436  problem2  32909  problem3  32910  problem4  32911  problem5  32912  circum  32917  logi  32966  iexpire  32967  taupilem1  34605  dvacos  34994  fdc  35035  0cnALT3  39202  re1m1e0m0  39276  arearect  39871  areaquad  39872  sineq0ALT  41320  wallispilem2  42400  stirlinglem3  42410  stirlinglem4  42411  stirlinglem13  42420  stirlinglem15  42422  dirkerper  42430  fourierdlem24  42465  fourierdlem103  42543  fourierdlem104  42544  sqwvfoura  42562  sqwvfourb  42563  fourierswlem  42564  fouriersw  42565  etransclem18  42586  etransclem23  42591  etransclem46  42614  etransclem47  42615  etransclem48  42616  etransc  42617  tgoldbach  44031