Theorem recni 10812

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

Syntax hints:   ∈ wcel 2112  ℂcc 10692  ℝcr 10693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-resscn 10751

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  0cnALT  11031  renegcli  11104  resubcli  11105  recgt0ii  11703  ledivp1i  11722  ltdivp1i  11723  2cnALT  11871  8th4div3  12015  numltc  12284  sqge0i  13722  lt2sqi  13723  le2sqi  13724  sq11i  13725  crreczi  13760  faclbnd4lem1  13824  sqrtmsq2i  14916  abs3lemi  14939  0.999...  15408  bpoly4  15584  ef01bndlem  15708  sin4lt0  15719  eirrlem  15728  rpnnen2lem3  15740  rpnnen2lem9  15746  rpnnen2lem11  15748  dvdslelem  15833  divalglem1  15918  divalglem2  15919  divalglem5  15921  divalglem6  15922  divalglem9  15925  prmreclem6  16437  modsubi  16588  pcoass  23875  aaliou3lem7  25196  picn  25303  sinhalfpilem  25307  cosneghalfpi  25314  sinhalfpip  25336  sinhalfpim  25337  coshalfpip  25338  coshalfpim  25339  sincosq1sgn  25342  sincosq2sgn  25343  sincosq3sgn  25344  sincosq4sgn  25345  sincos4thpi  25357  tan4thpi  25358  sincos6thpi  25359  pige3ALT  25363  cosne0  25372  sinord  25377  resinf1o  25379  efif1olem2  25386  efif1olem4  25388  efifo  25390  logimul  25456  ecxp  25515  cxpsqrtlem  25544  2irrexpq  25572  elogb  25607  logblog  25629  sqrt2cxp2logb9e3  25636  ang180lem1  25646  ang180lem2  25647  1cubrlem  25678  quartlem3  25696  asinsin  25729  acoscos  25730  asin1  25731  reasinsin  25733  acosbnd  25737  atanlogsublem  25752  atanbnd  25763  atan1  25765  log2tlbnd  25782  log2ublem1  25783  log2le1  25787  birthday  25791  basellem8  25924  basellem9  25925  cht2  26008  mumullem2  26016  chtublem  26046  chtub  26047  bposlem6  26124  bposlem7  26125  bposlem8  26126  bposlem9  26127  chebbnd1lem3  26306  chebbnd1  26307  chto1ub  26311  mulogsumlem  26366  mulog2sumlem1  26369  mulog2sumlem2  26370  mulog2sumlem3  26371  pntibndlem3  26427  ex-ceil  28485  nmblolbii  28834  ip0i  28860  ip1ilem  28861  ipasslem10  28874  siilem1  28886  siii  28888  normlem1  29145  normlem3  29147  normlem5  29149  normlem6  29150  norm-ii-i  29172  normsubi  29176  norm3adifii  29183  norm3lem  29184  normpar2i  29191  bcsiALT  29214  pjneli  29758  lnophmlem2  30052  nmbdoplbi  30059  nmcoplbi  30063  nmophmi  30066  nmbdfnlbi  30084  nmcfnlbi  30087  cnlnadjlem2  30103  cnlnadjlem7  30108  nmopadjlem  30124  nmopcoi  30130  nmopcoadji  30136  nmopcoadj0i  30138  unierri  30139  opsqrlem1  30175  dfdec100  30818  dp20u  30826  dp2ltsuc  30834  dpfrac1  30840  dpmul10  30843  decdiv10  30844  dpmul100  30845  dp3mul10  30846  dpmul1000  30847  dpexpp1  30856  dpadd2  30858  dpadd3  30860  dpmul  30861  dpmul4  30862  threehalves  30863  hgt750lemd  32294  hgt750lem  32297  hgt750lem2  32298  subfaclim  32817  subfacval3  32818  problem2  33291  problem3  33292  problem4  33293  problem5  33294  circum  33299  logi  33369  iexpire  33370  taupilem1  35175  dvacos  35548  fdc  35589  lcmineqlem23  39742  aks4d1p1p4  39761  aks4d1p1p7  39764  acos1half  39833  0cnALT3  39938  re1m1e0m0  40029  ipiiie0  40068  arearect  40690  areaquad  40691  sineq0ALT  42171  wallispilem2  43225  stirlinglem3  43235  stirlinglem4  43236  stirlinglem13  43245  stirlinglem15  43247  dirkerper  43255  fourierdlem24  43290  fourierdlem103  43368  fourierdlem104  43369  sqwvfoura  43387  sqwvfourb  43388  fourierswlem  43389  fouriersw  43390  etransclem18  43411  etransclem23  43416  etransclem46  43439  etransclem47  43440  etransclem48  43441  etransc  43442  tgoldbach  44885