Theorem recni 11251

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

This proof depends on syntax axioms:   ∈ wcel 2145  ℂcc 11126  ℝcr 11127

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 2147  ax-resscn 11185

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

This theorem is used by:  0cnALT  11473  renegcli  11547  resubcli  11548  recgt0ii  12149  ledivp1i  12168  ltdivp1i  12169  2cnALT  12345  numltc  12771  sqge0i  14256  lt2sqi  14257  le2sqi  14258  sq11i  14259  crreczi  14296  faclbnd4lem1  14361  sqrtmsq2i  15479  abs3lemi  15502  0.999...  15974  bpoly4  16151  ef01bndlem  16278  sin4lt0  16289  eirrlem  16298  rpnnen2lem3  16310  rpnnen2lem9  16316  rpnnen2lem11  16318  dvdslelem  16405  divalglem1  16490  divalglem2  16491  divalglem5  16493  divalglem6  16494  divalglem9  16497  prmreclem6  17019  modsubi  17170  pcoass  25258  aaliou3lem7  26592  picn  26701  sinhalfpilem  26708  cosneghalfpi  26715  sinhalfpip  26737  sinhalfpim  26738  coshalfpip  26739  coshalfpim  26740  sincosq1sgn  26743  sincosq2sgn  26744  sincosq3sgn  26745  sincosq4sgn  26746  sincos4thpi  26758  tan4thpi  26759  tan4thpiOLD  26760  sincos6thpi  26761  pige3ALT  26765  cosne0  26774  sinord  26779  resinf1o  26781  efif1olem2  26788  efif1olem4  26790  efifo  26792  logi  26832  logimul  26859  ecxp  26918  cxpsqrtlem  26947  2irrexpq  26976  elogb  27015  logblog  27037  sqrt2cxp2logb9e3  27044  ang180lem1  27054  ang180lem2  27055  1cubrlem  27086  quartlem3  27104  asinsin  27137  acoscos  27138  asin1  27139  reasinsin  27141  acosbnd  27145  atanlogsublem  27160  atanbnd  27171  atan1  27173  log2tlbnd  27190  log2ublem1  27191  log2le1  27195  birthday  27199  basellem8  27332  basellem9  27333  cht2  27416  mumullem2  27424  chtublem  27455  chtub  27456  bposlem6  27533  bposlem7  27534  bposlem8  27535  bposlem9  27536  chebbnd1lem3  27715  chebbnd1  27716  chto1ub  27720  mulogsumlem  27775  mulog2sumlem1  27778  mulog2sumlem2  27779  mulog2sumlem3  27780  pntibndlem3  27836  ex-ceil  30936  nmblolbii  31288  ip0i  31314  ip1ilem  31315  ipasslem10  31328  siilem1  31340  siii  31342  normlem1  31599  normlem3  31601  normlem5  31603  normlem6  31604  norm-ii-i  31626  normsubi  31630  norm3adifii  31637  norm3lem  31638  normpar2i  31645  bcsiALT  31668  pjneli  32212  lnophmlem2  32506  nmbdoplbi  32513  nmcoplbi  32517  nmophmi  32520  nmbdfnlbi  32538  nmcfnlbi  32541  cnlnadjlem2  32557  cnlnadjlem7  32562  nmopadjlem  32578  nmopcoi  32584  nmopcoadji  32590  nmopcoadj0i  32592  unierri  32593  opsqrlem1  32629  dfdec100  33308  dp20u  33331  dp2ltsuc  33339  dpfrac1  33345  dpmul10  33348  decdiv10  33349  dpmul100  33350  dp3mul10  33351  dpmul1000  33352  dpexpp1  33361  dpadd2  33363  dpadd3  33365  dpmul  33366  dpmul4  33367  threehalves  33368  hgt750lemd  35164  hgt750lem  35167  hgt750lem2  35168  subfaclim  35775  subfacval3  35776  problem2  36253  problem3  36254  problem4  36255  problem5  36256  circum  36261  iexpire  36322  taupilem1  38081  dvacos  38462  fdc  38503  lcmineqlem23  42925  aks4d1p1p4  42945  aks4d1p1p7  42948  0cnALT3  43128  acos1half  43241  re1m1e0m0  43280  ipiiie0  43321  arearect  44064  areaquad  44065  sineq0ALT  45767  wallispilem2  46902  stirlinglem3  46912  stirlinglem4  46913  stirlinglem13  46922  stirlinglem15  46924  dirkerper  46932  fourierdlem24  46967  fourierdlem103  47045  fourierdlem104  47046  sqwvfoura  47064  sqwvfourb  47065  fourierswlem  47066  fouriersw  47067  etransclem18  47088  etransclem23  47093  etransclem46  47116  etransclem47  47117  etransclem48  47118  etransc  47119  goldrasin  47755  goldratmolem2  47759  goldratmolem3  47760  goldratmolem4  47761  goldratval  47762  tgoldbach  48741