Theorem recni 11228

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

Syntax hints:   ∈ wcel 2107  ℂcc 11108  ℝcr 11109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  0cnALT  11448  renegcli  11521  resubcli  11522  recgt0ii  12120  ledivp1i  12139  ltdivp1i  12140  2cnALT  12288  8th4div3  12432  numltc  12703  sqge0i  14152  lt2sqi  14153  le2sqi  14154  sq11i  14155  crreczi  14191  faclbnd4lem1  14253  sqrtmsq2i  15334  abs3lemi  15357  0.999...  15827  bpoly4  16003  ef01bndlem  16127  sin4lt0  16138  eirrlem  16147  rpnnen2lem3  16159  rpnnen2lem9  16165  rpnnen2lem11  16167  dvdslelem  16252  divalglem1  16337  divalglem2  16338  divalglem5  16340  divalglem6  16341  divalglem9  16344  prmreclem6  16854  modsubi  17005  pcoass  24540  aaliou3lem7  25862  picn  25969  sinhalfpilem  25973  cosneghalfpi  25980  sinhalfpip  26002  sinhalfpim  26003  coshalfpip  26004  coshalfpim  26005  sincosq1sgn  26008  sincosq2sgn  26009  sincosq3sgn  26010  sincosq4sgn  26011  sincos4thpi  26023  tan4thpi  26024  sincos6thpi  26025  pige3ALT  26029  cosne0  26038  sinord  26043  resinf1o  26045  efif1olem2  26052  efif1olem4  26054  efifo  26056  logimul  26122  ecxp  26181  cxpsqrtlem  26210  2irrexpq  26239  elogb  26275  logblog  26297  sqrt2cxp2logb9e3  26304  ang180lem1  26314  ang180lem2  26315  1cubrlem  26346  quartlem3  26364  asinsin  26397  acoscos  26398  asin1  26399  reasinsin  26401  acosbnd  26405  atanlogsublem  26420  atanbnd  26431  atan1  26433  log2tlbnd  26450  log2ublem1  26451  log2le1  26455  birthday  26459  basellem8  26592  basellem9  26593  cht2  26676  mumullem2  26684  chtublem  26714  chtub  26715  bposlem6  26792  bposlem7  26793  bposlem8  26794  bposlem9  26795  chebbnd1lem3  26974  chebbnd1  26975  chto1ub  26979  mulogsumlem  27034  mulog2sumlem1  27037  mulog2sumlem2  27038  mulog2sumlem3  27039  pntibndlem3  27095  ex-ceil  29732  nmblolbii  30083  ip0i  30109  ip1ilem  30110  ipasslem10  30123  siilem1  30135  siii  30137  normlem1  30394  normlem3  30396  normlem5  30398  normlem6  30399  norm-ii-i  30421  normsubi  30425  norm3adifii  30432  norm3lem  30433  normpar2i  30440  bcsiALT  30463  pjneli  31007  lnophmlem2  31301  nmbdoplbi  31308  nmcoplbi  31312  nmophmi  31315  nmbdfnlbi  31333  nmcfnlbi  31336  cnlnadjlem2  31352  cnlnadjlem7  31357  nmopadjlem  31373  nmopcoi  31379  nmopcoadji  31385  nmopcoadj0i  31387  unierri  31388  opsqrlem1  31424  dfdec100  32067  dp20u  32075  dp2ltsuc  32083  dpfrac1  32089  dpmul10  32092  decdiv10  32093  dpmul100  32094  dp3mul10  32095  dpmul1000  32096  dpexpp1  32105  dpadd2  32107  dpadd3  32109  dpmul  32110  dpmul4  32111  threehalves  32112  hgt750lemd  33691  hgt750lem  33694  hgt750lem2  33695  subfaclim  34210  subfacval3  34211  problem2  34682  problem3  34683  problem4  34684  problem5  34685  circum  34690  logi  34735  iexpire  34736  taupilem1  36250  dvacos  36621  fdc  36661  lcmineqlem23  40964  aks4d1p1p4  40984  aks4d1p1p7  40987  0cnALT3  41222  re1m1e0m0  41318  ipiiie0  41358  acos1half  41463  arearect  42012  areaquad  42013  sineq0ALT  43746  wallispilem2  44830  stirlinglem3  44840  stirlinglem4  44841  stirlinglem13  44850  stirlinglem15  44852  dirkerper  44860  fourierdlem24  44895  fourierdlem103  44973  fourierdlem104  44974  sqwvfoura  44992  sqwvfourb  44993  fourierswlem  44994  fouriersw  44995  etransclem18  45016  etransclem23  45021  etransclem46  45044  etransclem47  45045  etransclem48  45046  etransc  45047  tgoldbach  46533