Theorem nncnd 12173

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℕcn 12157

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 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096  ax-addcl 11098

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 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158

This theorem is referenced by:  nneo  12588  facdiv  14222  facndiv  14223  faclbnd  14225  faclbnd5  14233  faclbnd6  14234  facubnd  14235  facavg  14236  bccmpl  14244  bcn0  14245  bcn1  14248  bcm1k  14250  bcp1n  14251  bcp1nk  14252  bcval5  14253  bcpasc  14256  permnn  14261  hashf1  14392  hashfac  14393  relexpaddnn  14986  binom11  15767  binom1dif  15768  climcndslem2  15785  arisum2  15796  trireciplem  15797  trirecip  15798  geo2sum  15808  geo2lim  15810  fprodfac  15908  risefacfac  15970  fallfacfwd  15971  fallfacval4  15978  bcfallfac  15979  fallfacfac  15980  bpolycl  15987  bpolysum  15988  bpolydiflem  15989  fsumkthpow  15991  eftcl  16008  eftabs  16010  efcllem  16012  ege2le3  16025  efcj  16027  efaddlem  16028  eftlub  16046  eirrlem  16141  sqrt2irrlem  16185  oexpneg  16284  pwp1fsum  16330  bitsp1  16370  bitsfzolem  16373  bitsfzo  16374  bitsmod  16375  bitscmp  16377  bitsinv1lem  16380  bitsinv1  16381  2ebits  16386  bitsinvp1  16388  sadcaddlem  16396  sadadd3  16400  bitsres  16412  bitsuz  16413  bitsshft  16414  dvdsgcdidd  16476  mulgcd  16487  rplpwr  16497  sqgcd  16501  expgcd  16502  nn0expgcd  16503  lcmgcdlem  16545  3lcm2e6woprm  16554  coprmprod  16600  coprmproddvdslem  16601  cncongr1  16606  cncongr2  16607  prmind2  16624  isprm5  16646  divgcdodd  16649  prmdvdsexpr  16656  qmuldeneqnum  16686  divnumden  16687  qnumgt0  16689  numdensq  16693  numdenexp  16699  hashdvds  16714  phiprmpw  16715  prmdiv  16724  prmdivdiv  16726  phisum  16730  modprm0  16745  pythagtriplem4  16759  pythagtriplem6  16761  pythagtriplem7  16762  pythagtriplem14  16768  pythagtriplem15  16769  pythagtriplem19  16773  pythagtrip  16774  pcprendvds2  16781  pcpre1  16782  pcpremul  16783  pceulem  16785  pcdiv  16792  pcqmul  16793  pcelnn  16810  pcid  16813  pc2dvds  16819  dvdsprmpweqnn  16825  dvdsprmpweqle  16826  pcaddlem  16828  pcadd  16829  pcfaclem  16838  qexpz  16841  expnprm  16842  oddprmdvds  16843  prmpwdvds  16844  pockthlem  16845  pockthg  16846  infpnlem1  16850  prmreclem1  16856  prmreclem2  16857  prmreclem3  16858  prmreclem4  16859  prmreclem6  16861  4sqlem6  16883  4sqlem7  16884  4sqlem10  16887  mul4sqlem  16893  4sqlem11  16895  4sqlem12  16896  4sqlem14  16898  4sqlem17  16901  4sqlem18  16902  vdwlem1  16921  vdwlem2  16922  vdwlem3  16923  vdwlem5  16925  vdwlem6  16926  vdwlem8  16928  vdwlem9  16929  vdwlem10  16930  vdwlem12  16932  ramub1lem2  16967  ramcl  16969  prmop1  16978  prmdvdsprmo  16982  prmgaplem7  16997  prmgaplem8  16998  chnub  18557  gsumsgrpccat  18777  mulgnndir  19045  mulgnnass  19051  psgnunilem5  19435  odf1o2  19514  pgp0  19537  sylow1lem1  19539  odcau  19545  sylow2blem3  19563  sylow3lem3  19570  sylow3lem4  19571  gexexlem  19793  ablfacrp2  20010  ablfac1lem  20011  ablfac1eu  20016  pgpfac1lem3a  20019  pgpfac1lem3  20020  fincygsubgodexd  20056  zringlpirlem3  21431  znrrg  21532  psdpw  22125  cpmadugsumlemF  22832  lebnumlem3  24930  ovollb2lem  25457  ovolunlem1a  25465  ovolunlem1  25466  uniioombllem3  25554  uniioombllem4  25555  dyaddisjlem  25564  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  itgpowd  26025  dgrcolem1  26247  vieta1lem1  26286  vieta1lem2  26287  elqaalem2  26296  elqaalem3  26297  aalioulem1  26308  aaliou3lem2  26319  aaliou3lem8  26321  aaliou3lem6  26324  aaliou3lem9  26326  taylfvallem1  26332  tayl0  26337  taylply2  26343  taylply2OLD  26344  taylply  26345  dvtaylp  26346  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  pserdvlem2  26406  advlogexp  26632  cxpmul2  26666  cxpeq  26735  rtprmirr  26738  atantayl3  26917  leibpi  26920  log2cnv  26922  log2tlbnd  26923  birthdaylem2  26930  birthdaylem3  26931  amgmlem  26968  amgm  26969  emcllem5  26978  fsumharmonic  26990  zetacvg  26993  dmgmdivn0  27006  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamgulm2  27014  lgamcvg2  27033  gamcvg  27034  gamcvg2lem  27037  facgam  27044  wilthlem1  27046  wilthlem2  27047  wilthlem3  27048  wilthimp  27050  basellem1  27059  basellem2  27060  basellem3  27061  basellem4  27062  basellem5  27063  basellem8  27066  vmaprm  27095  sgmval2  27121  0sgm  27122  sgmf  27123  vma1  27144  fsumdvdsdiaglem  27161  dvdsflf1o  27165  muinv  27171  mpodvdsmulf1o  27172  dvdsmulf1o  27174  sgmppw  27176  1sgmprm  27178  1sgm2ppw  27179  sgmmul  27180  chtublem  27190  fsumvma2  27193  chpchtsum  27198  logfaclbnd  27201  logexprlim  27204  mersenne  27206  perfect1  27207  perfectlem1  27208  perfectlem2  27209  perfect  27210  dchrsum2  27247  dchrhash  27250  bcmono  27256  bcp1ctr  27258  bclbnd  27259  bposlem1  27263  bposlem2  27264  bposlem3  27265  bposlem5  27267  bposlem6  27268  lgsval2lem  27286  lgsqrlem2  27326  gausslemma2dlem6  27351  gausslemma2dlem7  27352  gausslemma2d  27353  lgseisenlem1  27354  lgseisenlem4  27357  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  lgsquad2  27365  m1lgs  27367  2sqlem3  27399  2sqlem4  27400  chebbnd1lem1  27448  chebbnd1  27451  rplogsumlem1  27463  rplogsumlem2  27464  rpvmasumlem  27466  dchrisumlem1  27468  dchrmusum2  27473  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasum2if  27476  dchrvmasumlem2  27477  dchrvmasumlem3  27478  dchrvmasumiflem1  27480  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0fno1  27490  rpvmasum2  27491  rplogsum  27506  mulogsumlem  27510  mulogsum  27511  mulog2sumlem2  27514  vmalogdivsum2  27517  vmalogdivsum  27518  2vmadivsumlem  27519  logsqvma  27521  selberglem2  27525  selberglem3  27526  selberg  27527  selberg2lem  27529  logdivbnd  27535  selberg3lem1  27536  selberg4lem1  27539  pntrsumo1  27544  pntrsumbnd2  27546  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntsval2  27555  pntrlog2bndlem2  27557  pntrlog2bndlem4  27559  pntrlog2bndlem6  27562  pntpbnd1  27565  pntpbnd2  27566  pntlemg  27577  pntlemn  27579  pntlemf  27584  pnt  27593  padicabvf  27610  ostth2lem2  27613  ostth3  27617  fusgrhashclwwlkn  30166  eucrct2eupth  30332  nrt2irr  30560  elq2  32902  numdenneg  32905  ltesubnnd  32913  2exple2exp  32936  oexpled  32938  gsummptp1  33150  1arithidomlem2  33628  1arithidom  33629  zringfrac  33646  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  1smat1  33981  madjusmdetlem2  34005  madjusmdetlem4  34007  qqhnm  34167  oddpwdc  34531  eulerpartlemsv2  34535  eulerpartlems  34537  eulerpartlemsv3  34538  eulerpartlemgc  34539  eulerpartlemv  34541  eulerpartlemgs2  34557  fibp1  34578  ballotlemfc0  34670  ballotlemfcc  34671  signsvtn0  34747  reprpmtf1o  34803  vtscl  34815  hgt750lemb  34833  tgoldbachgt  34840  subfacp1lem1  35392  subfacp1lem5  35397  subfacval2  35400  subfaclim  35401  cvmliftlem2  35499  cvmliftlem7  35504  cvmliftlem10  35507  cvmliftlem11  35508  cvmliftlem13  35509  bcm1nt  35950  bcprod  35951  iprodgam  35955  faclimlem1  35956  faclimlem2  35957  faclim2  35961  nn0prpwlem  36535  nn0prpw  36536  knoppcnlem10  36721  knoppndvlem16  36746  poimirlem1  37861  poimirlem2  37862  poimirlem6  37866  poimirlem7  37867  poimirlem8  37868  poimirlem9  37869  poimirlem10  37870  poimirlem11  37871  poimirlem12  37872  poimirlem13  37873  poimirlem15  37875  poimirlem16  37876  poimirlem17  37877  poimirlem18  37878  poimirlem19  37879  poimirlem20  37880  poimirlem21  37881  poimirlem22  37882  poimirlem23  37883  poimirlem24  37884  poimirlem25  37885  poimirlem26  37886  poimirlem27  37887  poimirlem31  37891  nnproddivdvdsd  42359  lcmfunnnd  42371  lcmineqlem3  42390  lcmineqlem4  42391  lcmineqlem6  42393  lcmineqlem8  42395  lcmineqlem10  42397  lcmineqlem11  42398  lcmineqlem12  42399  lcmineqlem16  42403  lcmineqlem18  42405  lcmineqlem23  42410  dvrelogpow2b  42427  aks4d1p1p2  42429  aks4d1p1  42435  aks4d1p8  42446  primrootsunit1  42456  primrootscoprmpow  42458  posbezout  42459  primrootscoprbij  42461  primrootspoweq0  42465  aks6d1c1p3  42469  aks6d1c1p8  42474  aks6d1c2p2  42478  hashscontpow1  42480  2np3bcnp1  42503  2ap1caineq  42504  sticksstones10  42514  sticksstones12a  42516  sticksstones16  42521  sticksstones22  42527  bcled  42537  bcle2d  42538  aks6d1c7lem1  42539  aks6d1c7  42543  unitscyglem2  42555  unitscyglem4  42557  unitscyglem5  42558  aks5lem8  42560  nnadddir  42629  nnmul1com  42630  nnmulcom  42631  oddnumth  42670  nicomachus  42671  zaddcom  42823  fltabcoprmex  42986  fltaccoprm  42987  fltbccoprm  42988  fltne  42991  flt4lem3  42995  flt4lem5elem  42998  flt4lem5a  42999  flt4lem5b  43000  flt4lem5c  43001  flt4lem5d  43002  flt4lem5e  43003  flt4lem5f  43004  flt4lem6  43005  flt4lem7  43006  nna4b4nsq  43007  fltltc  43008  fltnltalem  43009  fltnlta  43010  irrapxlem4  43171  irrapxlem5  43172  pellexlem2  43176  pellexlem6  43180  pell1234qrne0  43199  pell1234qrreccl  43200  pell1234qrmulcl  43201  pell1234qrdich  43207  pell14qrdich  43215  pell1qrge1  43216  pell1qr1  43217  pell14qrgapw  43222  rmxyneg  43266  rmxm1  43280  rmxluc  43282  rmxdbl  43285  jm2.19lem1  43335  jm2.27c  43353  relexpmulnn  44054  relexpmulg  44055  inductionexd  44500  hashnzfzclim  44667  bcccl  44684  bcc0  44685  bccp1k  44686  bccm1k  44687  binomcxplemwb  44693  fsumnncl  45921  mccllem  45946  clim1fr1  45950  sumnnodd  45979  dvsinexp  46258  dvxpaek  46287  dvnxpaek  46289  dvnprodlem2  46294  itgsinexplem1  46301  itgsinexp  46302  stoweidlem1  46348  stoweidlem11  46358  stoweidlem25  46372  stoweidlem26  46373  stoweidlem34  46381  stoweidlem37  46384  stoweidlem38  46385  stoweidlem42  46389  wallispi2lem1  46418  wallispi2  46420  stirlinglem4  46424  stirlinglem5  46425  stirlinglem10  46430  stirlinglem15  46435  dirkertrigeqlem3  46447  dirkertrigeq  46448  dirkercncflem2  46451  dirkercncflem4  46453  fourierdlem11  46465  fourierdlem15  46469  fourierdlem79  46532  fourierdlem83  46536  sqwvfourb  46576  etransclem14  46595  etransclem15  46596  etransclem20  46601  etransclem21  46602  etransclem22  46603  etransclem23  46604  etransclem24  46605  etransclem25  46606  etransclem28  46609  etransclem31  46612  etransclem32  46613  etransclem33  46614  etransclem34  46615  etransclem35  46616  etransclem38  46619  etransclem41  46622  etransclem44  46625  etransclem45  46626  etransclem47  46628  etransclem48  46629  nnfoctbdjlem  46802  deccarry  47660  iccpartgtprec  47769  fmtnoodd  47882  fmtnorec2lem  47891  fmtnorec2  47892  fmtnodvds  47893  goldbachthlem2  47895  fmtnorec3  47897  fmtnorec4  47898  fmtnoprmfac1lem  47913  fmtnoprmfac1  47914  fmtnoprmfac2lem1  47915  fmtnoprmfac2  47916  2pwp1prm  47938  sfprmdvdsmersenne  47952  lighneallem4b  47958  lighneal  47960  proththdlem  47962  proththd  47963  oexpnegALTV  48026  perfectALTVlem1  48070  perfectALTVlem2  48071  perfectALTV  48072  nnpw2pmod  48932  nnolog2flm1  48939  blennn0em1  48940  blengt1fldiv2p1  48942  nn0sumshdiglemB  48969  amgmlemALT  50151