Theorem recni 11241

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

This proof depends on syntax axioms:   ∈ wcel 2146  ℂcc 11116  ℝcr 11117

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 2148  ax-resscn 11175

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

This theorem is used by:  0cnALT  11463  renegcli  11537  resubcli  11538  recgt0ii  12139  ledivp1i  12158  ltdivp1i  12159  2cnALT  12335  numltc  12760  sqge0i  14244  lt2sqi  14245  le2sqi  14246  sq11i  14247  crreczi  14284  faclbnd4lem1  14349  sqrtmsq2i  15465  abs3lemi  15488  0.999...  15961  bpoly4  16138  ef01bndlem  16265  sin4lt0  16276  eirrlem  16285  rpnnen2lem3  16297  rpnnen2lem9  16303  rpnnen2lem11  16305  dvdslelem  16392  divalglem1  16477  divalglem2  16478  divalglem5  16480  divalglem6  16481  divalglem9  16484  prmreclem6  17006  modsubi  17157  pcoass  25220  aaliou3lem7  26549  picn  26658  sinhalfpilem  26665  cosneghalfpi  26672  sinhalfpip  26694  sinhalfpim  26695  coshalfpip  26696  coshalfpim  26697  sincosq1sgn  26700  sincosq2sgn  26701  sincosq3sgn  26702  sincosq4sgn  26703  sincos4thpi  26715  tan4thpi  26716  tan4thpiOLD  26717  sincos6thpi  26718  pige3ALT  26722  cosne0  26731  sinord  26736  resinf1o  26738  efif1olem2  26745  efif1olem4  26747  efifo  26749  logi  26789  logimul  26816  ecxp  26875  cxpsqrtlem  26904  2irrexpq  26933  elogb  26972  logblog  26994  sqrt2cxp2logb9e3  27001  ang180lem1  27011  ang180lem2  27012  1cubrlem  27043  quartlem3  27061  asinsin  27094  acoscos  27095  asin1  27096  reasinsin  27098  acosbnd  27102  atanlogsublem  27117  atanbnd  27128  atan1  27130  log2tlbnd  27147  log2ublem1  27148  log2le1  27152  birthday  27156  basellem8  27289  basellem9  27290  cht2  27373  mumullem2  27381  chtublem  27412  chtub  27413  bposlem6  27490  bposlem7  27491  bposlem8  27492  bposlem9  27493  chebbnd1lem3  27672  chebbnd1  27673  chto1ub  27677  mulogsumlem  27732  mulog2sumlem1  27735  mulog2sumlem2  27736  mulog2sumlem3  27737  pntibndlem3  27793  ex-ceil  30836  nmblolbii  31188  ip0i  31214  ip1ilem  31215  ipasslem10  31228  siilem1  31240  siii  31242  normlem1  31499  normlem3  31501  normlem5  31503  normlem6  31504  norm-ii-i  31526  normsubi  31530  norm3adifii  31537  norm3lem  31538  normpar2i  31545  bcsiALT  31568  pjneli  32112  lnophmlem2  32406  nmbdoplbi  32413  nmcoplbi  32417  nmophmi  32420  nmbdfnlbi  32438  nmcfnlbi  32441  cnlnadjlem2  32457  cnlnadjlem7  32462  nmopadjlem  32478  nmopcoi  32484  nmopcoadji  32490  nmopcoadj0i  32492  unierri  32493  opsqrlem1  32529  dfdec100  33211  dp20u  33234  dp2ltsuc  33242  dpfrac1  33248  dpmul10  33251  decdiv10  33252  dpmul100  33253  dp3mul10  33254  dpmul1000  33255  dpexpp1  33264  dpadd2  33266  dpadd3  33268  dpmul  33269  dpmul4  33270  threehalves  33271  hgt750lemd  35067  hgt750lem  35070  hgt750lem2  35071  subfaclim  35701  subfacval3  35702  problem2  36179  problem3  36180  problem4  36181  problem5  36182  circum  36187  iexpire  36248  taupilem1  38006  dvacos  38397  fdc  38437  lcmineqlem23  42859  aks4d1p1p4  42879  aks4d1p1p7  42882  0cnALT3  43062  acos1half  43160  re1m1e0m0  43199  ipiiie0  43240  arearect  43983  areaquad  43984  sineq0ALT  45686  wallispilem2  46821  stirlinglem3  46831  stirlinglem4  46832  stirlinglem13  46841  stirlinglem15  46843  dirkerper  46851  fourierdlem24  46886  fourierdlem103  46964  fourierdlem104  46965  sqwvfoura  46983  sqwvfourb  46984  fourierswlem  46985  fouriersw  46986  etransclem18  47007  etransclem23  47012  etransclem46  47035  etransclem47  47036  etransclem48  47037  etransc  47038  goldrasin  47660  goldratmolem2  47664  tgoldbach  48623  crosspdotsumi  50687  crosspdoti  50688  crosspalti  50689  crossp3i  50690