Theorem recni 11247

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

Syntax hints:   ∈ wcel 2108  ℂcc 11125  ℝcr 11126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-resscn 11184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809  df-ss 3943

This theorem is referenced by:  0cnALT  11468  renegcli  11542  resubcli  11543  recgt0ii  12146  ledivp1i  12165  ltdivp1i  12166  2cnALT  12314  8th4div3  12459  numltc  12732  sqge0i  14204  lt2sqi  14205  le2sqi  14206  sq11i  14207  crreczi  14244  faclbnd4lem1  14309  sqrtmsq2i  15404  abs3lemi  15427  0.999...  15895  bpoly4  16073  ef01bndlem  16200  sin4lt0  16211  eirrlem  16220  rpnnen2lem3  16232  rpnnen2lem9  16238  rpnnen2lem11  16240  dvdslelem  16326  divalglem1  16411  divalglem2  16412  divalglem5  16414  divalglem6  16415  divalglem9  16418  prmreclem6  16939  modsubi  17090  pcoass  24973  aaliou3lem7  26307  picn  26417  sinhalfpilem  26422  cosneghalfpi  26429  sinhalfpip  26451  sinhalfpim  26452  coshalfpip  26453  coshalfpim  26454  sincosq1sgn  26457  sincosq2sgn  26458  sincosq3sgn  26459  sincosq4sgn  26460  sincos4thpi  26472  tan4thpi  26473  tan4thpiOLD  26474  sincos6thpi  26475  pige3ALT  26479  cosne0  26488  sinord  26493  resinf1o  26495  efif1olem2  26502  efif1olem4  26504  efifo  26506  logi  26546  logimul  26573  ecxp  26632  cxpsqrtlem  26661  2irrexpq  26690  elogb  26730  logblog  26752  sqrt2cxp2logb9e3  26759  ang180lem1  26769  ang180lem2  26770  1cubrlem  26801  quartlem3  26819  asinsin  26852  acoscos  26853  asin1  26854  reasinsin  26856  acosbnd  26860  atanlogsublem  26875  atanbnd  26886  atan1  26888  log2tlbnd  26905  log2ublem1  26906  log2le1  26910  birthday  26914  basellem8  27048  basellem9  27049  cht2  27132  mumullem2  27140  chtublem  27172  chtub  27173  bposlem6  27250  bposlem7  27251  bposlem8  27252  bposlem9  27253  chebbnd1lem3  27432  chebbnd1  27433  chto1ub  27437  mulogsumlem  27492  mulog2sumlem1  27495  mulog2sumlem2  27496  mulog2sumlem3  27497  pntibndlem3  27553  ex-ceil  30375  nmblolbii  30726  ip0i  30752  ip1ilem  30753  ipasslem10  30766  siilem1  30778  siii  30780  normlem1  31037  normlem3  31039  normlem5  31041  normlem6  31042  norm-ii-i  31064  normsubi  31068  norm3adifii  31075  norm3lem  31076  normpar2i  31083  bcsiALT  31106  pjneli  31650  lnophmlem2  31944  nmbdoplbi  31951  nmcoplbi  31955  nmophmi  31958  nmbdfnlbi  31976  nmcfnlbi  31979  cnlnadjlem2  31995  cnlnadjlem7  32000  nmopadjlem  32016  nmopcoi  32022  nmopcoadji  32028  nmopcoadj0i  32030  unierri  32031  opsqrlem1  32067  dfdec100  32755  dp20u  32798  dp2ltsuc  32806  dpfrac1  32812  dpmul10  32815  decdiv10  32816  dpmul100  32817  dp3mul10  32818  dpmul1000  32819  dpexpp1  32828  dpadd2  32830  dpadd3  32832  dpmul  32833  dpmul4  32834  threehalves  32835  hgt750lemd  34626  hgt750lem  34629  hgt750lem2  34630  subfaclim  35156  subfacval3  35157  problem2  35634  problem3  35635  problem4  35636  problem5  35637  circum  35642  iexpire  35698  taupilem1  37285  dvacos  37675  fdc  37715  lcmineqlem23  42010  aks4d1p1p4  42030  aks4d1p1p7  42033  0cnALT3  42251  acos1half  42348  re1m1e0m0  42387  ipiiie0  42427  arearect  43186  areaquad  43187  sineq0ALT  44909  wallispilem2  46043  stirlinglem3  46053  stirlinglem4  46054  stirlinglem13  46063  stirlinglem15  46065  dirkerper  46073  fourierdlem24  46108  fourierdlem103  46186  fourierdlem104  46187  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  etransclem18  46229  etransclem23  46234  etransclem46  46257  etransclem47  46258  etransclem48  46259  etransc  46260  tgoldbach  47779