Theorem nncnd 12188

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℂcc 11034  ℕcn 12172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685  ax-1cn 11094  ax-addcl 11096

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-nn 12173

This theorem is referenced by:  nnadddir  12231  nnmul1com  12232  nnmulcom  12233  nneo  12611  facdiv  14247  facndiv  14248  faclbnd  14250  faclbnd5  14258  faclbnd6  14259  facubnd  14260  facavg  14261  bccmpl  14269  bcn0  14270  bcn1  14273  bcm1k  14275  bcp1n  14276  bcp1nk  14277  bcval5  14278  bcpasc  14281  permnn  14286  hashf1  14417  hashfac  14418  relexpaddnn  15011  binom11  15795  binom1dif  15796  climcndslem2  15813  arisum2  15824  trireciplem  15825  trirecip  15826  geo2sum  15836  geo2lim  15838  fprodfac  15936  risefacfac  15998  fallfacfwd  15999  fallfacval4  16006  bcfallfac  16007  fallfacfac  16008  bpolycl  16015  bpolysum  16016  bpolydiflem  16017  fsumkthpow  16019  eftcl  16036  eftabs  16038  efcllem  16040  ege2le3  16053  efcj  16055  efaddlem  16056  eftlub  16074  eirrlem  16169  sqrt2irrlem  16213  oexpneg  16312  pwp1fsum  16358  bitsp1  16398  bitsfzolem  16401  bitsfzo  16402  bitsmod  16403  bitscmp  16405  bitsinv1lem  16408  bitsinv1  16409  2ebits  16414  bitsinvp1  16416  sadcaddlem  16424  sadadd3  16428  bitsres  16440  bitsuz  16441  bitsshft  16442  dvdsgcdidd  16504  mulgcd  16515  rplpwr  16525  sqgcd  16529  expgcd  16530  nn0expgcd  16531  lcmgcdlem  16573  3lcm2e6woprm  16582  coprmprod  16628  coprmproddvdslem  16629  cncongr1  16634  cncongr2  16635  prmind2  16652  isprm5  16675  divgcdodd  16678  prmdvdsexpr  16685  qmuldeneqnum  16715  divnumden  16716  qnumgt0  16718  numdensq  16722  numdenexp  16728  hashdvds  16743  phiprmpw  16744  prmdiv  16753  prmdivdiv  16755  phisum  16759  modprm0  16774  pythagtriplem4  16788  pythagtriplem6  16790  pythagtriplem7  16791  pythagtriplem14  16797  pythagtriplem15  16798  pythagtriplem19  16802  pythagtrip  16803  pcprendvds2  16810  pcpre1  16811  pcpremul  16812  pceulem  16814  pcdiv  16821  pcqmul  16822  pcelnn  16839  pcid  16842  pc2dvds  16848  dvdsprmpweqnn  16854  dvdsprmpweqle  16855  pcaddlem  16857  pcadd  16858  pcfaclem  16867  qexpz  16870  expnprm  16871  oddprmdvds  16872  prmpwdvds  16873  pockthlem  16874  pockthg  16875  infpnlem1  16879  prmreclem1  16885  prmreclem2  16886  prmreclem3  16887  prmreclem4  16888  prmreclem6  16890  4sqlem6  16912  4sqlem7  16913  4sqlem10  16916  mul4sqlem  16922  4sqlem11  16924  4sqlem12  16925  4sqlem14  16927  4sqlem17  16930  4sqlem18  16931  vdwlem1  16950  vdwlem2  16951  vdwlem3  16952  vdwlem5  16954  vdwlem6  16955  vdwlem8  16957  vdwlem9  16958  vdwlem10  16959  vdwlem12  16961  ramub1lem2  16996  ramcl  16998  prmop1  17007  prmdvdsprmo  17011  prmgaplem7  17026  prmgaplem8  17027  chnub  18586  gsumsgrpccat  18806  mulgnndir  19077  mulgnnass  19083  psgnunilem5  19467  odf1o2  19546  pgp0  19569  sylow1lem1  19571  odcau  19577  sylow2blem3  19595  sylow3lem3  19602  sylow3lem4  19603  gexexlem  19825  ablfacrp2  20042  ablfac1lem  20043  ablfac1eu  20048  pgpfac1lem3a  20051  pgpfac1lem3  20052  fincygsubgodexd  20088  zringlpirlem3  21446  znrrg  21547  psdpw  22165  cpmadugsumlemF  22866  lebnumlem3  24955  ovollb2lem  25480  ovolunlem1a  25488  ovolunlem1  25489  uniioombllem3  25577  uniioombllem4  25578  dyaddisjlem  25587  mbfi1fseqlem3  25709  mbfi1fseqlem4  25710  itgpowd  26042  dgrcolem1  26263  vieta1lem1  26301  vieta1lem2  26302  elqaalem2  26311  elqaalem3  26312  aalioulem1  26323  aaliou3lem2  26334  aaliou3lem8  26336  aaliou3lem6  26339  aaliou3lem9  26341  taylfvallem1  26347  tayl0  26352  taylply2  26358  taylply  26359  dvtaylp  26360  taylthlem1  26363  taylthlem2  26364  pserdvlem2  26418  advlogexp  26644  cxpmul2  26678  cxpeq  26746  rtprmirr  26749  atantayl3  26928  leibpi  26931  log2cnv  26933  log2tlbnd  26934  birthdaylem2  26941  birthdaylem3  26942  amgmlem  26978  amgm  26979  emcllem5  26988  fsumharmonic  27000  zetacvg  27003  dmgmdivn0  27016  lgamgulmlem3  27019  lgamgulmlem4  27020  lgamgulmlem5  27021  lgamgulmlem6  27022  lgamgulm2  27024  lgamcvg2  27043  gamcvg  27044  gamcvg2lem  27047  facgam  27054  wilthlem1  27056  wilthlem2  27057  wilthlem3  27058  wilthimp  27060  basellem1  27069  basellem2  27070  basellem3  27071  basellem4  27072  basellem5  27073  basellem8  27076  vmaprm  27105  sgmval2  27131  0sgm  27132  sgmf  27133  vma1  27154  fsumdvdsdiaglem  27171  dvdsflf1o  27175  muinv  27181  mpodvdsmulf1o  27182  dvdsmulf1o  27184  sgmppw  27185  1sgmprm  27187  1sgm2ppw  27188  sgmmul  27189  chtublem  27199  fsumvma2  27202  chpchtsum  27207  logfaclbnd  27210  logexprlim  27213  mersenne  27215  perfect1  27216  perfectlem1  27217  perfectlem2  27218  perfect  27219  dchrsum2  27256  dchrhash  27259  bcmono  27265  bcp1ctr  27267  bclbnd  27268  bposlem1  27272  bposlem2  27273  bposlem3  27274  bposlem5  27276  bposlem6  27277  lgsval2lem  27295  lgsqrlem2  27335  gausslemma2dlem6  27360  gausslemma2dlem7  27361  gausslemma2d  27362  lgseisenlem1  27363  lgseisenlem4  27366  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  lgsquad2  27374  m1lgs  27376  2sqlem3  27408  2sqlem4  27409  chebbnd1lem1  27457  chebbnd1  27460  rplogsumlem1  27472  rplogsumlem2  27473  rpvmasumlem  27475  dchrisumlem1  27477  dchrmusum2  27482  dchrvmasumlem1  27483  dchrvmasum2lem  27484  dchrvmasum2if  27485  dchrvmasumlem2  27486  dchrvmasumlem3  27487  dchrvmasumiflem1  27489  dchrisum0flblem1  27496  dchrisum0flblem2  27497  dchrisum0fno1  27499  rpvmasum2  27500  rplogsum  27515  mulogsumlem  27519  mulogsum  27520  mulog2sumlem2  27523  vmalogdivsum2  27526  vmalogdivsum  27527  2vmadivsumlem  27528  logsqvma  27530  selberglem2  27534  selberglem3  27535  selberg  27536  selberg2lem  27538  logdivbnd  27544  selberg3lem1  27545  selberg4lem1  27548  pntrsumo1  27553  pntrsumbnd2  27555  selberg3r  27557  selberg4r  27558  selberg34r  27559  pntsval2  27564  pntrlog2bndlem2  27566  pntrlog2bndlem4  27568  pntrlog2bndlem6  27571  pntpbnd1  27574  pntpbnd2  27575  pntlemg  27586  pntlemn  27588  pntlemf  27593  pnt  27602  padicabvf  27619  ostth2lem2  27622  ostth3  27626  fusgrhashclwwlkn  30174  eucrct2eupth  30340  nrt2irr  30568  elq2  32911  numdenneg  32914  ltesubnnd  32922  2exple2exp  32944  oexpled  32946  gsummptp1  33145  1arithidomlem2  33626  1arithidom  33627  zringfrac  33644  cos9thpiminplylem1  33973  cos9thpiminplylem2  33974  1smat1  33995  madjusmdetlem2  34019  madjusmdetlem4  34021  qqhnm  34181  oddpwdc  34545  eulerpartlemsv2  34549  eulerpartlems  34551  eulerpartlemsv3  34552  eulerpartlemgc  34553  eulerpartlemv  34555  eulerpartlemgs2  34571  fibp1  34592  ballotlemfc0  34684  ballotlemfcc  34685  signsvtn0  34761  reprpmtf1o  34817  vtscl  34829  hgt750lemb  34847  tgoldbachgt  34854  subfacp1lem1  35408  subfacp1lem5  35413  subfacval2  35416  subfaclim  35417  cvmliftlem2  35515  cvmliftlem7  35520  cvmliftlem10  35523  cvmliftlem11  35524  cvmliftlem13  35525  bcm1nt  35966  bcprod  35967  iprodgam  35971  faclimlem1  35972  faclimlem2  35973  faclim2  35977  nn0prpwlem  36551  nn0prpw  36552  knoppcnlem10  36809  knoppndvlem16  36834  poimirlem1  37989  poimirlem2  37990  poimirlem6  37994  poimirlem7  37995  poimirlem8  37996  poimirlem9  37997  poimirlem10  37998  poimirlem11  37999  poimirlem12  38000  poimirlem13  38001  poimirlem15  38003  poimirlem16  38004  poimirlem17  38005  poimirlem18  38006  poimirlem19  38007  poimirlem20  38008  poimirlem21  38009  poimirlem22  38010  poimirlem23  38011  poimirlem24  38012  poimirlem25  38013  poimirlem26  38014  poimirlem27  38015  poimirlem31  38019  nnproddivdvdsd  42486  lcmfunnnd  42498  lcmineqlem3  42517  lcmineqlem4  42518  lcmineqlem6  42520  lcmineqlem8  42522  lcmineqlem10  42524  lcmineqlem11  42525  lcmineqlem12  42526  lcmineqlem16  42530  lcmineqlem18  42532  lcmineqlem23  42537  dvrelogpow2b  42554  aks4d1p1p2  42556  aks4d1p1  42562  aks4d1p8  42573  primrootsunit1  42583  primrootscoprmpow  42585  posbezout  42586  primrootscoprbij  42588  primrootspoweq0  42592  aks6d1c1p3  42596  aks6d1c1p8  42601  aks6d1c2p2  42605  hashscontpow1  42607  2np3bcnp1  42630  2ap1caineq  42631  sticksstones10  42641  sticksstones12a  42643  sticksstones16  42648  sticksstones22  42654  bcled  42664  bcle2d  42665  aks6d1c7lem1  42666  aks6d1c7  42670  unitscyglem2  42682  unitscyglem4  42684  unitscyglem5  42685  aks5lem8  42687  oddnumth  42789  nicomachus  42790  zaddcom  42955  fltabcoprmex  43090  fltaccoprm  43091  fltbccoprm  43092  fltne  43095  flt4lem3  43099  flt4lem5elem  43102  flt4lem5a  43103  flt4lem5b  43104  flt4lem5c  43105  flt4lem5d  43106  flt4lem5e  43107  flt4lem5f  43108  flt4lem6  43109  flt4lem7  43110  nna4b4nsq  43111  fltltc  43112  fltnltalem  43113  fltnlta  43114  irrapxlem4  43271  irrapxlem5  43272  pellexlem2  43276  pellexlem6  43280  pell1234qrne0  43299  pell1234qrreccl  43300  pell1234qrmulcl  43301  pell1234qrdich  43307  pell14qrdich  43315  pell1qrge1  43316  pell1qr1  43317  pell14qrgapw  43322  rmxyneg  43366  rmxm1  43380  rmxluc  43382  rmxdbl  43385  jm2.19lem1  43435  jm2.27c  43453  relexpmulnn  44154  relexpmulg  44155  inductionexd  44600  hashnzfzclim  44767  bcccl  44784  bcc0  44785  bccp1k  44786  bccm1k  44787  binomcxplemwb  44793  fsumnncl  46018  mccllem  46043  clim1fr1  46047  sumnnodd  46076  dvsinexp  46355  dvxpaek  46384  dvnxpaek  46386  dvnprodlem2  46391  itgsinexplem1  46398  itgsinexp  46399  stoweidlem1  46445  stoweidlem11  46455  stoweidlem25  46469  stoweidlem26  46470  stoweidlem34  46478  stoweidlem37  46481  stoweidlem38  46482  stoweidlem42  46486  wallispi2lem1  46515  wallispi2  46517  stirlinglem4  46521  stirlinglem5  46522  stirlinglem10  46527  stirlinglem15  46532  dirkertrigeqlem3  46544  dirkertrigeq  46545  dirkercncflem2  46548  dirkercncflem4  46550  fourierdlem11  46562  fourierdlem15  46566  fourierdlem79  46629  fourierdlem83  46633  sqwvfourb  46673  etransclem14  46692  etransclem15  46693  etransclem20  46698  etransclem21  46699  etransclem22  46700  etransclem23  46701  etransclem24  46702  etransclem25  46703  etransclem28  46706  etransclem31  46709  etransclem32  46710  etransclem33  46711  etransclem34  46712  etransclem35  46713  etransclem38  46716  etransclem41  46719  etransclem44  46722  etransclem45  46723  etransclem47  46725  etransclem48  46726  nnfoctbdjlem  46899  deccarry  47775  iccpartgtprec  47896  fmtnoodd  48012  fmtnorec2lem  48021  fmtnorec2  48022  fmtnodvds  48023  goldbachthlem2  48025  fmtnorec3  48027  fmtnorec4  48028  fmtnoprmfac1lem  48043  fmtnoprmfac1  48044  fmtnoprmfac2lem1  48045  fmtnoprmfac2  48046  2pwp1prm  48068  sfprmdvdsmersenne  48082  lighneallem4b  48088  lighneal  48090  proththdlem  48092  proththd  48093  ppivalnnprm  48104  oexpnegALTV  48169  perfectALTVlem1  48213  perfectALTVlem2  48214  perfectALTV  48215  nnpw2pmod  49075  nnolog2flm1  49082  blennn0em1  49083  blengt1fldiv2p1  49085  nn0sumshdiglemB  49112  amgmlemALT  50294