Theorem nncnd 12309

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11182  ℕcn 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-nn 12294

This theorem is referenced by:  nneo  12727  facdiv  14336  facndiv  14337  faclbnd  14339  faclbnd5  14347  faclbnd6  14348  facubnd  14349  facavg  14350  bccmpl  14358  bcn0  14359  bcn1  14362  bcm1k  14364  bcp1n  14365  bcp1nk  14366  bcval5  14367  bcpasc  14370  permnn  14375  hashf1  14506  hashfac  14507  relexpaddnn  15100  binom11  15880  binom1dif  15881  climcndslem2  15898  arisum2  15909  trireciplem  15910  trirecip  15911  geo2sum  15921  geo2lim  15923  fprodfac  16021  risefacfac  16083  fallfacfwd  16084  fallfacval4  16091  bcfallfac  16092  fallfacfac  16093  bpolycl  16100  bpolysum  16101  bpolydiflem  16102  fsumkthpow  16104  eftcl  16121  eftabs  16123  efcllem  16125  ege2le3  16138  efcj  16140  efaddlem  16141  eftlub  16157  eirrlem  16252  sqrt2irrlem  16296  oexpneg  16393  pwp1fsum  16439  bitsp1  16477  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  bitscmp  16484  bitsinv1lem  16487  bitsinv1  16488  2ebits  16493  bitsinvp1  16495  sadcaddlem  16503  sadadd3  16507  bitsres  16519  bitsuz  16520  bitsshft  16521  dvdsgcdidd  16584  mulgcd  16595  rplpwr  16605  sqgcd  16609  expgcd  16610  nn0expgcd  16611  lcmgcdlem  16653  3lcm2e6woprm  16662  coprmprod  16708  coprmproddvdslem  16709  cncongr1  16714  cncongr2  16715  prmind2  16732  isprm5  16754  divgcdodd  16757  prmdvdsexpr  16764  qmuldeneqnum  16794  divnumden  16795  qnumgt0  16797  numdensq  16801  numdenexp  16807  hashdvds  16822  phiprmpw  16823  prmdiv  16832  prmdivdiv  16834  phisum  16837  modprm0  16852  pythagtriplem4  16866  pythagtriplem6  16868  pythagtriplem7  16869  pythagtriplem14  16875  pythagtriplem15  16876  pythagtriplem19  16880  pythagtrip  16881  pcprendvds2  16888  pcpre1  16889  pcpremul  16890  pceulem  16892  pcdiv  16899  pcqmul  16900  pcelnn  16917  pcid  16920  pc2dvds  16926  dvdsprmpweqnn  16932  dvdsprmpweqle  16933  pcaddlem  16935  pcadd  16936  pcfaclem  16945  qexpz  16948  expnprm  16949  oddprmdvds  16950  prmpwdvds  16951  pockthlem  16952  pockthg  16953  infpnlem1  16957  prmreclem1  16963  prmreclem2  16964  prmreclem3  16965  prmreclem4  16966  prmreclem6  16968  4sqlem6  16990  4sqlem7  16991  4sqlem10  16994  mul4sqlem  17000  4sqlem11  17002  4sqlem12  17003  4sqlem14  17005  4sqlem17  17008  4sqlem18  17009  vdwlem1  17028  vdwlem2  17029  vdwlem3  17030  vdwlem5  17032  vdwlem6  17033  vdwlem8  17035  vdwlem9  17036  vdwlem10  17037  vdwlem12  17039  ramub1lem2  17074  ramcl  17076  prmop1  17085  prmdvdsprmo  17089  prmgaplem7  17104  prmgaplem8  17105  gsumsgrpccat  18875  mulgnndir  19143  mulgnnass  19149  psgnunilem5  19536  odf1o2  19615  pgp0  19638  sylow1lem1  19640  odcau  19646  sylow2blem3  19664  sylow3lem3  19671  sylow3lem4  19672  gexexlem  19894  ablfacrp2  20111  ablfac1lem  20112  ablfac1eu  20117  pgpfac1lem3a  20120  pgpfac1lem3  20121  fincygsubgodexd  20157  zringlpirlem3  21498  znrrg  21607  cpmadugsumlemF  22903  lebnumlem3  25014  ovollb2lem  25542  ovolunlem1a  25550  ovolunlem1  25551  uniioombllem3  25639  uniioombllem4  25640  dyaddisjlem  25649  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  itgpowd  26111  dgrcolem1  26333  vieta1lem1  26370  vieta1lem2  26371  elqaalem2  26380  elqaalem3  26381  aalioulem1  26392  aaliou3lem2  26403  aaliou3lem8  26405  aaliou3lem6  26408  aaliou3lem9  26410  taylfvallem1  26416  tayl0  26421  taylply2  26427  taylply2OLD  26428  taylply  26429  dvtaylp  26430  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  pserdvlem2  26490  advlogexp  26715  cxpmul2  26749  cxpeq  26818  rtprmirr  26821  atantayl3  27000  leibpi  27003  log2cnv  27005  log2tlbnd  27006  birthdaylem2  27013  birthdaylem3  27014  amgmlem  27051  amgm  27052  emcllem5  27061  fsumharmonic  27073  zetacvg  27076  dmgmdivn0  27089  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem5  27094  lgamgulmlem6  27095  lgamgulm2  27097  lgamcvg2  27116  gamcvg  27117  gamcvg2lem  27120  facgam  27127  wilthlem1  27129  wilthlem2  27130  wilthlem3  27131  wilthimp  27133  basellem1  27142  basellem2  27143  basellem3  27144  basellem4  27145  basellem5  27146  basellem8  27149  vmaprm  27178  sgmval2  27204  0sgm  27205  sgmf  27206  vma1  27227  fsumdvdsdiaglem  27244  dvdsflf1o  27248  muinv  27254  mpodvdsmulf1o  27255  dvdsmulf1o  27257  sgmppw  27259  1sgmprm  27261  1sgm2ppw  27262  sgmmul  27263  chtublem  27273  fsumvma2  27276  chpchtsum  27281  logfaclbnd  27284  logexprlim  27287  mersenne  27289  perfect1  27290  perfectlem1  27291  perfectlem2  27292  perfect  27293  dchrsum2  27330  dchrhash  27333  bcmono  27339  bcp1ctr  27341  bclbnd  27342  bposlem1  27346  bposlem2  27347  bposlem3  27348  bposlem5  27350  bposlem6  27351  lgsval2lem  27369  lgsqrlem2  27409  gausslemma2dlem6  27434  gausslemma2dlem7  27435  gausslemma2d  27436  lgseisenlem1  27437  lgseisenlem4  27440  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  lgsquad2  27448  m1lgs  27450  2sqlem3  27482  2sqlem4  27483  chebbnd1lem1  27531  chebbnd1  27534  rplogsumlem1  27546  rplogsumlem2  27547  rpvmasumlem  27549  dchrisumlem1  27551  dchrmusum2  27556  dchrvmasumlem1  27557  dchrvmasum2lem  27558  dchrvmasum2if  27559  dchrvmasumlem2  27560  dchrvmasumlem3  27561  dchrvmasumiflem1  27563  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0fno1  27573  rpvmasum2  27574  rplogsum  27589  mulogsumlem  27593  mulogsum  27594  mulog2sumlem2  27597  vmalogdivsum2  27600  vmalogdivsum  27601  2vmadivsumlem  27602  logsqvma  27604  selberglem2  27608  selberglem3  27609  selberg  27610  selberg2lem  27612  logdivbnd  27618  selberg3lem1  27619  selberg4lem1  27622  pntrsumo1  27627  pntrsumbnd2  27629  selberg3r  27631  selberg4r  27632  selberg34r  27633  pntsval2  27638  pntrlog2bndlem2  27640  pntrlog2bndlem4  27642  pntrlog2bndlem6  27645  pntpbnd1  27648  pntpbnd2  27649  pntlemg  27660  pntlemn  27662  pntlemf  27667  pnt  27676  padicabvf  27693  ostth2lem2  27696  ostth3  27700  fusgrhashclwwlkn  30111  eucrct2eupth  30277  nrt2irr  30505  numdenneg  32818  ltesubnnd  32826  chnub  32984  1arithidomlem2  33529  1arithidom  33530  zringfrac  33547  1smat1  33750  madjusmdetlem2  33774  madjusmdetlem4  33776  qqhnm  33936  oddpwdc  34319  eulerpartlemsv2  34323  eulerpartlems  34325  eulerpartlemsv3  34326  eulerpartlemgc  34327  eulerpartlemv  34329  eulerpartlemgs2  34345  fibp1  34366  ballotlemfc0  34457  ballotlemfcc  34458  signsvtn0  34547  reprpmtf1o  34603  vtscl  34615  hgt750lemb  34633  tgoldbachgt  34640  subfacp1lem1  35147  subfacp1lem5  35152  subfacval2  35155  subfaclim  35156  cvmliftlem2  35254  cvmliftlem7  35259  cvmliftlem10  35262  cvmliftlem11  35263  cvmliftlem13  35264  bcm1nt  35699  bcprod  35700  iprodgam  35704  faclimlem1  35705  faclimlem2  35706  faclim2  35710  nn0prpwlem  36288  nn0prpw  36289  knoppcnlem10  36468  knoppndvlem16  36493  poimirlem1  37581  poimirlem2  37582  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem9  37589  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem15  37595  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  nnproddivdvdsd  41957  lcmfunnnd  41969  lcmineqlem3  41988  lcmineqlem4  41989  lcmineqlem6  41991  lcmineqlem8  41993  lcmineqlem10  41995  lcmineqlem11  41996  lcmineqlem12  41997  lcmineqlem16  42001  lcmineqlem18  42003  lcmineqlem23  42008  dvrelogpow2b  42025  aks4d1p1p2  42027  aks4d1p1  42033  aks4d1p8  42044  primrootsunit1  42054  primrootscoprmpow  42056  posbezout  42057  primrootscoprbij  42059  primrootspoweq0  42063  aks6d1c1p3  42067  aks6d1c1p8  42072  aks6d1c2p2  42076  hashscontpow1  42078  2np3bcnp1  42101  2ap1caineq  42102  sticksstones10  42112  sticksstones12a  42114  sticksstones16  42119  sticksstones22  42125  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  aks6d1c7  42141  unitscyglem2  42153  unitscyglem4  42155  unitscyglem5  42156  aks5lem8  42158  metakunt8  42169  metakunt15  42176  metakunt16  42177  metakunt20  42181  metakunt28  42189  metakunt30  42191  nnadddir  42259  nnmul1com  42260  nnmulcom  42261  oddnumth  42299  nicomachus  42300  zaddcom  42428  fltabcoprmex  42594  fltaccoprm  42595  fltbccoprm  42596  fltne  42599  flt4lem3  42603  flt4lem5elem  42606  flt4lem5a  42607  flt4lem5b  42608  flt4lem5c  42609  flt4lem5d  42610  flt4lem5e  42611  flt4lem5f  42612  flt4lem6  42613  flt4lem7  42614  nna4b4nsq  42615  fltltc  42616  fltnltalem  42617  fltnlta  42618  irrapxlem4  42781  irrapxlem5  42782  pellexlem2  42786  pellexlem6  42790  pell1234qrne0  42809  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell1234qrdich  42817  pell14qrdich  42825  pell1qrge1  42826  pell1qr1  42827  pell14qrgapw  42832  rmxyneg  42877  rmxm1  42891  rmxluc  42893  rmxdbl  42896  jm2.19lem1  42946  jm2.27c  42964  relexpmulnn  43671  relexpmulg  43672  inductionexd  44117  hashnzfzclim  44291  bcccl  44308  bcc0  44309  bccp1k  44310  bccm1k  44311  binomcxplemwb  44317  fsumnncl  45493  mccllem  45518  clim1fr1  45522  sumnnodd  45551  dvsinexp  45832  dvxpaek  45861  dvnxpaek  45863  dvnprodlem2  45868  itgsinexplem1  45875  itgsinexp  45876  stoweidlem1  45922  stoweidlem11  45932  stoweidlem25  45946  stoweidlem26  45947  stoweidlem34  45955  stoweidlem37  45958  stoweidlem38  45959  stoweidlem42  45963  wallispi2lem1  45992  wallispi2  45994  stirlinglem4  45998  stirlinglem5  45999  stirlinglem10  46004  stirlinglem15  46009  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem11  46039  fourierdlem15  46043  fourierdlem79  46106  fourierdlem83  46110  sqwvfourb  46150  etransclem14  46169  etransclem15  46170  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem23  46178  etransclem24  46179  etransclem25  46180  etransclem28  46183  etransclem31  46186  etransclem32  46187  etransclem33  46188  etransclem34  46189  etransclem35  46190  etransclem38  46193  etransclem41  46196  etransclem44  46199  etransclem45  46200  etransclem47  46202  etransclem48  46203  nnfoctbdjlem  46376  deccarry  47226  iccpartgtprec  47294  fmtnoodd  47407  fmtnorec2lem  47416  fmtnorec2  47417  fmtnodvds  47418  goldbachthlem2  47420  fmtnorec3  47422  fmtnorec4  47423  fmtnoprmfac1lem  47438  fmtnoprmfac1  47439  fmtnoprmfac2lem1  47440  fmtnoprmfac2  47441  2pwp1prm  47463  sfprmdvdsmersenne  47477  lighneallem4b  47483  lighneal  47485  proththdlem  47487  proththd  47488  oexpnegALTV  47551  perfectALTVlem1  47595  perfectALTVlem2  47596  perfectALTV  47597  nnpw2pmod  48317  nnolog2flm1  48324  blennn0em1  48325  blengt1fldiv2p1  48327  nn0sumshdiglemB  48354  amgmlemALT  48897