Theorem nncnd 9021

Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnred.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nncnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem nncnd

Step	Hyp	Ref	Expression
1		nnsscn 9012	. 2 ⊢ ℕ ⊆ ℂ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3182	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7894  ℕcn 9007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7987  ax-resscn 7988  ax-1re 7990  ax-addrcl 7993

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-in 3163  df-ss 3170  df-int 3876  df-inn 9008

This theorem is referenced by:  peano5uzti  9451  qapne  9730  qtri3or  10347  exbtwnzlemstep  10354  intfracq  10429  flqdiv  10430  modqmulnn  10451  addmodid  10481  modaddmodup  10496  modsumfzodifsn  10505  addmodlteq  10507  facdiv  10847  facndiv  10848  faclbnd  10850  faclbnd6  10853  facubnd  10854  facavg  10855  bccmpl  10863  bcn0  10864  bcn1  10867  bcm1k  10869  bcp1n  10870  bcp1nk  10871  bcval5  10872  bcpasc  10875  permnn  10880  cvg1nlemcxze  11164  cvg1nlemcau  11166  resqrexlemcalc3  11198  binom11  11668  binom1dif  11669  divcnv  11679  arisum2  11681  trireciplem  11682  trirecip  11683  expcnvap0  11684  geo2sum  11696  geo2lim  11698  cvgratnnlembern  11705  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  cvgratnnlemsumlt  11710  cvgratnnlemfm  11711  cvgratnnlemrate  11712  cvgratz  11714  eftcl  11836  eftabs  11838  efcllemp  11840  ege2le3  11853  efcj  11855  efaddlem  11856  eftlub  11872  eirraplem  11959  oexpneg  12059  divalglemnn  12100  bitsp1  12133  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitscmp  12140  bitsinv1lem  12143  bitsinv1  12144  dvdsgcdidd  12186  bezoutlemnewy  12188  mulgcd  12208  rplpwr  12219  sqgcd  12221  lcmgcdlem  12270  3lcm2e6woprm  12279  cncongr1  12296  cncongr2  12297  prmind2  12313  isprm5  12335  divgcdodd  12336  prmdvdsexpr  12343  sqrt2irrlem  12354  oddpwdclemxy  12362  oddpwdclemodd  12365  oddpwdclemdc  12366  oddpwdc  12367  sqpweven  12368  2sqpwodd  12369  sqrt2irraplemnn  12372  sqrt2irrap  12373  qmuldeneqnum  12388  divnumden  12389  qnumgt0  12391  numdensq  12395  hashdvds  12414  phiprmpw  12415  prmdiv  12428  prmdivdiv  12430  phisum  12434  modprm0  12448  pythagtriplem4  12462  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem14  12471  pythagtriplem15  12472  pythagtriplem16  12473  pythagtriplem19  12476  pythagtrip  12477  pcprendvds2  12485  pcpre1  12486  pcpremul  12487  pceulem  12488  pcdiv  12496  pcqmul  12497  pcelnn  12515  pcid  12518  pc2dvds  12524  dvdsprmpweqnn  12530  dvdsprmpweqle  12531  pcaddlem  12533  pcadd  12534  pcfaclem  12543  qexpz  12546  expnprm  12547  oddprmdvds  12548  prmpwdvds  12549  pockthlem  12550  pockthg  12551  infpnlem1  12553  4sqlem6  12577  4sqlem7  12578  4sqlem10  12581  mul4sqlem  12587  4sqlem11  12595  4sqlem12  12596  4sqlem14  12598  4sqlem17  12601  4sqlem18  12602  oddennn  12634  evenennn  12635  mulgnndir  13357  mulgnnass  13363  znrrg  14292  logbgcd1irraplemap  15289  wilthlem1  15300  0sgm  15305  mpodvdsmulf1o  15310  1sgmprm  15314  1sgm2ppw  15315  mersenne  15317  perfect1  15318  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgsval2lem  15335  gausslemma2dlem6  15392  gausslemma2dlem7  15393  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem2  15403  lgsquadlem3  15404  lgsquad2  15408  m1lgs  15410  2sqlem3  15442  2sqlem4  15443  trilpolemeq1  15771  trilpolemlt1  15772  redcwlpolemeq1  15785  nconstwlpolemgt0  15795