Theorem nncnd 12190

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℂcc 11036  ℕcn 12174

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 5232  ax-nul 5242  ax-pr 5376  ax-un 7689  ax-1cn 11096  ax-addcl 11098

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 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6266  df-ord 6327  df-on 6328  df-lim 6329  df-suc 6330  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175

This theorem is referenced by:  nnadddir  12233  nnmul1com  12234  nnmulcom  12235  nneo  12613  facdiv  14249  facndiv  14250  faclbnd  14252  faclbnd5  14260  faclbnd6  14261  facubnd  14262  facavg  14263  bccmpl  14271  bcn0  14272  bcn1  14275  bcm1k  14277  bcp1n  14278  bcp1nk  14279  bcval5  14280  bcpasc  14283  permnn  14288  hashf1  14419  hashfac  14420  relexpaddnn  15013  binom11  15797  binom1dif  15798  climcndslem2  15815  arisum2  15826  trireciplem  15827  trirecip  15828  geo2sum  15838  geo2lim  15840  fprodfac  15938  risefacfac  16000  fallfacfwd  16001  fallfacval4  16008  bcfallfac  16009  fallfacfac  16010  bpolycl  16017  bpolysum  16018  bpolydiflem  16019  fsumkthpow  16021  eftcl  16038  eftabs  16040  efcllem  16042  ege2le3  16055  efcj  16057  efaddlem  16058  eftlub  16076  eirrlem  16171  sqrt2irrlem  16215  oexpneg  16314  pwp1fsum  16360  bitsp1  16400  bitsfzolem  16403  bitsfzo  16404  bitsmod  16405  bitscmp  16407  bitsinv1lem  16410  bitsinv1  16411  2ebits  16416  bitsinvp1  16418  sadcaddlem  16426  sadadd3  16430  bitsres  16442  bitsuz  16443  bitsshft  16444  dvdsgcdidd  16506  mulgcd  16517  rplpwr  16527  sqgcd  16531  expgcd  16532  nn0expgcd  16533  lcmgcdlem  16575  3lcm2e6woprm  16584  coprmprod  16630  coprmproddvdslem  16631  cncongr1  16636  cncongr2  16637  prmind2  16654  isprm5  16677  divgcdodd  16680  prmdvdsexpr  16687  qmuldeneqnum  16717  divnumden  16718  qnumgt0  16720  numdensq  16724  numdenexp  16730  hashdvds  16745  phiprmpw  16746  prmdiv  16755  prmdivdiv  16757  phisum  16761  modprm0  16776  pythagtriplem4  16790  pythagtriplem6  16792  pythagtriplem7  16793  pythagtriplem14  16799  pythagtriplem15  16800  pythagtriplem19  16804  pythagtrip  16805  pcprendvds2  16812  pcpre1  16813  pcpremul  16814  pceulem  16816  pcdiv  16823  pcqmul  16824  pcelnn  16841  pcid  16844  pc2dvds  16850  dvdsprmpweqnn  16856  dvdsprmpweqle  16857  pcaddlem  16859  pcadd  16860  pcfaclem  16869  qexpz  16872  expnprm  16873  oddprmdvds  16874  prmpwdvds  16875  pockthlem  16876  pockthg  16877  infpnlem1  16881  prmreclem1  16887  prmreclem2  16888  prmreclem3  16889  prmreclem4  16890  prmreclem6  16892  4sqlem6  16914  4sqlem7  16915  4sqlem10  16918  mul4sqlem  16924  4sqlem11  16926  4sqlem12  16927  4sqlem14  16929  4sqlem17  16932  4sqlem18  16933  vdwlem1  16952  vdwlem2  16953  vdwlem3  16954  vdwlem5  16956  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwlem10  16961  vdwlem12  16963  ramub1lem2  16998  ramcl  17000  prmop1  17009  prmdvdsprmo  17013  prmgaplem7  17028  prmgaplem8  17029  chnub  18588  gsumsgrpccat  18808  mulgnndir  19079  mulgnnass  19085  psgnunilem5  19469  odf1o2  19548  pgp0  19571  sylow1lem1  19573  odcau  19579  sylow2blem3  19597  sylow3lem3  19604  sylow3lem4  19605  gexexlem  19827  ablfacrp2  20044  ablfac1lem  20045  ablfac1eu  20050  pgpfac1lem3a  20053  pgpfac1lem3  20054  fincygsubgodexd  20090  zringlpirlem3  21444  znrrg  21545  psdpw  22136  cpmadugsumlemF  22841  lebnumlem3  24930  ovollb2lem  25455  ovolunlem1a  25463  ovolunlem1  25464  uniioombllem3  25552  uniioombllem4  25553  dyaddisjlem  25562  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  itgpowd  26017  dgrcolem1  26238  vieta1lem1  26276  vieta1lem2  26277  elqaalem2  26286  elqaalem3  26287  aalioulem1  26298  aaliou3lem2  26309  aaliou3lem8  26311  aaliou3lem6  26314  aaliou3lem9  26316  taylfvallem1  26322  tayl0  26327  taylply2  26333  taylply  26334  dvtaylp  26335  taylthlem1  26338  taylthlem2  26339  pserdvlem2  26393  advlogexp  26619  cxpmul2  26653  cxpeq  26721  rtprmirr  26724  atantayl3  26903  leibpi  26906  log2cnv  26908  log2tlbnd  26909  birthdaylem2  26916  birthdaylem3  26917  amgmlem  26953  amgm  26954  emcllem5  26963  fsumharmonic  26975  zetacvg  26978  dmgmdivn0  26991  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamgulm2  26999  lgamcvg2  27018  gamcvg  27019  gamcvg2lem  27022  facgam  27029  wilthlem1  27031  wilthlem2  27032  wilthlem3  27033  wilthimp  27035  basellem1  27044  basellem2  27045  basellem3  27046  basellem4  27047  basellem5  27048  basellem8  27051  vmaprm  27080  sgmval2  27106  0sgm  27107  sgmf  27108  vma1  27129  fsumdvdsdiaglem  27146  dvdsflf1o  27150  muinv  27156  mpodvdsmulf1o  27157  dvdsmulf1o  27159  sgmppw  27160  1sgmprm  27162  1sgm2ppw  27163  sgmmul  27164  chtublem  27174  fsumvma2  27177  chpchtsum  27182  logfaclbnd  27185  logexprlim  27188  mersenne  27190  perfect1  27191  perfectlem1  27192  perfectlem2  27193  perfect  27194  dchrsum2  27231  dchrhash  27234  bcmono  27240  bcp1ctr  27242  bclbnd  27243  bposlem1  27247  bposlem2  27248  bposlem3  27249  bposlem5  27251  bposlem6  27252  lgsval2lem  27270  lgsqrlem2  27310  gausslemma2dlem6  27335  gausslemma2dlem7  27336  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad2  27349  m1lgs  27351  2sqlem3  27383  2sqlem4  27384  chebbnd1lem1  27432  chebbnd1  27435  rplogsumlem1  27447  rplogsumlem2  27448  rpvmasumlem  27450  dchrisumlem1  27452  dchrmusum2  27457  dchrvmasumlem1  27458  dchrvmasum2lem  27459  dchrvmasum2if  27460  dchrvmasumlem2  27461  dchrvmasumlem3  27462  dchrvmasumiflem1  27464  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0fno1  27474  rpvmasum2  27475  rplogsum  27490  mulogsumlem  27494  mulogsum  27495  mulog2sumlem2  27498  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  logsqvma  27505  selberglem2  27509  selberglem3  27510  selberg  27511  selberg2lem  27513  logdivbnd  27519  selberg3lem1  27520  selberg4lem1  27523  pntrsumo1  27528  pntrsumbnd2  27530  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntsval2  27539  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  pntrlog2bndlem6  27546  pntpbnd1  27549  pntpbnd2  27550  pntlemg  27561  pntlemn  27563  pntlemf  27568  pnt  27577  padicabvf  27594  ostth2lem2  27597  ostth3  27601  fusgrhashclwwlkn  30149  eucrct2eupth  30315  nrt2irr  30543  elq2  32885  numdenneg  32888  ltesubnnd  32896  2exple2exp  32918  oexpled  32920  gsummptp1  33118  1arithidomlem2  33596  1arithidom  33597  zringfrac  33614  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  1smat1  33948  madjusmdetlem2  33972  madjusmdetlem4  33974  qqhnm  34134  oddpwdc  34498  eulerpartlemsv2  34502  eulerpartlems  34504  eulerpartlemsv3  34505  eulerpartlemgc  34506  eulerpartlemv  34508  eulerpartlemgs2  34524  fibp1  34545  ballotlemfc0  34637  ballotlemfcc  34638  signsvtn0  34714  reprpmtf1o  34770  vtscl  34782  hgt750lemb  34800  tgoldbachgt  34807  subfacp1lem1  35361  subfacp1lem5  35366  subfacval2  35369  subfaclim  35370  cvmliftlem2  35468  cvmliftlem7  35473  cvmliftlem10  35476  cvmliftlem11  35477  cvmliftlem13  35478  bcm1nt  35919  bcprod  35920  iprodgam  35924  faclimlem1  35925  faclimlem2  35926  faclim2  35930  nn0prpwlem  36504  nn0prpw  36505  knoppcnlem10  36762  knoppndvlem16  36787  poimirlem1  37942  poimirlem2  37943  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  nnproddivdvdsd  42439  lcmfunnnd  42451  lcmineqlem3  42470  lcmineqlem4  42471  lcmineqlem6  42473  lcmineqlem8  42475  lcmineqlem10  42477  lcmineqlem11  42478  lcmineqlem12  42479  lcmineqlem16  42483  lcmineqlem18  42485  lcmineqlem23  42490  dvrelogpow2b  42507  aks4d1p1p2  42509  aks4d1p1  42515  aks4d1p8  42526  primrootsunit1  42536  primrootscoprmpow  42538  posbezout  42539  primrootscoprbij  42541  primrootspoweq0  42545  aks6d1c1p3  42549  aks6d1c1p8  42554  aks6d1c2p2  42558  hashscontpow1  42560  2np3bcnp1  42583  2ap1caineq  42584  sticksstones10  42594  sticksstones12a  42596  sticksstones16  42601  sticksstones22  42607  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  aks6d1c7  42623  unitscyglem2  42635  unitscyglem4  42637  unitscyglem5  42638  aks5lem8  42640  oddnumth  42743  nicomachus  42744  zaddcom  42909  fltabcoprmex  43072  fltaccoprm  43073  fltbccoprm  43074  fltne  43077  flt4lem3  43081  flt4lem5elem  43084  flt4lem5a  43085  flt4lem5b  43086  flt4lem5c  43087  flt4lem5d  43088  flt4lem5e  43089  flt4lem5f  43090  flt4lem6  43091  flt4lem7  43092  nna4b4nsq  43093  fltltc  43094  fltnltalem  43095  fltnlta  43096  irrapxlem4  43253  irrapxlem5  43254  pellexlem2  43258  pellexlem6  43262  pell1234qrne0  43281  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell1234qrdich  43289  pell14qrdich  43297  pell1qrge1  43298  pell1qr1  43299  pell14qrgapw  43304  rmxyneg  43348  rmxm1  43362  rmxluc  43364  rmxdbl  43367  jm2.19lem1  43417  jm2.27c  43435  relexpmulnn  44136  relexpmulg  44137  inductionexd  44582  hashnzfzclim  44749  bcccl  44766  bcc0  44767  bccp1k  44768  bccm1k  44769  binomcxplemwb  44775  fsumnncl  46002  mccllem  46027  clim1fr1  46031  sumnnodd  46060  dvsinexp  46339  dvxpaek  46368  dvnxpaek  46370  dvnprodlem2  46375  itgsinexplem1  46382  itgsinexp  46383  stoweidlem1  46429  stoweidlem11  46439  stoweidlem25  46453  stoweidlem26  46454  stoweidlem34  46462  stoweidlem37  46465  stoweidlem38  46466  stoweidlem42  46470  wallispi2lem1  46499  wallispi2  46501  stirlinglem4  46505  stirlinglem5  46506  stirlinglem10  46511  stirlinglem15  46516  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem11  46546  fourierdlem15  46550  fourierdlem79  46613  fourierdlem83  46617  sqwvfourb  46657  etransclem14  46676  etransclem15  46677  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem23  46685  etransclem24  46686  etransclem25  46687  etransclem28  46690  etransclem31  46693  etransclem32  46694  etransclem33  46695  etransclem34  46696  etransclem35  46697  etransclem38  46700  etransclem41  46703  etransclem44  46706  etransclem45  46707  etransclem47  46709  etransclem48  46710  nnfoctbdjlem  46883  deccarry  47753  iccpartgtprec  47874  fmtnoodd  47990  fmtnorec2lem  47999  fmtnorec2  48000  fmtnodvds  48001  goldbachthlem2  48003  fmtnorec3  48005  fmtnorec4  48006  fmtnoprmfac1lem  48021  fmtnoprmfac1  48022  fmtnoprmfac2lem1  48023  fmtnoprmfac2  48024  2pwp1prm  48046  sfprmdvdsmersenne  48060  lighneallem4b  48066  lighneal  48068  proththdlem  48070  proththd  48071  ppivalnnprm  48082  oexpnegALTV  48147  perfectALTVlem1  48191  perfectALTVlem2  48192  perfectALTV  48193  nnpw2pmod  49053  nnolog2flm1  49060  blennn0em1  49061  blengt1fldiv2p1  49063  nn0sumshdiglemB  49090  amgmlemALT  50272