Theorem nncnd 12179

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11025  ℕcn 12163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-un 7680  ax-1cn 11085  ax-addcl 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8222  df-wrecs 8253  df-recs 8302  df-rdg 8340  df-nn 12164

This theorem is referenced by:  nnadddir  12222  nnmul1com  12223  nnmulcom  12224  nneo  12602  facdiv  14238  facndiv  14239  faclbnd  14241  faclbnd5  14249  faclbnd6  14250  facubnd  14251  facavg  14252  bccmpl  14260  bcn0  14261  bcn1  14264  bcm1k  14266  bcp1n  14267  bcp1nk  14268  bcval5  14269  bcpasc  14272  permnn  14277  hashf1  14408  hashfac  14409  relexpaddnn  15002  binom11  15786  binom1dif  15787  climcndslem2  15804  arisum2  15815  trireciplem  15816  trirecip  15817  geo2sum  15827  geo2lim  15829  fprodfac  15927  risefacfac  15989  fallfacfwd  15990  fallfacval4  15997  bcfallfac  15998  fallfacfac  15999  bpolycl  16006  bpolysum  16007  bpolydiflem  16008  fsumkthpow  16010  eftcl  16027  eftabs  16029  efcllem  16031  ege2le3  16044  efcj  16046  efaddlem  16047  eftlub  16065  eirrlem  16160  sqrt2irrlem  16204  oexpneg  16303  pwp1fsum  16349  bitsp1  16389  bitsfzolem  16392  bitsfzo  16393  bitsmod  16394  bitscmp  16396  bitsinv1lem  16399  bitsinv1  16400  2ebits  16405  bitsinvp1  16407  sadcaddlem  16415  sadadd3  16419  bitsres  16431  bitsuz  16432  bitsshft  16433  dvdsgcdidd  16495  mulgcd  16506  rplpwr  16516  sqgcd  16520  expgcd  16521  nn0expgcd  16522  lcmgcdlem  16564  3lcm2e6woprm  16573  coprmprod  16619  coprmproddvdslem  16620  cncongr1  16625  cncongr2  16626  prmind2  16643  isprm5  16666  divgcdodd  16669  prmdvdsexpr  16676  qmuldeneqnum  16706  divnumden  16707  qnumgt0  16709  numdensq  16713  numdenexp  16719  hashdvds  16734  phiprmpw  16735  prmdiv  16744  prmdivdiv  16746  phisum  16750  modprm0  16765  pythagtriplem4  16779  pythagtriplem6  16781  pythagtriplem7  16782  pythagtriplem14  16788  pythagtriplem15  16789  pythagtriplem19  16793  pythagtrip  16794  pcprendvds2  16801  pcpre1  16802  pcpremul  16803  pceulem  16805  pcdiv  16812  pcqmul  16813  pcelnn  16830  pcid  16833  pc2dvds  16839  dvdsprmpweqnn  16845  dvdsprmpweqle  16846  pcaddlem  16848  pcadd  16849  pcfaclem  16858  qexpz  16861  expnprm  16862  oddprmdvds  16863  prmpwdvds  16864  pockthlem  16865  pockthg  16866  infpnlem1  16870  prmreclem1  16876  prmreclem2  16877  prmreclem3  16878  prmreclem4  16879  prmreclem6  16881  4sqlem6  16903  4sqlem7  16904  4sqlem10  16907  mul4sqlem  16913  4sqlem11  16915  4sqlem12  16916  4sqlem14  16918  4sqlem17  16921  4sqlem18  16922  vdwlem1  16941  vdwlem2  16942  vdwlem3  16943  vdwlem5  16945  vdwlem6  16946  vdwlem8  16948  vdwlem9  16949  vdwlem10  16950  vdwlem12  16952  ramub1lem2  16987  ramcl  16989  prmop1  16998  prmdvdsprmo  17002  prmgaplem7  17017  prmgaplem8  17018  chnub  18577  gsumsgrpccat  18797  mulgnndir  19068  mulgnnass  19074  psgnunilem5  19458  odf1o2  19537  pgp0  19560  sylow1lem1  19562  odcau  19568  sylow2blem3  19586  sylow3lem3  19593  sylow3lem4  19594  gexexlem  19816  ablfacrp2  20033  ablfac1lem  20034  ablfac1eu  20039  pgpfac1lem3a  20042  pgpfac1lem3  20043  fincygsubgodexd  20079  zringlpirlem3  21452  znrrg  21553  psdpw  22145  cpmadugsumlemF  22850  lebnumlem3  24939  ovollb2lem  25464  ovolunlem1a  25472  ovolunlem1  25473  uniioombllem3  25561  uniioombllem4  25562  dyaddisjlem  25571  mbfi1fseqlem3  25693  mbfi1fseqlem4  25694  itgpowd  26029  dgrcolem1  26250  vieta1lem1  26289  vieta1lem2  26290  elqaalem2  26299  elqaalem3  26300  aalioulem1  26311  aaliou3lem2  26322  aaliou3lem8  26324  aaliou3lem6  26327  aaliou3lem9  26329  taylfvallem1  26335  tayl0  26340  taylply2  26346  taylply2OLD  26347  taylply  26348  dvtaylp  26349  taylthlem1  26352  taylthlem2  26353  taylthlem2OLD  26354  pserdvlem2  26409  advlogexp  26635  cxpmul2  26669  cxpeq  26738  rtprmirr  26741  atantayl3  26920  leibpi  26923  log2cnv  26925  log2tlbnd  26926  birthdaylem2  26933  birthdaylem3  26934  amgmlem  26971  amgm  26972  emcllem5  26981  fsumharmonic  26993  zetacvg  26996  dmgmdivn0  27009  lgamgulmlem3  27012  lgamgulmlem4  27013  lgamgulmlem5  27014  lgamgulmlem6  27015  lgamgulm2  27017  lgamcvg2  27036  gamcvg  27037  gamcvg2lem  27040  facgam  27047  wilthlem1  27049  wilthlem2  27050  wilthlem3  27051  wilthimp  27053  basellem1  27062  basellem2  27063  basellem3  27064  basellem4  27065  basellem5  27066  basellem8  27069  vmaprm  27098  sgmval2  27124  0sgm  27125  sgmf  27126  vma1  27147  fsumdvdsdiaglem  27164  dvdsflf1o  27168  muinv  27174  mpodvdsmulf1o  27175  dvdsmulf1o  27177  sgmppw  27179  1sgmprm  27181  1sgm2ppw  27182  sgmmul  27183  chtublem  27193  fsumvma2  27196  chpchtsum  27201  logfaclbnd  27204  logexprlim  27207  mersenne  27209  perfect1  27210  perfectlem1  27211  perfectlem2  27212  perfect  27213  dchrsum2  27250  dchrhash  27253  bcmono  27259  bcp1ctr  27261  bclbnd  27262  bposlem1  27266  bposlem2  27267  bposlem3  27268  bposlem5  27270  bposlem6  27271  lgsval2lem  27289  lgsqrlem2  27329  gausslemma2dlem6  27354  gausslemma2dlem7  27355  gausslemma2d  27356  lgseisenlem1  27357  lgseisenlem4  27360  lgsquadlem1  27362  lgsquadlem2  27363  lgsquadlem3  27364  lgsquad2  27368  m1lgs  27370  2sqlem3  27402  2sqlem4  27403  chebbnd1lem1  27451  chebbnd1  27454  rplogsumlem1  27466  rplogsumlem2  27467  rpvmasumlem  27469  dchrisumlem1  27471  dchrmusum2  27476  dchrvmasumlem1  27477  dchrvmasum2lem  27478  dchrvmasum2if  27479  dchrvmasumlem2  27480  dchrvmasumlem3  27481  dchrvmasumiflem1  27483  dchrisum0flblem1  27490  dchrisum0flblem2  27491  dchrisum0fno1  27493  rpvmasum2  27494  rplogsum  27509  mulogsumlem  27513  mulogsum  27514  mulog2sumlem2  27517  vmalogdivsum2  27520  vmalogdivsum  27521  2vmadivsumlem  27522  logsqvma  27524  selberglem2  27528  selberglem3  27529  selberg  27530  selberg2lem  27532  logdivbnd  27538  selberg3lem1  27539  selberg4lem1  27542  pntrsumo1  27547  pntrsumbnd2  27549  selberg3r  27551  selberg4r  27552  selberg34r  27553  pntsval2  27558  pntrlog2bndlem2  27560  pntrlog2bndlem4  27562  pntrlog2bndlem6  27565  pntpbnd1  27568  pntpbnd2  27569  pntlemg  27580  pntlemn  27582  pntlemf  27587  pnt  27596  padicabvf  27613  ostth2lem2  27616  ostth3  27620  fusgrhashclwwlkn  30169  eucrct2eupth  30335  nrt2irr  30563  elq2  32905  numdenneg  32908  ltesubnnd  32916  2exple2exp  32938  oexpled  32940  gsummptp1  33138  1arithidomlem2  33616  1arithidom  33617  zringfrac  33634  cos9thpiminplylem1  33947  cos9thpiminplylem2  33948  1smat1  33969  madjusmdetlem2  33993  madjusmdetlem4  33995  qqhnm  34155  oddpwdc  34519  eulerpartlemsv2  34523  eulerpartlems  34525  eulerpartlemsv3  34526  eulerpartlemgc  34527  eulerpartlemv  34529  eulerpartlemgs2  34545  fibp1  34566  ballotlemfc0  34658  ballotlemfcc  34659  signsvtn0  34735  reprpmtf1o  34791  vtscl  34803  hgt750lemb  34821  tgoldbachgt  34828  subfacp1lem1  35382  subfacp1lem5  35387  subfacval2  35390  subfaclim  35391  cvmliftlem2  35489  cvmliftlem7  35494  cvmliftlem10  35497  cvmliftlem11  35498  cvmliftlem13  35499  bcm1nt  35940  bcprod  35941  iprodgam  35945  faclimlem1  35946  faclimlem2  35947  faclim2  35951  nn0prpwlem  36525  nn0prpw  36526  knoppcnlem10  36775  knoppndvlem16  36800  poimirlem1  37953  poimirlem2  37954  poimirlem6  37958  poimirlem7  37959  poimirlem8  37960  poimirlem9  37961  poimirlem10  37962  poimirlem11  37963  poimirlem12  37964  poimirlem13  37965  poimirlem15  37967  poimirlem16  37968  poimirlem17  37969  poimirlem18  37970  poimirlem19  37971  poimirlem20  37972  poimirlem21  37973  poimirlem22  37974  poimirlem23  37975  poimirlem24  37976  poimirlem25  37977  poimirlem26  37978  poimirlem27  37979  poimirlem31  37983  nnproddivdvdsd  42450  lcmfunnnd  42462  lcmineqlem3  42481  lcmineqlem4  42482  lcmineqlem6  42484  lcmineqlem8  42486  lcmineqlem10  42488  lcmineqlem11  42489  lcmineqlem12  42490  lcmineqlem16  42494  lcmineqlem18  42496  lcmineqlem23  42501  dvrelogpow2b  42518  aks4d1p1p2  42520  aks4d1p1  42526  aks4d1p8  42537  primrootsunit1  42547  primrootscoprmpow  42549  posbezout  42550  primrootscoprbij  42552  primrootspoweq0  42556  aks6d1c1p3  42560  aks6d1c1p8  42565  aks6d1c2p2  42569  hashscontpow1  42571  2np3bcnp1  42594  2ap1caineq  42595  sticksstones10  42605  sticksstones12a  42607  sticksstones16  42612  sticksstones22  42618  bcled  42628  bcle2d  42629  aks6d1c7lem1  42630  aks6d1c7  42634  unitscyglem2  42646  unitscyglem4  42648  unitscyglem5  42649  aks5lem8  42651  oddnumth  42754  nicomachus  42755  zaddcom  42920  fltabcoprmex  43083  fltaccoprm  43084  fltbccoprm  43085  fltne  43088  flt4lem3  43092  flt4lem5elem  43095  flt4lem5a  43096  flt4lem5b  43097  flt4lem5c  43098  flt4lem5d  43099  flt4lem5e  43100  flt4lem5f  43101  flt4lem6  43102  flt4lem7  43103  nna4b4nsq  43104  fltltc  43105  fltnltalem  43106  fltnlta  43107  irrapxlem4  43268  irrapxlem5  43269  pellexlem2  43273  pellexlem6  43277  pell1234qrne0  43296  pell1234qrreccl  43297  pell1234qrmulcl  43298  pell1234qrdich  43304  pell14qrdich  43312  pell1qrge1  43313  pell1qr1  43314  pell14qrgapw  43319  rmxyneg  43363  rmxm1  43377  rmxluc  43379  rmxdbl  43382  jm2.19lem1  43432  jm2.27c  43450  relexpmulnn  44151  relexpmulg  44152  inductionexd  44597  hashnzfzclim  44764  bcccl  44781  bcc0  44782  bccp1k  44783  bccm1k  44784  binomcxplemwb  44790  fsumnncl  46017  mccllem  46042  clim1fr1  46046  sumnnodd  46075  dvsinexp  46354  dvxpaek  46383  dvnxpaek  46385  dvnprodlem2  46390  itgsinexplem1  46397  itgsinexp  46398  stoweidlem1  46444  stoweidlem11  46454  stoweidlem25  46468  stoweidlem26  46469  stoweidlem34  46477  stoweidlem37  46480  stoweidlem38  46481  stoweidlem42  46485  wallispi2lem1  46514  wallispi2  46516  stirlinglem4  46520  stirlinglem5  46521  stirlinglem10  46526  stirlinglem15  46531  dirkertrigeqlem3  46543  dirkertrigeq  46544  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem11  46561  fourierdlem15  46565  fourierdlem79  46628  fourierdlem83  46632  sqwvfourb  46672  etransclem14  46691  etransclem15  46692  etransclem20  46697  etransclem21  46698  etransclem22  46699  etransclem23  46700  etransclem24  46701  etransclem25  46702  etransclem28  46705  etransclem31  46708  etransclem32  46709  etransclem33  46710  etransclem34  46711  etransclem35  46712  etransclem38  46715  etransclem41  46718  etransclem44  46721  etransclem45  46722  etransclem47  46724  etransclem48  46725  nnfoctbdjlem  46898  deccarry  47756  iccpartgtprec  47877  fmtnoodd  47993  fmtnorec2lem  48002  fmtnorec2  48003  fmtnodvds  48004  goldbachthlem2  48006  fmtnorec3  48008  fmtnorec4  48009  fmtnoprmfac1lem  48024  fmtnoprmfac1  48025  fmtnoprmfac2lem1  48026  fmtnoprmfac2  48027  2pwp1prm  48049  sfprmdvdsmersenne  48063  lighneallem4b  48069  lighneal  48071  proththdlem  48073  proththd  48074  ppivalnnprm  48085  oexpnegALTV  48150  perfectALTVlem1  48194  perfectALTVlem2  48195  perfectALTV  48196  nnpw2pmod  49056  nnolog2flm1  49063  blennn0em1  49064  blengt1fldiv2p1  49066  nn0sumshdiglemB  49093  amgmlemALT  50275