Theorem nncnd 12151

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11014  ℕcn 12135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677  ax-1cn 11074  ax-addcl 11076

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7358  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-nn 12136

This theorem is referenced by:  nneo  12567  facdiv  14204  facndiv  14205  faclbnd  14207  faclbnd5  14215  faclbnd6  14216  facubnd  14217  facavg  14218  bccmpl  14226  bcn0  14227  bcn1  14230  bcm1k  14232  bcp1n  14233  bcp1nk  14234  bcval5  14235  bcpasc  14238  permnn  14243  hashf1  14374  hashfac  14375  relexpaddnn  14968  binom11  15749  binom1dif  15750  climcndslem2  15767  arisum2  15778  trireciplem  15779  trirecip  15780  geo2sum  15790  geo2lim  15792  fprodfac  15890  risefacfac  15952  fallfacfwd  15953  fallfacval4  15960  bcfallfac  15961  fallfacfac  15962  bpolycl  15969  bpolysum  15970  bpolydiflem  15971  fsumkthpow  15973  eftcl  15990  eftabs  15992  efcllem  15994  ege2le3  16007  efcj  16009  efaddlem  16010  eftlub  16028  eirrlem  16123  sqrt2irrlem  16167  oexpneg  16266  pwp1fsum  16312  bitsp1  16352  bitsfzolem  16355  bitsfzo  16356  bitsmod  16357  bitscmp  16359  bitsinv1lem  16362  bitsinv1  16363  2ebits  16368  bitsinvp1  16370  sadcaddlem  16378  sadadd3  16382  bitsres  16394  bitsuz  16395  bitsshft  16396  dvdsgcdidd  16458  mulgcd  16469  rplpwr  16479  sqgcd  16483  expgcd  16484  nn0expgcd  16485  lcmgcdlem  16527  3lcm2e6woprm  16536  coprmprod  16582  coprmproddvdslem  16583  cncongr1  16588  cncongr2  16589  prmind2  16606  isprm5  16628  divgcdodd  16631  prmdvdsexpr  16638  qmuldeneqnum  16668  divnumden  16669  qnumgt0  16671  numdensq  16675  numdenexp  16681  hashdvds  16696  phiprmpw  16697  prmdiv  16706  prmdivdiv  16708  phisum  16712  modprm0  16727  pythagtriplem4  16741  pythagtriplem6  16743  pythagtriplem7  16744  pythagtriplem14  16750  pythagtriplem15  16751  pythagtriplem19  16755  pythagtrip  16756  pcprendvds2  16763  pcpre1  16764  pcpremul  16765  pceulem  16767  pcdiv  16774  pcqmul  16775  pcelnn  16792  pcid  16795  pc2dvds  16801  dvdsprmpweqnn  16807  dvdsprmpweqle  16808  pcaddlem  16810  pcadd  16811  pcfaclem  16820  qexpz  16823  expnprm  16824  oddprmdvds  16825  prmpwdvds  16826  pockthlem  16827  pockthg  16828  infpnlem1  16832  prmreclem1  16838  prmreclem2  16839  prmreclem3  16840  prmreclem4  16841  prmreclem6  16843  4sqlem6  16865  4sqlem7  16866  4sqlem10  16869  mul4sqlem  16875  4sqlem11  16877  4sqlem12  16878  4sqlem14  16880  4sqlem17  16883  4sqlem18  16884  vdwlem1  16903  vdwlem2  16904  vdwlem3  16905  vdwlem5  16907  vdwlem6  16908  vdwlem8  16910  vdwlem9  16911  vdwlem10  16912  vdwlem12  16914  ramub1lem2  16949  ramcl  16951  prmop1  16960  prmdvdsprmo  16964  prmgaplem7  16979  prmgaplem8  16980  chnub  18538  gsumsgrpccat  18758  mulgnndir  19026  mulgnnass  19032  psgnunilem5  19416  odf1o2  19495  pgp0  19518  sylow1lem1  19520  odcau  19526  sylow2blem3  19544  sylow3lem3  19551  sylow3lem4  19552  gexexlem  19774  ablfacrp2  19991  ablfac1lem  19992  ablfac1eu  19997  pgpfac1lem3a  20000  pgpfac1lem3  20001  fincygsubgodexd  20037  zringlpirlem3  21411  znrrg  21512  psdpw  22095  cpmadugsumlemF  22801  lebnumlem3  24899  ovollb2lem  25426  ovolunlem1a  25434  ovolunlem1  25435  uniioombllem3  25523  uniioombllem4  25524  dyaddisjlem  25533  mbfi1fseqlem3  25655  mbfi1fseqlem4  25656  itgpowd  25994  dgrcolem1  26216  vieta1lem1  26255  vieta1lem2  26256  elqaalem2  26265  elqaalem3  26266  aalioulem1  26277  aaliou3lem2  26288  aaliou3lem8  26290  aaliou3lem6  26293  aaliou3lem9  26295  taylfvallem1  26301  tayl0  26306  taylply2  26312  taylply2OLD  26313  taylply  26314  dvtaylp  26315  taylthlem1  26318  taylthlem2  26319  taylthlem2OLD  26320  pserdvlem2  26375  advlogexp  26601  cxpmul2  26635  cxpeq  26704  rtprmirr  26707  atantayl3  26886  leibpi  26889  log2cnv  26891  log2tlbnd  26892  birthdaylem2  26899  birthdaylem3  26900  amgmlem  26937  amgm  26938  emcllem5  26947  fsumharmonic  26959  zetacvg  26962  dmgmdivn0  26975  lgamgulmlem3  26978  lgamgulmlem4  26979  lgamgulmlem5  26980  lgamgulmlem6  26981  lgamgulm2  26983  lgamcvg2  27002  gamcvg  27003  gamcvg2lem  27006  facgam  27013  wilthlem1  27015  wilthlem2  27016  wilthlem3  27017  wilthimp  27019  basellem1  27028  basellem2  27029  basellem3  27030  basellem4  27031  basellem5  27032  basellem8  27035  vmaprm  27064  sgmval2  27090  0sgm  27091  sgmf  27092  vma1  27113  fsumdvdsdiaglem  27130  dvdsflf1o  27134  muinv  27140  mpodvdsmulf1o  27141  dvdsmulf1o  27143  sgmppw  27145  1sgmprm  27147  1sgm2ppw  27148  sgmmul  27149  chtublem  27159  fsumvma2  27162  chpchtsum  27167  logfaclbnd  27170  logexprlim  27173  mersenne  27175  perfect1  27176  perfectlem1  27177  perfectlem2  27178  perfect  27179  dchrsum2  27216  dchrhash  27219  bcmono  27225  bcp1ctr  27227  bclbnd  27228  bposlem1  27232  bposlem2  27233  bposlem3  27234  bposlem5  27236  bposlem6  27237  lgsval2lem  27255  lgsqrlem2  27295  gausslemma2dlem6  27320  gausslemma2dlem7  27321  gausslemma2d  27322  lgseisenlem1  27323  lgseisenlem4  27326  lgsquadlem1  27328  lgsquadlem2  27329  lgsquadlem3  27330  lgsquad2  27334  m1lgs  27336  2sqlem3  27368  2sqlem4  27369  chebbnd1lem1  27417  chebbnd1  27420  rplogsumlem1  27432  rplogsumlem2  27433  rpvmasumlem  27435  dchrisumlem1  27437  dchrmusum2  27442  dchrvmasumlem1  27443  dchrvmasum2lem  27444  dchrvmasum2if  27445  dchrvmasumlem2  27446  dchrvmasumlem3  27447  dchrvmasumiflem1  27449  dchrisum0flblem1  27456  dchrisum0flblem2  27457  dchrisum0fno1  27459  rpvmasum2  27460  rplogsum  27475  mulogsumlem  27479  mulogsum  27480  mulog2sumlem2  27483  vmalogdivsum2  27486  vmalogdivsum  27487  2vmadivsumlem  27488  logsqvma  27490  selberglem2  27494  selberglem3  27495  selberg  27496  selberg2lem  27498  logdivbnd  27504  selberg3lem1  27505  selberg4lem1  27508  pntrsumo1  27513  pntrsumbnd2  27515  selberg3r  27517  selberg4r  27518  selberg34r  27519  pntsval2  27524  pntrlog2bndlem2  27526  pntrlog2bndlem4  27528  pntrlog2bndlem6  27531  pntpbnd1  27534  pntpbnd2  27535  pntlemg  27546  pntlemn  27548  pntlemf  27553  pnt  27562  padicabvf  27579  ostth2lem2  27582  ostth3  27586  fusgrhashclwwlkn  30070  eucrct2eupth  30236  nrt2irr  30464  elq2  32805  numdenneg  32808  ltesubnnd  32816  2exple2exp  32839  oexpled  32841  1arithidomlem2  33512  1arithidom  33513  zringfrac  33530  cos9thpiminplylem1  33806  cos9thpiminplylem2  33807  1smat1  33828  madjusmdetlem2  33852  madjusmdetlem4  33854  qqhnm  34014  oddpwdc  34378  eulerpartlemsv2  34382  eulerpartlems  34384  eulerpartlemsv3  34385  eulerpartlemgc  34386  eulerpartlemv  34388  eulerpartlemgs2  34404  fibp1  34425  ballotlemfc0  34517  ballotlemfcc  34518  signsvtn0  34594  reprpmtf1o  34650  vtscl  34662  hgt750lemb  34680  tgoldbachgt  34687  subfacp1lem1  35234  subfacp1lem5  35239  subfacval2  35242  subfaclim  35243  cvmliftlem2  35341  cvmliftlem7  35346  cvmliftlem10  35349  cvmliftlem11  35350  cvmliftlem13  35351  bcm1nt  35792  bcprod  35793  iprodgam  35797  faclimlem1  35798  faclimlem2  35799  faclim2  35803  nn0prpwlem  36377  nn0prpw  36378  knoppcnlem10  36557  knoppndvlem16  36582  poimirlem1  37671  poimirlem2  37672  poimirlem6  37676  poimirlem7  37677  poimirlem8  37678  poimirlem9  37679  poimirlem10  37680  poimirlem11  37681  poimirlem12  37682  poimirlem13  37683  poimirlem15  37685  poimirlem16  37686  poimirlem17  37687  poimirlem18  37688  poimirlem19  37689  poimirlem20  37690  poimirlem21  37691  poimirlem22  37692  poimirlem23  37693  poimirlem24  37694  poimirlem25  37695  poimirlem26  37696  poimirlem27  37697  poimirlem31  37701  nnproddivdvdsd  42103  lcmfunnnd  42115  lcmineqlem3  42134  lcmineqlem4  42135  lcmineqlem6  42137  lcmineqlem8  42139  lcmineqlem10  42141  lcmineqlem11  42142  lcmineqlem12  42143  lcmineqlem16  42147  lcmineqlem18  42149  lcmineqlem23  42154  dvrelogpow2b  42171  aks4d1p1p2  42173  aks4d1p1  42179  aks4d1p8  42190  primrootsunit1  42200  primrootscoprmpow  42202  posbezout  42203  primrootscoprbij  42205  primrootspoweq0  42209  aks6d1c1p3  42213  aks6d1c1p8  42218  aks6d1c2p2  42222  hashscontpow1  42224  2np3bcnp1  42247  2ap1caineq  42248  sticksstones10  42258  sticksstones12a  42260  sticksstones16  42265  sticksstones22  42271  bcled  42281  bcle2d  42282  aks6d1c7lem1  42283  aks6d1c7  42287  unitscyglem2  42299  unitscyglem4  42301  unitscyglem5  42302  aks5lem8  42304  nnadddir  42378  nnmul1com  42379  nnmulcom  42380  oddnumth  42419  nicomachus  42420  zaddcom  42572  fltabcoprmex  42747  fltaccoprm  42748  fltbccoprm  42749  fltne  42752  flt4lem3  42756  flt4lem5elem  42759  flt4lem5a  42760  flt4lem5b  42761  flt4lem5c  42762  flt4lem5d  42763  flt4lem5e  42764  flt4lem5f  42765  flt4lem6  42766  flt4lem7  42767  nna4b4nsq  42768  fltltc  42769  fltnltalem  42770  fltnlta  42771  irrapxlem4  42932  irrapxlem5  42933  pellexlem2  42937  pellexlem6  42941  pell1234qrne0  42960  pell1234qrreccl  42961  pell1234qrmulcl  42962  pell1234qrdich  42968  pell14qrdich  42976  pell1qrge1  42977  pell1qr1  42978  pell14qrgapw  42983  rmxyneg  43027  rmxm1  43041  rmxluc  43043  rmxdbl  43046  jm2.19lem1  43096  jm2.27c  43114  relexpmulnn  43816  relexpmulg  43817  inductionexd  44262  hashnzfzclim  44429  bcccl  44446  bcc0  44447  bccp1k  44448  bccm1k  44449  binomcxplemwb  44455  fsumnncl  45686  mccllem  45711  clim1fr1  45715  sumnnodd  45744  dvsinexp  46023  dvxpaek  46052  dvnxpaek  46054  dvnprodlem2  46059  itgsinexplem1  46066  itgsinexp  46067  stoweidlem1  46113  stoweidlem11  46123  stoweidlem25  46137  stoweidlem26  46138  stoweidlem34  46146  stoweidlem37  46149  stoweidlem38  46150  stoweidlem42  46154  wallispi2lem1  46183  wallispi2  46185  stirlinglem4  46189  stirlinglem5  46190  stirlinglem10  46195  stirlinglem15  46200  dirkertrigeqlem3  46212  dirkertrigeq  46213  dirkercncflem2  46216  dirkercncflem4  46218  fourierdlem11  46230  fourierdlem15  46234  fourierdlem79  46297  fourierdlem83  46301  sqwvfourb  46341  etransclem14  46360  etransclem15  46361  etransclem20  46366  etransclem21  46367  etransclem22  46368  etransclem23  46369  etransclem24  46370  etransclem25  46371  etransclem28  46374  etransclem31  46377  etransclem32  46378  etransclem33  46379  etransclem34  46380  etransclem35  46381  etransclem38  46384  etransclem41  46387  etransclem44  46390  etransclem45  46391  etransclem47  46393  etransclem48  46394  nnfoctbdjlem  46567  deccarry  47425  iccpartgtprec  47534  fmtnoodd  47647  fmtnorec2lem  47656  fmtnorec2  47657  fmtnodvds  47658  goldbachthlem2  47660  fmtnorec3  47662  fmtnorec4  47663  fmtnoprmfac1lem  47678  fmtnoprmfac1  47679  fmtnoprmfac2lem1  47680  fmtnoprmfac2  47681  2pwp1prm  47703  sfprmdvdsmersenne  47717  lighneallem4b  47723  lighneal  47725  proththdlem  47727  proththd  47728  oexpnegALTV  47791  perfectALTVlem1  47835  perfectALTVlem2  47836  perfectALTV  47837  nnpw2pmod  48698  nnolog2flm1  48705  blennn0em1  48706  blengt1fldiv2p1  48708  nn0sumshdiglemB  48735  amgmlemALT  49918