Theorem nncnd 12267

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11116  ℕcn 12251

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745  ax-1cn 11176  ax-addcl 11178

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-nn 12252

This theorem is used by:  nnadddir  12310  nnmul1com  12311  nnmulcom  12312  nneo  12698  facdiv  14343  facndiv  14344  faclbnd  14346  faclbnd5  14354  faclbnd6  14355  facubnd  14356  facavg  14357  bccmpl  14365  bcn0  14366  bcn1  14369  bcm1k  14371  bcp1n  14372  bcp1nk  14373  bcval5  14374  bcpasc  14377  permnn  14382  hashf1  14514  hashfac  14515  relexpaddnn  15114  binom11  15912  binom1dif  15913  climcndslem2  15930  arisum2  15941  trireciplem  15942  trirecip  15943  geo2sum  15953  geo2lim  15955  fprodfac  16053  risefacfac  16114  fallfacfwd  16115  fallfacval4  16122  bcfallfac  16123  fallfacfac  16124  bpolycl  16131  bpolysum  16132  bpolydiflem  16133  fsumkthpow  16135  eftcl  16152  eftabs  16154  efcllem  16156  ege2le3  16169  efcj  16171  efaddlem  16172  eftlub  16190  eirrlem  16285  sqrt2irrlem  16329  oexpneg  16428  pwp1fsum  16474  bitsp1  16514  bitsfzolem  16517  bitsfzo  16518  bitsmod  16519  bitscmp  16521  bitsinv1lem  16524  bitsinv1  16525  2ebits  16530  bitsinvp1  16532  sadcaddlem  16540  sadadd3  16544  bitsres  16556  bitsuz  16557  bitsshft  16558  dvdsgcdidd  16620  mulgcd  16631  rplpwr  16641  sqgcd  16645  expgcd  16646  nn0expgcd  16647  lcmgcdlem  16689  3lcm2e6woprm  16698  coprmprod  16744  coprmproddvdslem  16745  cncongr1  16750  cncongr2  16751  prmind2  16768  isprm5  16791  divgcdodd  16794  prmdvdsexpr  16801  qmuldeneqnum  16831  divnumden  16832  qnumgt0  16834  numdensq  16838  numdenexp  16844  hashdvds  16859  phiprmpw  16860  prmdiv  16869  prmdivdiv  16871  phisum  16875  modprm0  16890  pythagtriplem4  16904  pythagtriplem6  16906  pythagtriplem7  16907  pythagtriplem14  16913  pythagtriplem15  16914  pythagtriplem19  16918  pythagtrip  16919  pcprendvds2  16926  pcpre1  16927  pcpremul  16928  pceulem  16930  pcdiv  16937  pcqmul  16938  pcelnn  16955  pcid  16958  pc2dvds  16964  dvdsprmpweqnn  16970  dvdsprmpweqle  16971  pcaddlem  16973  pcadd  16974  pcfaclem  16983  qexpz  16986  expnprm  16987  oddprmdvds  16988  prmpwdvds  16989  pockthlem  16990  pockthg  16991  infpnlem1  16995  prmreclem1  17001  prmreclem2  17002  prmreclem3  17003  prmreclem4  17004  prmreclem6  17006  4sqlem6  17028  4sqlem7  17029  4sqlem10  17032  mul4sqlem  17038  4sqlem11  17040  4sqlem12  17041  4sqlem14  17043  4sqlem17  17046  4sqlem18  17047  vdwlem1  17066  vdwlem2  17067  vdwlem3  17068  vdwlem5  17070  vdwlem6  17071  vdwlem8  17073  vdwlem9  17074  vdwlem10  17075  vdwlem12  17077  ramub1lem2  17112  ramcl  17114  prmop1  17123  prmdvdsprmo  17127  prmgaplem7  17142  prmgaplem8  17143  chnub  18703  gsumsgrpccat  18924  mulgnndir  19194  mulgnnass  19200  psgnunilem5  19589  odf1o2  19668  pgp0  19691  sylow1lem1  19693  odcau  19699  sylow2blem3  19717  sylow3lem3  19724  sylow3lem4  19725  gexexlem  19947  ablfacrp2  20164  ablfac1lem  20165  ablfac1eu  20170  pgpfac1lem3a  20173  pgpfac1lem3  20174  fincygsubgodexd  20210  zringlpirlem3  21644  znrrg  21745  psdpw  22363  cpmadugsumlemF  23063  lebnumlem3  25152  ovollb2lem  25677  ovolunlem1a  25685  ovolunlem1  25686  uniioombllem3  25774  uniioombllem4  25775  dyaddisjlem  25784  mbfi1fseqlem3  25906  mbfi1fseqlem4  25907  itgpowd  26239  dgrcolem1  26460  vieta1lem1  26501  vieta1lem2  26502  elqaalem2  26511  elqaalem3  26512  aalioulem1  26525  aaliou3lem2  26536  aaliou3lem8  26538  aaliou3lem6  26541  aaliou3lem9  26543  taylfvallem1  26550  tayl0  26555  taylply2  26561  taylply  26562  dvtaylp  26563  taylthlem1  26566  taylthlem2  26567  pserdvlem2  26621  advlogexp  26850  cxpmul2  26884  cxpeq  26952  rtprmirr  26955  atantayl3  27134  leibpi  27137  log2cnv  27139  log2tlbnd  27140  birthdaylem2  27147  birthdaylem3  27148  amgmlem  27184  amgm  27185  emcllem5  27194  fsumharmonic  27206  zetacvg  27209  dmgmdivn0  27222  lgamgulmlem3  27225  lgamgulmlem4  27226  lgamgulmlem5  27227  lgamgulmlem6  27228  lgamgulm2  27230  lgamcvg2  27249  gamcvg  27250  gamcvg2lem  27253  facgam  27260  wilthlem1  27262  wilthlem2  27263  wilthlem3  27264  wilthimp  27266  basellem1  27275  basellem2  27276  basellem3  27277  basellem4  27278  basellem5  27279  basellem8  27282  vmaprm  27311  sgmval2  27337  0sgm  27338  sgmf  27339  vma1  27360  fsumdvdsdiaglem  27377  dvdsflf1o  27381  muinv  27387  mpodvdsmulf1o  27388  dvdsmulf1o  27390  sgmppw  27391  1sgmprm  27393  1sgm2ppw  27394  sgmmul  27395  chtublem  27405  fsumvma2  27408  chpchtsum  27413  logfaclbnd  27416  logexprlim  27419  mersenne  27421  perfect1  27422  perfectlem1  27423  perfectlem2  27424  perfect  27425  dchrsum2  27462  dchrhash  27465  bcmono  27471  bcp1ctr  27473  bclbnd  27474  bposlem1  27478  bposlem2  27479  bposlem3  27480  bposlem5  27482  bposlem6  27483  lgsval2lem  27501  lgsqrlem2  27541  gausslemma2dlem6  27566  gausslemma2dlem7  27567  gausslemma2d  27568  lgseisenlem1  27569  lgseisenlem4  27572  lgsquadlem1  27574  lgsquadlem2  27575  lgsquadlem3  27576  lgsquad2  27580  m1lgs  27582  2sqlem3  27614  2sqlem4  27615  chebbnd1lem1  27663  chebbnd1  27666  rplogsumlem1  27678  rplogsumlem2  27679  rpvmasumlem  27681  dchrisumlem1  27683  dchrmusum2  27688  dchrvmasumlem1  27689  dchrvmasum2lem  27690  dchrvmasum2if  27691  dchrvmasumlem2  27692  dchrvmasumlem3  27693  dchrvmasumiflem1  27695  dchrisum0flblem1  27702  dchrisum0flblem2  27703  dchrisum0fno1  27705  rpvmasum2  27706  rplogsum  27721  mulogsumlem  27725  mulogsum  27726  mulog2sumlem2  27729  vmalogdivsum2  27732  vmalogdivsum  27733  2vmadivsumlem  27734  logsqvma  27736  selberglem2  27740  selberglem3  27741  selberg  27742  selberg2lem  27744  logdivbnd  27750  selberg3lem1  27751  selberg4lem1  27754  pntrsumo1  27759  pntrsumbnd2  27761  selberg3r  27763  selberg4r  27764  selberg34r  27765  pntsval2  27770  pntrlog2bndlem2  27772  pntrlog2bndlem4  27774  pntrlog2bndlem6  27777  pntpbnd1  27780  pntpbnd2  27781  pntlemg  27792  pntlemn  27794  pntlemf  27799  pnt  27808  padicabvf  27825  ostth2lem2  27828  ostth3  27832  fusgrhashclwwlkn  30460  eucrct2eupth  30626  nrt2irr  30854  elq2  33186  numdenneg  33189  ltesubnnd  33197  2exple2exp  33208  oexpled  33210  gsummptp1  33401  1arithidomlem2  33850  1arithidom  33851  zringfrac  33868  cos9thpiminplylem1  34196  cos9thpiminplylem2  34197  1smat1  34218  madjusmdetlem2  34242  madjusmdetlem4  34244  qqhnm  34404  oddpwdc  34768  eulerpartlemsv2  34772  eulerpartlems  34774  eulerpartlemsv3  34775  eulerpartlemgc  34776  eulerpartlemv  34778  eulerpartlemgs2  34794  fibp1  34815  ballotlemfc0  34907  ballotlemfcc  34908  signsvtn0  34981  reprpmtf1o  35037  vtscl  35049  hgt750lemb  35067  tgoldbachgt  35074  subfacp1lem1  35684  subfacp1lem5  35689  subfacval2  35692  subfaclim  35693  cvmliftlem2  35791  cvmliftlem7  35796  cvmliftlem10  35799  cvmliftlem11  35800  cvmliftlem13  35801  bcm1nt  36242  bcprod  36243  iprodgam  36247  faclimlem1  36248  faclimlem2  36249  faclim2  36253  nn0prpwlem  36866  nn0prpw  36867  knoppcnlem10  37124  knoppndvlem16  37149  poimirlem1  38305  poimirlem2  38306  poimirlem6  38310  poimirlem7  38311  poimirlem8  38312  poimirlem9  38313  poimirlem10  38314  poimirlem11  38315  poimirlem12  38316  poimirlem13  38317  poimirlem15  38319  poimirlem16  38320  poimirlem17  38321  poimirlem18  38322  poimirlem19  38323  poimirlem20  38324  poimirlem21  38325  poimirlem22  38326  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem26  38330  poimirlem27  38331  poimirlem31  38335  nnproddivdvdsd  42800  lcmfunnnd  42812  lcmineqlem3  42831  lcmineqlem4  42832  lcmineqlem6  42834  lcmineqlem8  42836  lcmineqlem10  42838  lcmineqlem11  42839  lcmineqlem12  42840  lcmineqlem16  42844  lcmineqlem18  42846  lcmineqlem23  42851  dvrelogpow2b  42868  aks4d1p1p2  42870  aks4d1p1  42876  aks4d1p8  42887  primrootsunit1  42897  primrootscoprmpow  42899  posbezout  42900  primrootscoprbij  42902  primrootspoweq0  42906  aks6d1c1p3  42910  aks6d1c1p8  42915  aks6d1c2p2  42919  hashscontpow1  42921  2np3bcnp1  42944  2ap1caineq  42945  sticksstones10  42955  sticksstones12a  42957  sticksstones16  42962  sticksstones22  42968  bcled  42978  bcle2d  42979  aks6d1c7lem1  42980  aks6d1c7  42984  unitscyglem2  42996  unitscyglem4  42998  unitscyglem5  42999  aks5lem8  43001  oddnumth  43105  nicomachus  43106  zaddcom  43271  fltabcoprmex  43404  fltaccoprm  43405  fltbccoprm  43406  fltne  43409  flt4lem3  43413  flt4lem5elem  43416  flt4lem5a  43417  flt4lem5b  43418  flt4lem5c  43419  flt4lem5d  43420  flt4lem5e  43421  flt4lem5f  43422  flt4lem6  43423  flt4lem7  43424  nna4b4nsq  43425  fltltc  43426  fltnltalem  43427  fltnlta  43428  irrapxlem4  43585  irrapxlem5  43586  pellexlem2  43590  pellexlem6  43594  pell1234qrne0  43613  pell1234qrreccl  43614  pell1234qrmulcl  43615  pell1234qrdich  43621  pell14qrdich  43629  pell1qrge1  43630  pell1qr1  43631  pell14qrgapw  43636  rmxyneg  43680  rmxm1  43694  rmxluc  43696  rmxdbl  43699  jm2.19lem1  43749  jm2.27c  43767  relexpmulnn  44468  relexpmulg  44469  inductionexd  44914  hashnzfzclim  45065  bcccl  45082  bcc0  45083  bccp1k  45084  bccm1k  45085  binomcxplemwb  45091  fsumnncl  46321  mccllem  46346  clim1fr1  46350  sumnnodd  46379  dvsinexp  46658  dvxpaek  46687  dvnxpaek  46689  dvnprodlem2  46694  itgsinexplem1  46701  itgsinexp  46702  stoweidlem1  46748  stoweidlem11  46758  stoweidlem25  46772  stoweidlem26  46773  stoweidlem34  46781  stoweidlem37  46784  stoweidlem38  46785  stoweidlem42  46789  wallispi2lem1  46818  wallispi2  46820  stirlinglem4  46824  stirlinglem5  46825  stirlinglem10  46830  stirlinglem15  46835  dirkertrigeqlem3  46847  dirkertrigeq  46848  dirkercncflem2  46851  dirkercncflem4  46853  fourierdlem11  46865  fourierdlem15  46869  fourierdlem79  46932  fourierdlem83  46936  sqwvfourb  46976  etransclem14  46995  etransclem15  46996  etransclem20  47001  etransclem21  47002  etransclem22  47003  etransclem23  47004  etransclem24  47005  etransclem25  47006  etransclem28  47009  etransclem31  47012  etransclem32  47013  etransclem33  47014  etransclem34  47015  etransclem35  47016  etransclem38  47019  etransclem41  47022  etransclem44  47025  etransclem45  47026  etransclem47  47028  etransclem48  47029  nnfoctbdjlem  47202  deccarry  48081  iccpartgtprec  48202  fmtnoodd  48318  fmtnorec2lem  48327  fmtnorec2  48328  fmtnodvds  48329  goldbachthlem2  48331  fmtnorec3  48333  fmtnorec4  48334  fmtnoprmfac1lem  48349  fmtnoprmfac1  48350  fmtnoprmfac2lem1  48351  fmtnoprmfac2  48352  2pwp1prm  48374  sfprmdvdsmersenne  48388  lighneallem4b  48394  lighneal  48396  proththdlem  48398  proththd  48399  ppivalnnprm  48410  oexpnegALTV  48475  perfectALTVlem1  48519  perfectALTVlem2  48520  perfectALTV  48521  nnpw2pmod  49396  nnolog2flm1  49403  blennn0em1  49404  blengt1fldiv2p1  49406  nn0sumshdiglemB  49433  amgmlemALT  50684