Theorem nncnd 11656

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 10537  ℕcn 11640

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-1cn 10597  ax-addcl 10599

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-om 7583  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-nn 11641

This theorem is referenced by:  facdiv  13650  facndiv  13651  faclbnd  13653  faclbnd5  13661  faclbnd6  13662  facubnd  13663  facavg  13664  bccmpl  13672  bcn0  13673  bcn1  13676  bcm1k  13678  bcp1n  13679  bcp1nk  13680  bcval5  13681  bcpasc  13684  permnn  13689  hashf1  13818  hashfac  13819  relexpaddnn  14412  binom11  15189  binom1dif  15190  climcndslem2  15207  arisum2  15218  trireciplem  15219  trirecip  15220  geo2sum  15231  geo2lim  15233  fprodfac  15329  risefacfac  15391  fallfacfwd  15392  fallfacval4  15399  bcfallfac  15400  fallfacfac  15401  bpolycl  15408  bpolysum  15409  bpolydiflem  15410  fsumkthpow  15412  eftcl  15429  eftabs  15431  efcllem  15433  ege2le3  15445  efcj  15447  efaddlem  15448  eftlub  15464  eirrlem  15559  sqrt2irrlem  15603  oexpneg  15696  pwp1fsum  15744  bitsp1  15782  bitsfzolem  15785  bitsfzo  15786  bitsmod  15787  bitscmp  15789  bitsinv1lem  15792  bitsinv1  15793  2ebits  15798  bitsinvp1  15800  sadcaddlem  15808  sadadd3  15812  bitsres  15824  bitsuz  15825  bitsshft  15826  dvdsgcdidd  15887  mulgcd  15898  rplpwr  15909  sqgcd  15911  lcmgcdlem  15952  3lcm2e6woprm  15961  coprmprod  16007  coprmproddvdslem  16008  cncongr1  16013  cncongr2  16014  prmind2  16031  isprm5  16053  divgcdodd  16056  prmdvdsexpr  16063  qmuldeneqnum  16089  divnumden  16090  qnumgt0  16092  numdensq  16096  hashdvds  16114  phiprmpw  16115  prmdiv  16124  prmdivdiv  16126  phisum  16129  modprm0  16144  pythagtriplem4  16158  pythagtriplem6  16160  pythagtriplem7  16161  pythagtriplem14  16167  pythagtriplem15  16168  pythagtriplem19  16172  pythagtrip  16173  pcprendvds2  16180  pcpre1  16181  pcpremul  16182  pceulem  16184  pcdiv  16191  pcqmul  16192  pcelnn  16208  pcid  16211  pc2dvds  16217  dvdsprmpweqnn  16223  dvdsprmpweqle  16224  pcaddlem  16226  pcadd  16227  pcfaclem  16236  qexpz  16239  expnprm  16240  oddprmdvds  16241  prmpwdvds  16242  pockthlem  16243  pockthg  16244  infpnlem1  16248  prmreclem1  16254  prmreclem2  16255  prmreclem3  16256  prmreclem4  16257  prmreclem6  16259  4sqlem6  16281  4sqlem7  16282  4sqlem10  16285  mul4sqlem  16291  4sqlem11  16293  4sqlem12  16294  4sqlem14  16296  4sqlem17  16299  4sqlem18  16300  vdwlem1  16319  vdwlem2  16320  vdwlem3  16321  vdwlem5  16323  vdwlem6  16324  vdwlem8  16326  vdwlem9  16327  vdwlem10  16328  vdwlem12  16330  ramub1lem2  16365  ramcl  16367  prmop1  16376  prmdvdsprmo  16380  prmgaplem7  16395  prmgaplem8  16396  gsumsgrpccat  18006  gsumccatOLD  18007  mulgnndir  18258  mulgnnass  18264  psgnunilem5  18624  odf1o2  18700  pgp0  18723  sylow1lem1  18725  odcau  18731  sylow2blem3  18749  sylow3lem3  18756  sylow3lem4  18757  gexexlem  18974  ablfacrp2  19191  ablfac1lem  19192  ablfac1eu  19197  pgpfac1lem3a  19200  pgpfac1lem3  19201  fincygsubgodexd  19237  zringlpirlem3  20635  znrrg  20714  cpmadugsumlemF  21486  lebnumlem3  23569  ovollb2lem  24091  ovolunlem1a  24099  ovolunlem1  24100  uniioombllem3  24188  uniioombllem4  24189  dyaddisjlem  24198  mbfi1fseqlem3  24320  mbfi1fseqlem4  24321  dgrcolem1  24865  vieta1lem1  24901  vieta1lem2  24902  elqaalem2  24911  elqaalem3  24912  aalioulem1  24923  aaliou3lem2  24934  aaliou3lem8  24936  aaliou3lem6  24939  aaliou3lem9  24941  taylfvallem1  24947  tayl0  24952  taylply2  24958  taylply  24959  dvtaylp  24960  taylthlem1  24963  taylthlem2  24964  pserdvlem2  25018  advlogexp  25240  cxpmul2  25274  cxpeq  25340  atantayl3  25519  leibpi  25522  log2cnv  25524  log2tlbnd  25525  birthdaylem2  25532  birthdaylem3  25533  amgmlem  25569  amgm  25570  emcllem5  25579  fsumharmonic  25591  zetacvg  25594  dmgmdivn0  25607  lgamgulmlem3  25610  lgamgulmlem4  25611  lgamgulmlem5  25612  lgamgulmlem6  25613  lgamgulm2  25615  lgamcvg2  25634  gamcvg  25635  gamcvg2lem  25638  facgam  25645  wilthlem1  25647  wilthlem2  25648  wilthlem3  25649  wilthimp  25651  basellem1  25660  basellem2  25661  basellem3  25662  basellem4  25663  basellem5  25664  basellem8  25667  vmaprm  25696  sgmval2  25722  0sgm  25723  sgmf  25724  vma1  25745  fsumdvdsdiaglem  25762  dvdsflf1o  25766  muinv  25772  dvdsmulf1o  25773  sgmppw  25775  1sgmprm  25777  1sgm2ppw  25778  sgmmul  25779  chtublem  25789  fsumvma2  25792  chpchtsum  25797  logfaclbnd  25800  logexprlim  25803  mersenne  25805  perfect1  25806  perfectlem1  25807  perfectlem2  25808  perfect  25809  dchrsum2  25846  dchrhash  25849  bcmono  25855  bcp1ctr  25857  bclbnd  25858  bposlem1  25862  bposlem2  25863  bposlem3  25864  bposlem5  25866  bposlem6  25867  lgsval2lem  25885  lgsqrlem2  25925  gausslemma2dlem6  25950  gausslemma2dlem7  25951  gausslemma2d  25952  lgseisenlem1  25953  lgseisenlem4  25956  lgsquadlem1  25958  lgsquadlem2  25959  lgsquadlem3  25960  lgsquad2  25964  m1lgs  25966  2sqlem3  25998  2sqlem4  25999  chebbnd1lem1  26047  chebbnd1  26050  rplogsumlem1  26062  rplogsumlem2  26063  rpvmasumlem  26065  dchrisumlem1  26067  dchrmusum2  26072  dchrvmasumlem1  26073  dchrvmasum2lem  26074  dchrvmasum2if  26075  dchrvmasumlem2  26076  dchrvmasumlem3  26077  dchrvmasumiflem1  26079  dchrisum0flblem1  26086  dchrisum0flblem2  26087  dchrisum0fno1  26089  rpvmasum2  26090  rplogsum  26105  mulogsumlem  26109  mulogsum  26110  mulog2sumlem2  26113  vmalogdivsum2  26116  vmalogdivsum  26117  2vmadivsumlem  26118  logsqvma  26120  selberglem2  26124  selberglem3  26125  selberg  26126  selberg2lem  26128  logdivbnd  26134  selberg3lem1  26135  selberg4lem1  26138  pntrsumo1  26143  pntrsumbnd2  26145  selberg3r  26147  selberg4r  26148  selberg34r  26149  pntsval2  26154  pntrlog2bndlem2  26156  pntrlog2bndlem4  26158  pntrlog2bndlem6  26161  pntpbnd1  26164  pntpbnd2  26165  pntlemg  26176  pntlemn  26178  pntlemf  26183  pnt  26192  padicabvf  26209  ostth2lem2  26212  ostth3  26216  fusgrhashclwwlkn  27860  eucrct2eupth  28026  numdenneg  30535  ltesubnnd  30540  1smat1  31071  madjusmdetlem2  31095  madjusmdetlem4  31097  qqhnm  31233  oddpwdc  31614  eulerpartlemsv2  31618  eulerpartlems  31620  eulerpartlemsv3  31621  eulerpartlemgc  31622  eulerpartlemv  31624  eulerpartlemgs2  31640  fibp1  31661  ballotlemfc0  31752  ballotlemfcc  31753  signsvtn0  31842  reprpmtf1o  31899  vtscl  31911  hgt750lemb  31929  tgoldbachgt  31936  subfacp1lem1  32428  subfacp1lem5  32433  subfacval2  32436  subfaclim  32437  cvmliftlem2  32535  cvmliftlem7  32540  cvmliftlem10  32543  cvmliftlem11  32544  cvmliftlem13  32545  bcm1nt  32971  bcprod  32972  iprodgam  32976  faclimlem1  32977  faclimlem2  32978  faclim2  32982  nn0prpwlem  33672  nn0prpw  33673  knoppndvlem16  33868  poimirlem1  34895  poimirlem2  34896  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem9  34903  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem13  34907  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  poimirlem31  34925  nnadddir  39170  nnmul1com  39171  nnmulcom  39172  expgcd  39190  nn0expgcd  39191  numdenexp  39193  fltne  39279  fltltc  39280  fltnltalem  39281  fltnlta  39282  irrapxlem4  39429  irrapxlem5  39430  pellexlem2  39434  pellexlem6  39438  pell1234qrne0  39457  pell1234qrreccl  39458  pell1234qrmulcl  39459  pell1234qrdich  39465  pell14qrdich  39473  pell1qrge1  39474  pell1qr1  39475  pell14qrgapw  39480  rmxyneg  39524  rmxm1  39538  rmxluc  39540  rmxdbl  39543  jm2.19lem1  39593  jm2.27c  39611  itgpowd  39828  relexpmulnn  40061  relexpmulg  40062  inductionexd  40512  hashnzfzclim  40661  bcccl  40678  bcc0  40679  bccp1k  40680  bccm1k  40681  binomcxplemwb  40687  fsumnncl  41859  mccllem  41885  clim1fr1  41889  sumnnodd  41918  dvsinexp  42202  dvxpaek  42232  dvnxpaek  42234  dvnprodlem2  42239  itgsinexplem1  42246  itgsinexp  42247  stoweidlem1  42293  stoweidlem11  42303  stoweidlem25  42317  stoweidlem26  42318  stoweidlem34  42326  stoweidlem37  42329  stoweidlem38  42330  stoweidlem42  42334  wallispi2lem1  42363  wallispi2  42365  stirlinglem4  42369  stirlinglem5  42370  stirlinglem10  42375  stirlinglem15  42380  dirkertrigeqlem3  42392  dirkertrigeq  42393  dirkercncflem2  42396  dirkercncflem4  42398  fourierdlem11  42410  fourierdlem15  42414  fourierdlem79  42477  fourierdlem83  42481  sqwvfourb  42521  etransclem14  42540  etransclem15  42541  etransclem20  42546  etransclem21  42547  etransclem22  42548  etransclem23  42549  etransclem24  42550  etransclem25  42551  etransclem28  42554  etransclem31  42557  etransclem32  42558  etransclem33  42559  etransclem34  42560  etransclem35  42561  etransclem38  42564  etransclem41  42567  etransclem44  42570  etransclem45  42571  etransclem47  42573  etransclem48  42574  nnfoctbdjlem  42744  deccarry  43518  iccpartgtprec  43587  fmtnoodd  43702  fmtnorec2lem  43711  fmtnorec2  43712  fmtnodvds  43713  goldbachthlem2  43715  fmtnorec3  43717  fmtnorec4  43718  fmtnoprmfac1lem  43733  fmtnoprmfac1  43734  fmtnoprmfac2lem1  43735  fmtnoprmfac2  43736  2pwp1prm  43758  sfprmdvdsmersenne  43775  lighneallem4b  43781  lighneal  43783  proththdlem  43785  proththd  43786  oexpnegALTV  43849  perfectALTVlem1  43893  perfectALTVlem2  43894  perfectALTV  43895  nnpw2pmod  44650  nnolog2flm1  44657  blennn0em1  44658  blengt1fldiv2p1  44660  nn0sumshdiglemB  44687  amgmlemALT  44911