Theorem nncnd 12209

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11073  ℕcn 12193

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194

This theorem is referenced by:  nneo  12625  facdiv  14259  facndiv  14260  faclbnd  14262  faclbnd5  14270  faclbnd6  14271  facubnd  14272  facavg  14273  bccmpl  14281  bcn0  14282  bcn1  14285  bcm1k  14287  bcp1n  14288  bcp1nk  14289  bcval5  14290  bcpasc  14293  permnn  14298  hashf1  14429  hashfac  14430  relexpaddnn  15024  binom11  15805  binom1dif  15806  climcndslem2  15823  arisum2  15834  trireciplem  15835  trirecip  15836  geo2sum  15846  geo2lim  15848  fprodfac  15946  risefacfac  16008  fallfacfwd  16009  fallfacval4  16016  bcfallfac  16017  fallfacfac  16018  bpolycl  16025  bpolysum  16026  bpolydiflem  16027  fsumkthpow  16029  eftcl  16046  eftabs  16048  efcllem  16050  ege2le3  16063  efcj  16065  efaddlem  16066  eftlub  16084  eirrlem  16179  sqrt2irrlem  16223  oexpneg  16322  pwp1fsum  16368  bitsp1  16408  bitsfzolem  16411  bitsfzo  16412  bitsmod  16413  bitscmp  16415  bitsinv1lem  16418  bitsinv1  16419  2ebits  16424  bitsinvp1  16426  sadcaddlem  16434  sadadd3  16438  bitsres  16450  bitsuz  16451  bitsshft  16452  dvdsgcdidd  16514  mulgcd  16525  rplpwr  16535  sqgcd  16539  expgcd  16540  nn0expgcd  16541  lcmgcdlem  16583  3lcm2e6woprm  16592  coprmprod  16638  coprmproddvdslem  16639  cncongr1  16644  cncongr2  16645  prmind2  16662  isprm5  16684  divgcdodd  16687  prmdvdsexpr  16694  qmuldeneqnum  16724  divnumden  16725  qnumgt0  16727  numdensq  16731  numdenexp  16737  hashdvds  16752  phiprmpw  16753  prmdiv  16762  prmdivdiv  16764  phisum  16768  modprm0  16783  pythagtriplem4  16797  pythagtriplem6  16799  pythagtriplem7  16800  pythagtriplem14  16806  pythagtriplem15  16807  pythagtriplem19  16811  pythagtrip  16812  pcprendvds2  16819  pcpre1  16820  pcpremul  16821  pceulem  16823  pcdiv  16830  pcqmul  16831  pcelnn  16848  pcid  16851  pc2dvds  16857  dvdsprmpweqnn  16863  dvdsprmpweqle  16864  pcaddlem  16866  pcadd  16867  pcfaclem  16876  qexpz  16879  expnprm  16880  oddprmdvds  16881  prmpwdvds  16882  pockthlem  16883  pockthg  16884  infpnlem1  16888  prmreclem1  16894  prmreclem2  16895  prmreclem3  16896  prmreclem4  16897  prmreclem6  16899  4sqlem6  16921  4sqlem7  16922  4sqlem10  16925  mul4sqlem  16931  4sqlem11  16933  4sqlem12  16934  4sqlem14  16936  4sqlem17  16939  4sqlem18  16940  vdwlem1  16959  vdwlem2  16960  vdwlem3  16961  vdwlem5  16963  vdwlem6  16964  vdwlem8  16966  vdwlem9  16967  vdwlem10  16968  vdwlem12  16970  ramub1lem2  17005  ramcl  17007  prmop1  17016  prmdvdsprmo  17020  prmgaplem7  17035  prmgaplem8  17036  gsumsgrpccat  18774  mulgnndir  19042  mulgnnass  19048  psgnunilem5  19431  odf1o2  19510  pgp0  19533  sylow1lem1  19535  odcau  19541  sylow2blem3  19559  sylow3lem3  19566  sylow3lem4  19567  gexexlem  19789  ablfacrp2  20006  ablfac1lem  20007  ablfac1eu  20012  pgpfac1lem3a  20015  pgpfac1lem3  20016  fincygsubgodexd  20052  zringlpirlem3  21381  znrrg  21482  psdpw  22064  cpmadugsumlemF  22770  lebnumlem3  24869  ovollb2lem  25396  ovolunlem1a  25404  ovolunlem1  25405  uniioombllem3  25493  uniioombllem4  25494  dyaddisjlem  25503  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  itgpowd  25964  dgrcolem1  26186  vieta1lem1  26225  vieta1lem2  26226  elqaalem2  26235  elqaalem3  26236  aalioulem1  26247  aaliou3lem2  26258  aaliou3lem8  26260  aaliou3lem6  26263  aaliou3lem9  26265  taylfvallem1  26271  tayl0  26276  taylply2  26282  taylply2OLD  26283  taylply  26284  dvtaylp  26285  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  pserdvlem2  26345  advlogexp  26571  cxpmul2  26605  cxpeq  26674  rtprmirr  26677  atantayl3  26856  leibpi  26859  log2cnv  26861  log2tlbnd  26862  birthdaylem2  26869  birthdaylem3  26870  amgmlem  26907  amgm  26908  emcllem5  26917  fsumharmonic  26929  zetacvg  26932  dmgmdivn0  26945  lgamgulmlem3  26948  lgamgulmlem4  26949  lgamgulmlem5  26950  lgamgulmlem6  26951  lgamgulm2  26953  lgamcvg2  26972  gamcvg  26973  gamcvg2lem  26976  facgam  26983  wilthlem1  26985  wilthlem2  26986  wilthlem3  26987  wilthimp  26989  basellem1  26998  basellem2  26999  basellem3  27000  basellem4  27001  basellem5  27002  basellem8  27005  vmaprm  27034  sgmval2  27060  0sgm  27061  sgmf  27062  vma1  27083  fsumdvdsdiaglem  27100  dvdsflf1o  27104  muinv  27110  mpodvdsmulf1o  27111  dvdsmulf1o  27113  sgmppw  27115  1sgmprm  27117  1sgm2ppw  27118  sgmmul  27119  chtublem  27129  fsumvma2  27132  chpchtsum  27137  logfaclbnd  27140  logexprlim  27143  mersenne  27145  perfect1  27146  perfectlem1  27147  perfectlem2  27148  perfect  27149  dchrsum2  27186  dchrhash  27189  bcmono  27195  bcp1ctr  27197  bclbnd  27198  bposlem1  27202  bposlem2  27203  bposlem3  27204  bposlem5  27206  bposlem6  27207  lgsval2lem  27225  lgsqrlem2  27265  gausslemma2dlem6  27290  gausslemma2dlem7  27291  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem4  27296  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  lgsquad2  27304  m1lgs  27306  2sqlem3  27338  2sqlem4  27339  chebbnd1lem1  27387  chebbnd1  27390  rplogsumlem1  27402  rplogsumlem2  27403  rpvmasumlem  27405  dchrisumlem1  27407  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrvmasum2if  27415  dchrvmasumlem2  27416  dchrvmasumlem3  27417  dchrvmasumiflem1  27419  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0fno1  27429  rpvmasum2  27430  rplogsum  27445  mulogsumlem  27449  mulogsum  27450  mulog2sumlem2  27453  vmalogdivsum2  27456  vmalogdivsum  27457  2vmadivsumlem  27458  logsqvma  27460  selberglem2  27464  selberglem3  27465  selberg  27466  selberg2lem  27468  logdivbnd  27474  selberg3lem1  27475  selberg4lem1  27478  pntrsumo1  27483  pntrsumbnd2  27485  selberg3r  27487  selberg4r  27488  selberg34r  27489  pntsval2  27494  pntrlog2bndlem2  27496  pntrlog2bndlem4  27498  pntrlog2bndlem6  27501  pntpbnd1  27504  pntpbnd2  27505  pntlemg  27516  pntlemn  27518  pntlemf  27523  pnt  27532  padicabvf  27549  ostth2lem2  27552  ostth3  27556  fusgrhashclwwlkn  30015  eucrct2eupth  30181  nrt2irr  30409  elq2  32743  numdenneg  32746  ltesubnnd  32754  2exple2exp  32777  oexpled  32779  chnub  32945  1arithidomlem2  33514  1arithidom  33515  zringfrac  33532  cos9thpiminplylem1  33779  cos9thpiminplylem2  33780  1smat1  33801  madjusmdetlem2  33825  madjusmdetlem4  33827  qqhnm  33987  oddpwdc  34352  eulerpartlemsv2  34356  eulerpartlems  34358  eulerpartlemsv3  34359  eulerpartlemgc  34360  eulerpartlemv  34362  eulerpartlemgs2  34378  fibp1  34399  ballotlemfc0  34491  ballotlemfcc  34492  signsvtn0  34568  reprpmtf1o  34624  vtscl  34636  hgt750lemb  34654  tgoldbachgt  34661  subfacp1lem1  35173  subfacp1lem5  35178  subfacval2  35181  subfaclim  35182  cvmliftlem2  35280  cvmliftlem7  35285  cvmliftlem10  35288  cvmliftlem11  35289  cvmliftlem13  35290  bcm1nt  35731  bcprod  35732  iprodgam  35736  faclimlem1  35737  faclimlem2  35738  faclim2  35742  nn0prpwlem  36317  nn0prpw  36318  knoppcnlem10  36497  knoppndvlem16  36522  poimirlem1  37622  poimirlem2  37623  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem31  37652  nnproddivdvdsd  41995  lcmfunnnd  42007  lcmineqlem3  42026  lcmineqlem4  42027  lcmineqlem6  42029  lcmineqlem8  42031  lcmineqlem10  42033  lcmineqlem11  42034  lcmineqlem12  42035  lcmineqlem16  42039  lcmineqlem18  42041  lcmineqlem23  42046  dvrelogpow2b  42063  aks4d1p1p2  42065  aks4d1p1  42071  aks4d1p8  42082  primrootsunit1  42092  primrootscoprmpow  42094  posbezout  42095  primrootscoprbij  42097  primrootspoweq0  42101  aks6d1c1p3  42105  aks6d1c1p8  42110  aks6d1c2p2  42114  hashscontpow1  42116  2np3bcnp1  42139  2ap1caineq  42140  sticksstones10  42150  sticksstones12a  42152  sticksstones16  42157  sticksstones22  42163  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  aks6d1c7  42179  unitscyglem2  42191  unitscyglem4  42193  unitscyglem5  42194  aks5lem8  42196  nnadddir  42265  nnmul1com  42266  nnmulcom  42267  oddnumth  42306  nicomachus  42307  zaddcom  42459  fltabcoprmex  42634  fltaccoprm  42635  fltbccoprm  42636  fltne  42639  flt4lem3  42643  flt4lem5elem  42646  flt4lem5a  42647  flt4lem5b  42648  flt4lem5c  42649  flt4lem5d  42650  flt4lem5e  42651  flt4lem5f  42652  flt4lem6  42653  flt4lem7  42654  nna4b4nsq  42655  fltltc  42656  fltnltalem  42657  fltnlta  42658  irrapxlem4  42820  irrapxlem5  42821  pellexlem2  42825  pellexlem6  42829  pell1234qrne0  42848  pell1234qrreccl  42849  pell1234qrmulcl  42850  pell1234qrdich  42856  pell14qrdich  42864  pell1qrge1  42865  pell1qr1  42866  pell14qrgapw  42871  rmxyneg  42916  rmxm1  42930  rmxluc  42932  rmxdbl  42935  jm2.19lem1  42985  jm2.27c  43003  relexpmulnn  43705  relexpmulg  43706  inductionexd  44151  hashnzfzclim  44318  bcccl  44335  bcc0  44336  bccp1k  44337  bccm1k  44338  binomcxplemwb  44344  fsumnncl  45577  mccllem  45602  clim1fr1  45606  sumnnodd  45635  dvsinexp  45916  dvxpaek  45945  dvnxpaek  45947  dvnprodlem2  45952  itgsinexplem1  45959  itgsinexp  45960  stoweidlem1  46006  stoweidlem11  46016  stoweidlem25  46030  stoweidlem26  46031  stoweidlem34  46039  stoweidlem37  46042  stoweidlem38  46043  stoweidlem42  46047  wallispi2lem1  46076  wallispi2  46078  stirlinglem4  46082  stirlinglem5  46083  stirlinglem10  46088  stirlinglem15  46093  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem11  46123  fourierdlem15  46127  fourierdlem79  46190  fourierdlem83  46194  sqwvfourb  46234  etransclem14  46253  etransclem15  46254  etransclem20  46259  etransclem21  46260  etransclem22  46261  etransclem23  46262  etransclem24  46263  etransclem25  46264  etransclem28  46267  etransclem31  46270  etransclem32  46271  etransclem33  46272  etransclem34  46273  etransclem35  46274  etransclem38  46277  etransclem41  46280  etransclem44  46283  etransclem45  46284  etransclem47  46286  etransclem48  46287  nnfoctbdjlem  46460  deccarry  47316  iccpartgtprec  47425  fmtnoodd  47538  fmtnorec2lem  47547  fmtnorec2  47548  fmtnodvds  47549  goldbachthlem2  47551  fmtnorec3  47553  fmtnorec4  47554  fmtnoprmfac1lem  47569  fmtnoprmfac1  47570  fmtnoprmfac2lem1  47571  fmtnoprmfac2  47572  2pwp1prm  47594  sfprmdvdsmersenne  47608  lighneallem4b  47614  lighneal  47616  proththdlem  47618  proththd  47619  oexpnegALTV  47682  perfectALTVlem1  47726  perfectALTVlem2  47727  perfectALTV  47728  nnpw2pmod  48576  nnolog2flm1  48583  blennn0em1  48584  blengt1fldiv2p1  48586  nn0sumshdiglemB  48613  amgmlemALT  49796