Theorem nncnd 12165

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 12154	. 2 ⊢ ℕ ⊆ ℂ
2		nnred.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
3	1, 2	sselid 3932	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11028  ℕcn 12149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7682  ax-1cn 11088  ax-addcl 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12150

This theorem is referenced by:  nneo  12580  facdiv  14214  facndiv  14215  faclbnd  14217  faclbnd5  14225  faclbnd6  14226  facubnd  14227  facavg  14228  bccmpl  14236  bcn0  14237  bcn1  14240  bcm1k  14242  bcp1n  14243  bcp1nk  14244  bcval5  14245  bcpasc  14248  permnn  14253  hashf1  14384  hashfac  14385  relexpaddnn  14978  binom11  15759  binom1dif  15760  climcndslem2  15777  arisum2  15788  trireciplem  15789  trirecip  15790  geo2sum  15800  geo2lim  15802  fprodfac  15900  risefacfac  15962  fallfacfwd  15963  fallfacval4  15970  bcfallfac  15971  fallfacfac  15972  bpolycl  15979  bpolysum  15980  bpolydiflem  15981  fsumkthpow  15983  eftcl  16000  eftabs  16002  efcllem  16004  ege2le3  16017  efcj  16019  efaddlem  16020  eftlub  16038  eirrlem  16133  sqrt2irrlem  16177  oexpneg  16276  pwp1fsum  16322  bitsp1  16362  bitsfzolem  16365  bitsfzo  16366  bitsmod  16367  bitscmp  16369  bitsinv1lem  16372  bitsinv1  16373  2ebits  16378  bitsinvp1  16380  sadcaddlem  16388  sadadd3  16392  bitsres  16404  bitsuz  16405  bitsshft  16406  dvdsgcdidd  16468  mulgcd  16479  rplpwr  16489  sqgcd  16493  expgcd  16494  nn0expgcd  16495  lcmgcdlem  16537  3lcm2e6woprm  16546  coprmprod  16592  coprmproddvdslem  16593  cncongr1  16598  cncongr2  16599  prmind2  16616  isprm5  16638  divgcdodd  16641  prmdvdsexpr  16648  qmuldeneqnum  16678  divnumden  16679  qnumgt0  16681  numdensq  16685  numdenexp  16691  hashdvds  16706  phiprmpw  16707  prmdiv  16716  prmdivdiv  16718  phisum  16722  modprm0  16737  pythagtriplem4  16751  pythagtriplem6  16753  pythagtriplem7  16754  pythagtriplem14  16760  pythagtriplem15  16761  pythagtriplem19  16765  pythagtrip  16766  pcprendvds2  16773  pcpre1  16774  pcpremul  16775  pceulem  16777  pcdiv  16784  pcqmul  16785  pcelnn  16802  pcid  16805  pc2dvds  16811  dvdsprmpweqnn  16817  dvdsprmpweqle  16818  pcaddlem  16820  pcadd  16821  pcfaclem  16830  qexpz  16833  expnprm  16834  oddprmdvds  16835  prmpwdvds  16836  pockthlem  16837  pockthg  16838  infpnlem1  16842  prmreclem1  16848  prmreclem2  16849  prmreclem3  16850  prmreclem4  16851  prmreclem6  16853  4sqlem6  16875  4sqlem7  16876  4sqlem10  16879  mul4sqlem  16885  4sqlem11  16887  4sqlem12  16888  4sqlem14  16890  4sqlem17  16893  4sqlem18  16894  vdwlem1  16913  vdwlem2  16914  vdwlem3  16915  vdwlem5  16917  vdwlem6  16918  vdwlem8  16920  vdwlem9  16921  vdwlem10  16922  vdwlem12  16924  ramub1lem2  16959  ramcl  16961  prmop1  16970  prmdvdsprmo  16974  prmgaplem7  16989  prmgaplem8  16990  chnub  18549  gsumsgrpccat  18769  mulgnndir  19037  mulgnnass  19043  psgnunilem5  19427  odf1o2  19506  pgp0  19529  sylow1lem1  19531  odcau  19537  sylow2blem3  19555  sylow3lem3  19562  sylow3lem4  19563  gexexlem  19785  ablfacrp2  20002  ablfac1lem  20003  ablfac1eu  20008  pgpfac1lem3a  20011  pgpfac1lem3  20012  fincygsubgodexd  20048  zringlpirlem3  21423  znrrg  21524  psdpw  22117  cpmadugsumlemF  22824  lebnumlem3  24922  ovollb2lem  25449  ovolunlem1a  25457  ovolunlem1  25458  uniioombllem3  25546  uniioombllem4  25547  dyaddisjlem  25556  mbfi1fseqlem3  25678  mbfi1fseqlem4  25679  itgpowd  26017  dgrcolem1  26239  vieta1lem1  26278  vieta1lem2  26279  elqaalem2  26288  elqaalem3  26289  aalioulem1  26300  aaliou3lem2  26311  aaliou3lem8  26313  aaliou3lem6  26316  aaliou3lem9  26318  taylfvallem1  26324  tayl0  26329  taylply2  26335  taylply2OLD  26336  taylply  26337  dvtaylp  26338  taylthlem1  26341  taylthlem2  26342  taylthlem2OLD  26343  pserdvlem2  26398  advlogexp  26624  cxpmul2  26658  cxpeq  26727  rtprmirr  26730  atantayl3  26909  leibpi  26912  log2cnv  26914  log2tlbnd  26915  birthdaylem2  26922  birthdaylem3  26923  amgmlem  26960  amgm  26961  emcllem5  26970  fsumharmonic  26982  zetacvg  26985  dmgmdivn0  26998  lgamgulmlem3  27001  lgamgulmlem4  27002  lgamgulmlem5  27003  lgamgulmlem6  27004  lgamgulm2  27006  lgamcvg2  27025  gamcvg  27026  gamcvg2lem  27029  facgam  27036  wilthlem1  27038  wilthlem2  27039  wilthlem3  27040  wilthimp  27042  basellem1  27051  basellem2  27052  basellem3  27053  basellem4  27054  basellem5  27055  basellem8  27058  vmaprm  27087  sgmval2  27113  0sgm  27114  sgmf  27115  vma1  27136  fsumdvdsdiaglem  27153  dvdsflf1o  27157  muinv  27163  mpodvdsmulf1o  27164  dvdsmulf1o  27166  sgmppw  27168  1sgmprm  27170  1sgm2ppw  27171  sgmmul  27172  chtublem  27182  fsumvma2  27185  chpchtsum  27190  logfaclbnd  27193  logexprlim  27196  mersenne  27198  perfect1  27199  perfectlem1  27200  perfectlem2  27201  perfect  27202  dchrsum2  27239  dchrhash  27242  bcmono  27248  bcp1ctr  27250  bclbnd  27251  bposlem1  27255  bposlem2  27256  bposlem3  27257  bposlem5  27259  bposlem6  27260  lgsval2lem  27278  lgsqrlem2  27318  gausslemma2dlem6  27343  gausslemma2dlem7  27344  gausslemma2d  27345  lgseisenlem1  27346  lgseisenlem4  27349  lgsquadlem1  27351  lgsquadlem2  27352  lgsquadlem3  27353  lgsquad2  27357  m1lgs  27359  2sqlem3  27391  2sqlem4  27392  chebbnd1lem1  27440  chebbnd1  27443  rplogsumlem1  27455  rplogsumlem2  27456  rpvmasumlem  27458  dchrisumlem1  27460  dchrmusum2  27465  dchrvmasumlem1  27466  dchrvmasum2lem  27467  dchrvmasum2if  27468  dchrvmasumlem2  27469  dchrvmasumlem3  27470  dchrvmasumiflem1  27472  dchrisum0flblem1  27479  dchrisum0flblem2  27480  dchrisum0fno1  27482  rpvmasum2  27483  rplogsum  27498  mulogsumlem  27502  mulogsum  27503  mulog2sumlem2  27506  vmalogdivsum2  27509  vmalogdivsum  27510  2vmadivsumlem  27511  logsqvma  27513  selberglem2  27517  selberglem3  27518  selberg  27519  selberg2lem  27521  logdivbnd  27527  selberg3lem1  27528  selberg4lem1  27531  pntrsumo1  27536  pntrsumbnd2  27538  selberg3r  27540  selberg4r  27541  selberg34r  27542  pntsval2  27547  pntrlog2bndlem2  27549  pntrlog2bndlem4  27551  pntrlog2bndlem6  27554  pntpbnd1  27557  pntpbnd2  27558  pntlemg  27569  pntlemn  27571  pntlemf  27576  pnt  27585  padicabvf  27602  ostth2lem2  27605  ostth3  27609  fusgrhashclwwlkn  30137  eucrct2eupth  30303  nrt2irr  30531  elq2  32873  numdenneg  32876  ltesubnnd  32884  2exple2exp  32907  oexpled  32909  gsummptp1  33121  1arithidomlem2  33598  1arithidom  33599  zringfrac  33616  cos9thpiminplylem1  33920  cos9thpiminplylem2  33921  1smat1  33942  madjusmdetlem2  33966  madjusmdetlem4  33968  qqhnm  34128  oddpwdc  34492  eulerpartlemsv2  34496  eulerpartlems  34498  eulerpartlemsv3  34499  eulerpartlemgc  34500  eulerpartlemv  34502  eulerpartlemgs2  34518  fibp1  34539  ballotlemfc0  34631  ballotlemfcc  34632  signsvtn0  34708  reprpmtf1o  34764  vtscl  34776  hgt750lemb  34794  tgoldbachgt  34801  subfacp1lem1  35354  subfacp1lem5  35359  subfacval2  35362  subfaclim  35363  cvmliftlem2  35461  cvmliftlem7  35466  cvmliftlem10  35469  cvmliftlem11  35470  cvmliftlem13  35471  bcm1nt  35912  bcprod  35913  iprodgam  35917  faclimlem1  35918  faclimlem2  35919  faclim2  35923  nn0prpwlem  36497  nn0prpw  36498  knoppcnlem10  36677  knoppndvlem16  36702  poimirlem1  37793  poimirlem2  37794  poimirlem6  37798  poimirlem7  37799  poimirlem8  37800  poimirlem9  37801  poimirlem10  37802  poimirlem11  37803  poimirlem12  37804  poimirlem13  37805  poimirlem15  37807  poimirlem16  37808  poimirlem17  37809  poimirlem18  37810  poimirlem19  37811  poimirlem20  37812  poimirlem21  37813  poimirlem22  37814  poimirlem23  37815  poimirlem24  37816  poimirlem25  37817  poimirlem26  37818  poimirlem27  37819  poimirlem31  37823  nnproddivdvdsd  42291  lcmfunnnd  42303  lcmineqlem3  42322  lcmineqlem4  42323  lcmineqlem6  42325  lcmineqlem8  42327  lcmineqlem10  42329  lcmineqlem11  42330  lcmineqlem12  42331  lcmineqlem16  42335  lcmineqlem18  42337  lcmineqlem23  42342  dvrelogpow2b  42359  aks4d1p1p2  42361  aks4d1p1  42367  aks4d1p8  42378  primrootsunit1  42388  primrootscoprmpow  42390  posbezout  42391  primrootscoprbij  42393  primrootspoweq0  42397  aks6d1c1p3  42401  aks6d1c1p8  42406  aks6d1c2p2  42410  hashscontpow1  42412  2np3bcnp1  42435  2ap1caineq  42436  sticksstones10  42446  sticksstones12a  42448  sticksstones16  42453  sticksstones22  42459  bcled  42469  bcle2d  42470  aks6d1c7lem1  42471  aks6d1c7  42475  unitscyglem2  42487  unitscyglem4  42489  unitscyglem5  42490  aks5lem8  42492  nnadddir  42561  nnmul1com  42562  nnmulcom  42563  oddnumth  42602  nicomachus  42603  zaddcom  42755  fltabcoprmex  42918  fltaccoprm  42919  fltbccoprm  42920  fltne  42923  flt4lem3  42927  flt4lem5elem  42930  flt4lem5a  42931  flt4lem5b  42932  flt4lem5c  42933  flt4lem5d  42934  flt4lem5e  42935  flt4lem5f  42936  flt4lem6  42937  flt4lem7  42938  nna4b4nsq  42939  fltltc  42940  fltnltalem  42941  fltnlta  42942  irrapxlem4  43103  irrapxlem5  43104  pellexlem2  43108  pellexlem6  43112  pell1234qrne0  43131  pell1234qrreccl  43132  pell1234qrmulcl  43133  pell1234qrdich  43139  pell14qrdich  43147  pell1qrge1  43148  pell1qr1  43149  pell14qrgapw  43154  rmxyneg  43198  rmxm1  43212  rmxluc  43214  rmxdbl  43217  jm2.19lem1  43267  jm2.27c  43285  relexpmulnn  43986  relexpmulg  43987  inductionexd  44432  hashnzfzclim  44599  bcccl  44616  bcc0  44617  bccp1k  44618  bccm1k  44619  binomcxplemwb  44625  fsumnncl  45854  mccllem  45879  clim1fr1  45883  sumnnodd  45912  dvsinexp  46191  dvxpaek  46220  dvnxpaek  46222  dvnprodlem2  46227  itgsinexplem1  46234  itgsinexp  46235  stoweidlem1  46281  stoweidlem11  46291  stoweidlem25  46305  stoweidlem26  46306  stoweidlem34  46314  stoweidlem37  46317  stoweidlem38  46318  stoweidlem42  46322  wallispi2lem1  46351  wallispi2  46353  stirlinglem4  46357  stirlinglem5  46358  stirlinglem10  46363  stirlinglem15  46368  dirkertrigeqlem3  46380  dirkertrigeq  46381  dirkercncflem2  46384  dirkercncflem4  46386  fourierdlem11  46398  fourierdlem15  46402  fourierdlem79  46465  fourierdlem83  46469  sqwvfourb  46509  etransclem14  46528  etransclem15  46529  etransclem20  46534  etransclem21  46535  etransclem22  46536  etransclem23  46537  etransclem24  46538  etransclem25  46539  etransclem28  46542  etransclem31  46545  etransclem32  46546  etransclem33  46547  etransclem34  46548  etransclem35  46549  etransclem38  46552  etransclem41  46555  etransclem44  46558  etransclem45  46559  etransclem47  46561  etransclem48  46562  nnfoctbdjlem  46735  deccarry  47593  iccpartgtprec  47702  fmtnoodd  47815  fmtnorec2lem  47824  fmtnorec2  47825  fmtnodvds  47826  goldbachthlem2  47828  fmtnorec3  47830  fmtnorec4  47831  fmtnoprmfac1lem  47846  fmtnoprmfac1  47847  fmtnoprmfac2lem1  47848  fmtnoprmfac2  47849  2pwp1prm  47871  sfprmdvdsmersenne  47885  lighneallem4b  47891  lighneal  47893  proththdlem  47895  proththd  47896  oexpnegALTV  47959  perfectALTVlem1  48003  perfectALTVlem2  48004  perfectALTV  48005  nnpw2pmod  48865  nnolog2flm1  48872  blennn0em1  48873  blengt1fldiv2p1  48875  nn0sumshdiglemB  48902  amgmlemALT  50084