Theorem nncnd 12248

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 11097  ℕcn 12232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404  ax-un 7732  ax-1cn 11157  ax-addcl 11159

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-nn 12233

This theorem is referenced by:  nnadddir  12291  nnmul1com  12292  nnmulcom  12293  nneo  12679  facdiv  14323  facndiv  14324  faclbnd  14326  faclbnd5  14334  faclbnd6  14335  facubnd  14336  facavg  14337  bccmpl  14345  bcn0  14346  bcn1  14349  bcm1k  14351  bcp1n  14352  bcp1nk  14353  bcval5  14354  bcpasc  14357  permnn  14362  hashf1  14494  hashfac  14495  relexpaddnn  15088  binom11  15886  binom1dif  15887  climcndslem2  15904  arisum2  15915  trireciplem  15916  trirecip  15917  geo2sum  15927  geo2lim  15929  fprodfac  16027  risefacfac  16088  fallfacfwd  16089  fallfacval4  16096  bcfallfac  16097  fallfacfac  16098  bpolycl  16105  bpolysum  16106  bpolydiflem  16107  fsumkthpow  16109  eftcl  16126  eftabs  16128  efcllem  16130  ege2le3  16143  efcj  16145  efaddlem  16146  eftlub  16164  eirrlem  16259  sqrt2irrlem  16303  oexpneg  16402  pwp1fsum  16448  bitsp1  16488  bitsfzolem  16491  bitsfzo  16492  bitsmod  16493  bitscmp  16495  bitsinv1lem  16498  bitsinv1  16499  2ebits  16504  bitsinvp1  16506  sadcaddlem  16514  sadadd3  16518  bitsres  16530  bitsuz  16531  bitsshft  16532  dvdsgcdidd  16594  mulgcd  16605  rplpwr  16615  sqgcd  16619  expgcd  16620  nn0expgcd  16621  lcmgcdlem  16663  3lcm2e6woprm  16672  coprmprod  16718  coprmproddvdslem  16719  cncongr1  16724  cncongr2  16725  prmind2  16742  isprm5  16765  divgcdodd  16768  prmdvdsexpr  16775  qmuldeneqnum  16805  divnumden  16806  qnumgt0  16808  numdensq  16812  numdenexp  16818  hashdvds  16833  phiprmpw  16834  prmdiv  16843  prmdivdiv  16845  phisum  16849  modprm0  16864  pythagtriplem4  16878  pythagtriplem6  16880  pythagtriplem7  16881  pythagtriplem14  16887  pythagtriplem15  16888  pythagtriplem19  16892  pythagtrip  16893  pcprendvds2  16900  pcpre1  16901  pcpremul  16902  pceulem  16904  pcdiv  16911  pcqmul  16912  pcelnn  16929  pcid  16932  pc2dvds  16938  dvdsprmpweqnn  16944  dvdsprmpweqle  16945  pcaddlem  16947  pcadd  16948  pcfaclem  16957  qexpz  16960  expnprm  16961  oddprmdvds  16962  prmpwdvds  16963  pockthlem  16964  pockthg  16965  infpnlem1  16969  prmreclem1  16975  prmreclem2  16976  prmreclem3  16977  prmreclem4  16978  prmreclem6  16980  4sqlem6  17002  4sqlem7  17003  4sqlem10  17006  mul4sqlem  17012  4sqlem11  17014  4sqlem12  17015  4sqlem14  17017  4sqlem17  17020  4sqlem18  17021  vdwlem1  17040  vdwlem2  17041  vdwlem3  17042  vdwlem5  17044  vdwlem6  17045  vdwlem8  17047  vdwlem9  17048  vdwlem10  17049  vdwlem12  17051  ramub1lem2  17086  ramcl  17088  prmop1  17097  prmdvdsprmo  17101  prmgaplem7  17116  prmgaplem8  17117  chnub  18677  gsumsgrpccat  18898  mulgnndir  19168  mulgnnass  19174  psgnunilem5  19563  odf1o2  19642  pgp0  19665  sylow1lem1  19667  odcau  19673  sylow2blem3  19691  sylow3lem3  19698  sylow3lem4  19699  gexexlem  19921  ablfacrp2  20138  ablfac1lem  20139  ablfac1eu  20144  pgpfac1lem3a  20147  pgpfac1lem3  20148  fincygsubgodexd  20184  zringlpirlem3  21593  znrrg  21694  psdpw  22312  cpmadugsumlemF  23012  lebnumlem3  25101  ovollb2lem  25626  ovolunlem1a  25634  ovolunlem1  25635  uniioombllem3  25723  uniioombllem4  25724  dyaddisjlem  25733  mbfi1fseqlem3  25855  mbfi1fseqlem4  25856  itgpowd  26188  dgrcolem1  26409  vieta1lem1  26450  vieta1lem2  26451  elqaalem2  26460  elqaalem3  26461  aalioulem1  26472  aaliou3lem2  26483  aaliou3lem8  26485  aaliou3lem6  26488  aaliou3lem9  26490  taylfvallem1  26496  tayl0  26501  taylply2  26507  taylply  26508  dvtaylp  26509  taylthlem1  26512  taylthlem2  26513  pserdvlem2  26567  advlogexp  26796  cxpmul2  26830  cxpeq  26898  rtprmirr  26901  atantayl3  27080  leibpi  27083  log2cnv  27085  log2tlbnd  27086  birthdaylem2  27093  birthdaylem3  27094  amgmlem  27130  amgm  27131  emcllem5  27140  fsumharmonic  27152  zetacvg  27155  dmgmdivn0  27168  lgamgulmlem3  27171  lgamgulmlem4  27172  lgamgulmlem5  27173  lgamgulmlem6  27174  lgamgulm2  27176  lgamcvg2  27195  gamcvg  27196  gamcvg2lem  27199  facgam  27206  wilthlem1  27208  wilthlem2  27209  wilthlem3  27210  wilthimp  27212  basellem1  27221  basellem2  27222  basellem3  27223  basellem4  27224  basellem5  27225  basellem8  27228  vmaprm  27257  sgmval2  27283  0sgm  27284  sgmf  27285  vma1  27306  fsumdvdsdiaglem  27323  dvdsflf1o  27327  muinv  27333  mpodvdsmulf1o  27334  dvdsmulf1o  27336  sgmppw  27337  1sgmprm  27339  1sgm2ppw  27340  sgmmul  27341  chtublem  27351  fsumvma2  27354  chpchtsum  27359  logfaclbnd  27362  logexprlim  27365  mersenne  27367  perfect1  27368  perfectlem1  27369  perfectlem2  27370  perfect  27371  dchrsum2  27408  dchrhash  27411  bcmono  27417  bcp1ctr  27419  bclbnd  27420  bposlem1  27424  bposlem2  27425  bposlem3  27426  bposlem5  27428  bposlem6  27429  lgsval2lem  27447  lgsqrlem2  27487  gausslemma2dlem6  27512  gausslemma2dlem7  27513  gausslemma2d  27514  lgseisenlem1  27515  lgseisenlem4  27518  lgsquadlem1  27520  lgsquadlem2  27521  lgsquadlem3  27522  lgsquad2  27526  m1lgs  27528  2sqlem3  27560  2sqlem4  27561  chebbnd1lem1  27609  chebbnd1  27612  rplogsumlem1  27624  rplogsumlem2  27625  rpvmasumlem  27627  dchrisumlem1  27629  dchrmusum2  27634  dchrvmasumlem1  27635  dchrvmasum2lem  27636  dchrvmasum2if  27637  dchrvmasumlem2  27638  dchrvmasumlem3  27639  dchrvmasumiflem1  27641  dchrisum0flblem1  27648  dchrisum0flblem2  27649  dchrisum0fno1  27651  rpvmasum2  27652  rplogsum  27667  mulogsumlem  27671  mulogsum  27672  mulog2sumlem2  27675  vmalogdivsum2  27678  vmalogdivsum  27679  2vmadivsumlem  27680  logsqvma  27682  selberglem2  27686  selberglem3  27687  selberg  27688  selberg2lem  27690  logdivbnd  27696  selberg3lem1  27697  selberg4lem1  27700  pntrsumo1  27705  pntrsumbnd2  27707  selberg3r  27709  selberg4r  27710  selberg34r  27711  pntsval2  27716  pntrlog2bndlem2  27718  pntrlog2bndlem4  27720  pntrlog2bndlem6  27723  pntpbnd1  27726  pntpbnd2  27727  pntlemg  27738  pntlemn  27740  pntlemf  27745  pnt  27754  padicabvf  27771  ostth2lem2  27774  ostth3  27778  fusgrhashclwwlkn  30396  eucrct2eupth  30562  nrt2irr  30790  elq2  33122  numdenneg  33125  ltesubnnd  33133  2exple2exp  33144  oexpled  33146  gsummptp1  33343  1arithidomlem2  33792  1arithidom  33793  zringfrac  33810  cos9thpiminplylem1  34138  cos9thpiminplylem2  34139  1smat1  34160  madjusmdetlem2  34184  madjusmdetlem4  34186  qqhnm  34346  oddpwdc  34710  eulerpartlemsv2  34714  eulerpartlems  34716  eulerpartlemsv3  34717  eulerpartlemgc  34718  eulerpartlemv  34720  eulerpartlemgs2  34736  fibp1  34757  ballotlemfc0  34849  ballotlemfcc  34850  signsvtn0  34923  reprpmtf1o  34979  vtscl  34991  hgt750lemb  35009  tgoldbachgt  35016  subfacp1lem1  35637  subfacp1lem5  35642  subfacval2  35645  subfaclim  35646  cvmliftlem2  35744  cvmliftlem7  35749  cvmliftlem10  35752  cvmliftlem11  35753  cvmliftlem13  35754  bcm1nt  36195  bcprod  36196  iprodgam  36200  faclimlem1  36201  faclimlem2  36202  faclim2  36206  nn0prpwlem  36799  nn0prpw  36800  knoppcnlem10  37057  knoppndvlem16  37082  poimirlem1  38238  poimirlem2  38239  poimirlem6  38243  poimirlem7  38244  poimirlem8  38245  poimirlem9  38246  poimirlem10  38247  poimirlem11  38248  poimirlem12  38249  poimirlem13  38250  poimirlem15  38252  poimirlem16  38253  poimirlem17  38254  poimirlem18  38255  poimirlem19  38256  poimirlem20  38257  poimirlem21  38258  poimirlem22  38259  poimirlem23  38260  poimirlem24  38261  poimirlem25  38262  poimirlem26  38263  poimirlem27  38264  poimirlem31  38268  nnproddivdvdsd  42735  lcmfunnnd  42747  lcmineqlem3  42766  lcmineqlem4  42767  lcmineqlem6  42769  lcmineqlem8  42771  lcmineqlem10  42773  lcmineqlem11  42774  lcmineqlem12  42775  lcmineqlem16  42779  lcmineqlem18  42781  lcmineqlem23  42786  dvrelogpow2b  42803  aks4d1p1p2  42805  aks4d1p1  42811  aks4d1p8  42822  primrootsunit1  42832  primrootscoprmpow  42834  posbezout  42835  primrootscoprbij  42837  primrootspoweq0  42841  aks6d1c1p3  42845  aks6d1c1p8  42850  aks6d1c2p2  42854  hashscontpow1  42856  2np3bcnp1  42879  2ap1caineq  42880  sticksstones10  42890  sticksstones12a  42892  sticksstones16  42897  sticksstones22  42903  bcled  42913  bcle2d  42914  aks6d1c7lem1  42915  aks6d1c7  42919  unitscyglem2  42931  unitscyglem4  42933  unitscyglem5  42934  aks5lem8  42936  oddnumth  43040  nicomachus  43041  zaddcom  43206  fltabcoprmex  43341  fltaccoprm  43342  fltbccoprm  43343  fltne  43346  flt4lem3  43350  flt4lem5elem  43353  flt4lem5a  43354  flt4lem5b  43355  flt4lem5c  43356  flt4lem5d  43357  flt4lem5e  43358  flt4lem5f  43359  flt4lem6  43360  flt4lem7  43361  nna4b4nsq  43362  fltltc  43363  fltnltalem  43364  fltnlta  43365  irrapxlem4  43522  irrapxlem5  43523  pellexlem2  43527  pellexlem6  43531  pell1234qrne0  43550  pell1234qrreccl  43551  pell1234qrmulcl  43552  pell1234qrdich  43558  pell14qrdich  43566  pell1qrge1  43567  pell1qr1  43568  pell14qrgapw  43573  rmxyneg  43617  rmxm1  43631  rmxluc  43633  rmxdbl  43636  jm2.19lem1  43686  jm2.27c  43704  relexpmulnn  44405  relexpmulg  44406  inductionexd  44851  hashnzfzclim  45002  bcccl  45019  bcc0  45020  bccp1k  45021  bccm1k  45022  binomcxplemwb  45028  fsumnncl  46258  mccllem  46283  clim1fr1  46287  sumnnodd  46316  dvsinexp  46595  dvxpaek  46624  dvnxpaek  46626  dvnprodlem2  46631  itgsinexplem1  46638  itgsinexp  46639  stoweidlem1  46685  stoweidlem11  46695  stoweidlem25  46709  stoweidlem26  46710  stoweidlem34  46718  stoweidlem37  46721  stoweidlem38  46722  stoweidlem42  46726  wallispi2lem1  46755  wallispi2  46757  stirlinglem4  46761  stirlinglem5  46762  stirlinglem10  46767  stirlinglem15  46772  dirkertrigeqlem3  46784  dirkertrigeq  46785  dirkercncflem2  46788  dirkercncflem4  46790  fourierdlem11  46802  fourierdlem15  46806  fourierdlem79  46869  fourierdlem83  46873  sqwvfourb  46913  etransclem14  46932  etransclem15  46933  etransclem20  46938  etransclem21  46939  etransclem22  46940  etransclem23  46941  etransclem24  46942  etransclem25  46943  etransclem28  46946  etransclem31  46949  etransclem32  46950  etransclem33  46951  etransclem34  46952  etransclem35  46953  etransclem38  46956  etransclem41  46959  etransclem44  46962  etransclem45  46963  etransclem47  46965  etransclem48  46966  nnfoctbdjlem  47139  deccarry  48015  iccpartgtprec  48136  fmtnoodd  48252  fmtnorec2lem  48261  fmtnorec2  48262  fmtnodvds  48263  goldbachthlem2  48265  fmtnorec3  48267  fmtnorec4  48268  fmtnoprmfac1lem  48283  fmtnoprmfac1  48284  fmtnoprmfac2lem1  48285  fmtnoprmfac2  48286  2pwp1prm  48308  sfprmdvdsmersenne  48322  lighneallem4b  48328  lighneal  48330  proththdlem  48332  proththd  48333  ppivalnnprm  48344  oexpnegALTV  48409  perfectALTVlem1  48453  perfectALTVlem2  48454  perfectALTV  48455  nnpw2pmod  49330  nnolog2flm1  49337  blennn0em1  49338  blengt1fldiv2p1  49340  nn0sumshdiglemB  49367  amgmlemALT  50570