Theorem nncnd 12162

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 11026  ℕcn 12146

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086  ax-addcl 11088

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12147

This theorem is referenced by:  nneo  12578  facdiv  14212  facndiv  14213  faclbnd  14215  faclbnd5  14223  faclbnd6  14224  facubnd  14225  facavg  14226  bccmpl  14234  bcn0  14235  bcn1  14238  bcm1k  14240  bcp1n  14241  bcp1nk  14242  bcval5  14243  bcpasc  14246  permnn  14251  hashf1  14382  hashfac  14383  relexpaddnn  14976  binom11  15757  binom1dif  15758  climcndslem2  15775  arisum2  15786  trireciplem  15787  trirecip  15788  geo2sum  15798  geo2lim  15800  fprodfac  15898  risefacfac  15960  fallfacfwd  15961  fallfacval4  15968  bcfallfac  15969  fallfacfac  15970  bpolycl  15977  bpolysum  15978  bpolydiflem  15979  fsumkthpow  15981  eftcl  15998  eftabs  16000  efcllem  16002  ege2le3  16015  efcj  16017  efaddlem  16018  eftlub  16036  eirrlem  16131  sqrt2irrlem  16175  oexpneg  16274  pwp1fsum  16320  bitsp1  16360  bitsfzolem  16363  bitsfzo  16364  bitsmod  16365  bitscmp  16367  bitsinv1lem  16370  bitsinv1  16371  2ebits  16376  bitsinvp1  16378  sadcaddlem  16386  sadadd3  16390  bitsres  16402  bitsuz  16403  bitsshft  16404  dvdsgcdidd  16466  mulgcd  16477  rplpwr  16487  sqgcd  16491  expgcd  16492  nn0expgcd  16493  lcmgcdlem  16535  3lcm2e6woprm  16544  coprmprod  16590  coprmproddvdslem  16591  cncongr1  16596  cncongr2  16597  prmind2  16614  isprm5  16636  divgcdodd  16639  prmdvdsexpr  16646  qmuldeneqnum  16676  divnumden  16677  qnumgt0  16679  numdensq  16683  numdenexp  16689  hashdvds  16704  phiprmpw  16705  prmdiv  16714  prmdivdiv  16716  phisum  16720  modprm0  16735  pythagtriplem4  16749  pythagtriplem6  16751  pythagtriplem7  16752  pythagtriplem14  16758  pythagtriplem15  16759  pythagtriplem19  16763  pythagtrip  16764  pcprendvds2  16771  pcpre1  16772  pcpremul  16773  pceulem  16775  pcdiv  16782  pcqmul  16783  pcelnn  16800  pcid  16803  pc2dvds  16809  dvdsprmpweqnn  16815  dvdsprmpweqle  16816  pcaddlem  16818  pcadd  16819  pcfaclem  16828  qexpz  16831  expnprm  16832  oddprmdvds  16833  prmpwdvds  16834  pockthlem  16835  pockthg  16836  infpnlem1  16840  prmreclem1  16846  prmreclem2  16847  prmreclem3  16848  prmreclem4  16849  prmreclem6  16851  4sqlem6  16873  4sqlem7  16874  4sqlem10  16877  mul4sqlem  16883  4sqlem11  16885  4sqlem12  16886  4sqlem14  16888  4sqlem17  16891  4sqlem18  16892  vdwlem1  16911  vdwlem2  16912  vdwlem3  16913  vdwlem5  16915  vdwlem6  16916  vdwlem8  16918  vdwlem9  16919  vdwlem10  16920  vdwlem12  16922  ramub1lem2  16957  ramcl  16959  prmop1  16968  prmdvdsprmo  16972  prmgaplem7  16987  prmgaplem8  16988  gsumsgrpccat  18732  mulgnndir  19000  mulgnnass  19006  psgnunilem5  19391  odf1o2  19470  pgp0  19493  sylow1lem1  19495  odcau  19501  sylow2blem3  19519  sylow3lem3  19526  sylow3lem4  19527  gexexlem  19749  ablfacrp2  19966  ablfac1lem  19967  ablfac1eu  19972  pgpfac1lem3a  19975  pgpfac1lem3  19976  fincygsubgodexd  20012  zringlpirlem3  21389  znrrg  21490  psdpw  22073  cpmadugsumlemF  22779  lebnumlem3  24878  ovollb2lem  25405  ovolunlem1a  25413  ovolunlem1  25414  uniioombllem3  25502  uniioombllem4  25503  dyaddisjlem  25512  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  itgpowd  25973  dgrcolem1  26195  vieta1lem1  26234  vieta1lem2  26235  elqaalem2  26244  elqaalem3  26245  aalioulem1  26256  aaliou3lem2  26267  aaliou3lem8  26269  aaliou3lem6  26272  aaliou3lem9  26274  taylfvallem1  26280  tayl0  26285  taylply2  26291  taylply2OLD  26292  taylply  26293  dvtaylp  26294  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  pserdvlem2  26354  advlogexp  26580  cxpmul2  26614  cxpeq  26683  rtprmirr  26686  atantayl3  26865  leibpi  26868  log2cnv  26870  log2tlbnd  26871  birthdaylem2  26878  birthdaylem3  26879  amgmlem  26916  amgm  26917  emcllem5  26926  fsumharmonic  26938  zetacvg  26941  dmgmdivn0  26954  lgamgulmlem3  26957  lgamgulmlem4  26958  lgamgulmlem5  26959  lgamgulmlem6  26960  lgamgulm2  26962  lgamcvg2  26981  gamcvg  26982  gamcvg2lem  26985  facgam  26992  wilthlem1  26994  wilthlem2  26995  wilthlem3  26996  wilthimp  26998  basellem1  27007  basellem2  27008  basellem3  27009  basellem4  27010  basellem5  27011  basellem8  27014  vmaprm  27043  sgmval2  27069  0sgm  27070  sgmf  27071  vma1  27092  fsumdvdsdiaglem  27109  dvdsflf1o  27113  muinv  27119  mpodvdsmulf1o  27120  dvdsmulf1o  27122  sgmppw  27124  1sgmprm  27126  1sgm2ppw  27127  sgmmul  27128  chtublem  27138  fsumvma2  27141  chpchtsum  27146  logfaclbnd  27149  logexprlim  27152  mersenne  27154  perfect1  27155  perfectlem1  27156  perfectlem2  27157  perfect  27158  dchrsum2  27195  dchrhash  27198  bcmono  27204  bcp1ctr  27206  bclbnd  27207  bposlem1  27211  bposlem2  27212  bposlem3  27213  bposlem5  27215  bposlem6  27216  lgsval2lem  27234  lgsqrlem2  27274  gausslemma2dlem6  27299  gausslemma2dlem7  27300  gausslemma2d  27301  lgseisenlem1  27302  lgseisenlem4  27305  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  lgsquad2  27313  m1lgs  27315  2sqlem3  27347  2sqlem4  27348  chebbnd1lem1  27396  chebbnd1  27399  rplogsumlem1  27411  rplogsumlem2  27412  rpvmasumlem  27414  dchrisumlem1  27416  dchrmusum2  27421  dchrvmasumlem1  27422  dchrvmasum2lem  27423  dchrvmasum2if  27424  dchrvmasumlem2  27425  dchrvmasumlem3  27426  dchrvmasumiflem1  27428  dchrisum0flblem1  27435  dchrisum0flblem2  27436  dchrisum0fno1  27438  rpvmasum2  27439  rplogsum  27454  mulogsumlem  27458  mulogsum  27459  mulog2sumlem2  27462  vmalogdivsum2  27465  vmalogdivsum  27466  2vmadivsumlem  27467  logsqvma  27469  selberglem2  27473  selberglem3  27474  selberg  27475  selberg2lem  27477  logdivbnd  27483  selberg3lem1  27484  selberg4lem1  27487  pntrsumo1  27492  pntrsumbnd2  27494  selberg3r  27496  selberg4r  27497  selberg34r  27498  pntsval2  27503  pntrlog2bndlem2  27505  pntrlog2bndlem4  27507  pntrlog2bndlem6  27510  pntpbnd1  27513  pntpbnd2  27514  pntlemg  27525  pntlemn  27527  pntlemf  27532  pnt  27541  padicabvf  27558  ostth2lem2  27561  ostth3  27565  fusgrhashclwwlkn  30041  eucrct2eupth  30207  nrt2irr  30435  elq2  32769  numdenneg  32772  ltesubnnd  32780  2exple2exp  32803  oexpled  32805  chnub  32967  1arithidomlem2  33483  1arithidom  33484  zringfrac  33501  cos9thpiminplylem1  33748  cos9thpiminplylem2  33749  1smat1  33770  madjusmdetlem2  33794  madjusmdetlem4  33796  qqhnm  33956  oddpwdc  34321  eulerpartlemsv2  34325  eulerpartlems  34327  eulerpartlemsv3  34328  eulerpartlemgc  34329  eulerpartlemv  34331  eulerpartlemgs2  34347  fibp1  34368  ballotlemfc0  34460  ballotlemfcc  34461  signsvtn0  34537  reprpmtf1o  34593  vtscl  34605  hgt750lemb  34623  tgoldbachgt  34630  subfacp1lem1  35151  subfacp1lem5  35156  subfacval2  35159  subfaclim  35160  cvmliftlem2  35258  cvmliftlem7  35263  cvmliftlem10  35266  cvmliftlem11  35267  cvmliftlem13  35268  bcm1nt  35709  bcprod  35710  iprodgam  35714  faclimlem1  35715  faclimlem2  35716  faclim2  35720  nn0prpwlem  36295  nn0prpw  36296  knoppcnlem10  36475  knoppndvlem16  36500  poimirlem1  37600  poimirlem2  37601  poimirlem6  37605  poimirlem7  37606  poimirlem8  37607  poimirlem9  37608  poimirlem10  37609  poimirlem11  37610  poimirlem12  37611  poimirlem13  37612  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  poimirlem21  37620  poimirlem22  37621  poimirlem23  37622  poimirlem24  37623  poimirlem25  37624  poimirlem26  37625  poimirlem27  37626  poimirlem31  37630  nnproddivdvdsd  41973  lcmfunnnd  41985  lcmineqlem3  42004  lcmineqlem4  42005  lcmineqlem6  42007  lcmineqlem8  42009  lcmineqlem10  42011  lcmineqlem11  42012  lcmineqlem12  42013  lcmineqlem16  42017  lcmineqlem18  42019  lcmineqlem23  42024  dvrelogpow2b  42041  aks4d1p1p2  42043  aks4d1p1  42049  aks4d1p8  42060  primrootsunit1  42070  primrootscoprmpow  42072  posbezout  42073  primrootscoprbij  42075  primrootspoweq0  42079  aks6d1c1p3  42083  aks6d1c1p8  42088  aks6d1c2p2  42092  hashscontpow1  42094  2np3bcnp1  42117  2ap1caineq  42118  sticksstones10  42128  sticksstones12a  42130  sticksstones16  42135  sticksstones22  42141  bcled  42151  bcle2d  42152  aks6d1c7lem1  42153  aks6d1c7  42157  unitscyglem2  42169  unitscyglem4  42171  unitscyglem5  42172  aks5lem8  42174  nnadddir  42243  nnmul1com  42244  nnmulcom  42245  oddnumth  42284  nicomachus  42285  zaddcom  42437  fltabcoprmex  42612  fltaccoprm  42613  fltbccoprm  42614  fltne  42617  flt4lem3  42621  flt4lem5elem  42624  flt4lem5a  42625  flt4lem5b  42626  flt4lem5c  42627  flt4lem5d  42628  flt4lem5e  42629  flt4lem5f  42630  flt4lem6  42631  flt4lem7  42632  nna4b4nsq  42633  fltltc  42634  fltnltalem  42635  fltnlta  42636  irrapxlem4  42798  irrapxlem5  42799  pellexlem2  42803  pellexlem6  42807  pell1234qrne0  42826  pell1234qrreccl  42827  pell1234qrmulcl  42828  pell1234qrdich  42834  pell14qrdich  42842  pell1qrge1  42843  pell1qr1  42844  pell14qrgapw  42849  rmxyneg  42893  rmxm1  42907  rmxluc  42909  rmxdbl  42912  jm2.19lem1  42962  jm2.27c  42980  relexpmulnn  43682  relexpmulg  43683  inductionexd  44128  hashnzfzclim  44295  bcccl  44312  bcc0  44313  bccp1k  44314  bccm1k  44315  binomcxplemwb  44321  fsumnncl  45554  mccllem  45579  clim1fr1  45583  sumnnodd  45612  dvsinexp  45893  dvxpaek  45922  dvnxpaek  45924  dvnprodlem2  45929  itgsinexplem1  45936  itgsinexp  45937  stoweidlem1  45983  stoweidlem11  45993  stoweidlem25  46007  stoweidlem26  46008  stoweidlem34  46016  stoweidlem37  46019  stoweidlem38  46020  stoweidlem42  46024  wallispi2lem1  46053  wallispi2  46055  stirlinglem4  46059  stirlinglem5  46060  stirlinglem10  46065  stirlinglem15  46070  dirkertrigeqlem3  46082  dirkertrigeq  46083  dirkercncflem2  46086  dirkercncflem4  46088  fourierdlem11  46100  fourierdlem15  46104  fourierdlem79  46167  fourierdlem83  46171  sqwvfourb  46211  etransclem14  46230  etransclem15  46231  etransclem20  46236  etransclem21  46237  etransclem22  46238  etransclem23  46239  etransclem24  46240  etransclem25  46241  etransclem28  46244  etransclem31  46247  etransclem32  46248  etransclem33  46249  etransclem34  46250  etransclem35  46251  etransclem38  46254  etransclem41  46257  etransclem44  46260  etransclem45  46261  etransclem47  46263  etransclem48  46264  nnfoctbdjlem  46437  deccarry  47296  iccpartgtprec  47405  fmtnoodd  47518  fmtnorec2lem  47527  fmtnorec2  47528  fmtnodvds  47529  goldbachthlem2  47531  fmtnorec3  47533  fmtnorec4  47534  fmtnoprmfac1lem  47549  fmtnoprmfac1  47550  fmtnoprmfac2lem1  47551  fmtnoprmfac2  47552  2pwp1prm  47574  sfprmdvdsmersenne  47588  lighneallem4b  47594  lighneal  47596  proththdlem  47598  proththd  47599  oexpnegALTV  47662  perfectALTVlem1  47706  perfectALTVlem2  47707  perfectALTV  47708  nnpw2pmod  48556  nnolog2flm1  48563  blennn0em1  48564  blengt1fldiv2p1  48566  nn0sumshdiglemB  48593  amgmlemALT  49776