Theorem recni 11155

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

Syntax hints:   ∈ wcel 2121  ℂcc 11032  ℝcr 11033

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 1975  ax-7 2016  ax-8 2123  ax-resscn 11091

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-clel 2816  df-ss 3901

This theorem is referenced by:  0cnALT  11377  renegcli  11451  resubcli  11452  recgt0ii  12057  ledivp1i  12076  ltdivp1i  12077  2cnALT  12252  8th4div3  12392  numltc  12665  sqge0i  14145  lt2sqi  14146  le2sqi  14147  sq11i  14148  crreczi  14185  faclbnd4lem1  14250  sqrtmsq2i  15345  abs3lemi  15368  0.999...  15841  bpoly4  16019  ef01bndlem  16146  sin4lt0  16157  eirrlem  16166  rpnnen2lem3  16178  rpnnen2lem9  16184  rpnnen2lem11  16186  dvdslelem  16273  divalglem1  16358  divalglem2  16359  divalglem5  16361  divalglem6  16362  divalglem9  16365  prmreclem6  16887  modsubi  17038  pcoass  25012  aaliou3lem7  26336  picn  26443  sinhalfpilem  26448  cosneghalfpi  26455  sinhalfpip  26477  sinhalfpim  26478  coshalfpip  26479  coshalfpim  26480  sincosq1sgn  26483  sincosq2sgn  26484  sincosq3sgn  26485  sincosq4sgn  26486  sincos4thpi  26498  tan4thpi  26499  tan4thpiOLD  26500  sincos6thpi  26501  pige3ALT  26505  cosne0  26514  sinord  26519  resinf1o  26521  efif1olem2  26528  efif1olem4  26530  efifo  26532  logi  26572  logimul  26599  ecxp  26658  cxpsqrtlem  26687  2irrexpq  26716  elogb  26755  logblog  26777  sqrt2cxp2logb9e3  26784  ang180lem1  26794  ang180lem2  26795  1cubrlem  26826  quartlem3  26844  asinsin  26877  acoscos  26878  asin1  26879  reasinsin  26881  acosbnd  26885  atanlogsublem  26900  atanbnd  26911  atan1  26913  log2tlbnd  26930  log2ublem1  26931  log2le1  26935  birthday  26939  basellem8  27072  basellem9  27073  cht2  27156  mumullem2  27164  chtublem  27195  chtub  27196  bposlem6  27273  bposlem7  27274  bposlem8  27275  bposlem9  27276  chebbnd1lem3  27455  chebbnd1  27456  chto1ub  27460  mulogsumlem  27515  mulog2sumlem1  27518  mulog2sumlem2  27519  mulog2sumlem3  27520  pntibndlem3  27576  ex-ceil  30538  nmblolbii  30890  ip0i  30916  ip1ilem  30917  ipasslem10  30930  siilem1  30942  siii  30944  normlem1  31201  normlem3  31203  normlem5  31205  normlem6  31206  norm-ii-i  31228  normsubi  31232  norm3adifii  31239  norm3lem  31240  normpar2i  31247  bcsiALT  31270  pjneli  31814  lnophmlem2  32108  nmbdoplbi  32115  nmcoplbi  32119  nmophmi  32122  nmbdfnlbi  32140  nmcfnlbi  32143  cnlnadjlem2  32159  cnlnadjlem7  32164  nmopadjlem  32180  nmopcoi  32186  nmopcoadji  32192  nmopcoadj0i  32194  unierri  32195  opsqrlem1  32231  dfdec100  32924  dp20u  32958  dp2ltsuc  32966  dpfrac1  32972  dpmul10  32975  decdiv10  32976  dpmul100  32977  dp3mul10  32978  dpmul1000  32979  dpexpp1  32988  dpadd2  32990  dpadd3  32992  dpmul  32993  dpmul4  32994  threehalves  32995  hgt750lemd  34842  hgt750lem  34845  hgt750lem2  34846  subfaclim  35429  subfacval3  35430  problem2  35907  problem3  35908  problem4  35909  problem5  35910  circum  35915  iexpire  35976  taupilem1  37694  dvacos  38085  fdc  38125  lcmineqlem23  42549  aks4d1p1p4  42569  aks4d1p1p7  42572  0cnALT3  42750  acos1half  42848  re1m1e0m0  42887  ipiiie0  42928  arearect  43673  areaquad  43674  sineq0ALT  45393  wallispilem2  46521  stirlinglem3  46531  stirlinglem4  46532  stirlinglem13  46541  stirlinglem15  46543  dirkerper  46551  fourierdlem24  46586  fourierdlem103  46664  fourierdlem104  46665  sqwvfoura  46683  sqwvfourb  46684  fourierswlem  46685  fouriersw  46686  etransclem18  46707  etransclem23  46712  etransclem46  46735  etransclem47  46736  etransclem48  46737  etransc  46738  goldrasin  47357  goldratmolem2  47361  tgoldbach  48320