Theorem nncnd 12240

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℂcc 11086  ℕcn 12224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722  ax-1cn 11146  ax-addcl 11148

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-nn 12225

This theorem is referenced by:  nnadddir  12283  nnmul1com  12284  nnmulcom  12285  nneo  12671  facdiv  14314  facndiv  14315  faclbnd  14317  faclbnd5  14325  faclbnd6  14326  facubnd  14327  facavg  14328  bccmpl  14336  bcn0  14337  bcn1  14340  bcm1k  14342  bcp1n  14343  bcp1nk  14344  bcval5  14345  bcpasc  14348  permnn  14353  hashf1  14484  hashfac  14485  relexpaddnn  15078  binom11  15876  binom1dif  15877  climcndslem2  15894  arisum2  15905  trireciplem  15906  trirecip  15907  geo2sum  15917  geo2lim  15919  fprodfac  16017  risefacfac  16079  fallfacfwd  16080  fallfacval4  16087  bcfallfac  16088  fallfacfac  16089  bpolycl  16096  bpolysum  16097  bpolydiflem  16098  fsumkthpow  16100  eftcl  16117  eftabs  16119  efcllem  16121  ege2le3  16134  efcj  16136  efaddlem  16137  eftlub  16155  eirrlem  16250  sqrt2irrlem  16294  oexpneg  16393  pwp1fsum  16439  bitsp1  16479  bitsfzolem  16482  bitsfzo  16483  bitsmod  16484  bitscmp  16486  bitsinv1lem  16489  bitsinv1  16490  2ebits  16495  bitsinvp1  16497  sadcaddlem  16505  sadadd3  16509  bitsres  16521  bitsuz  16522  bitsshft  16523  dvdsgcdidd  16585  mulgcd  16596  rplpwr  16606  sqgcd  16610  expgcd  16611  nn0expgcd  16612  lcmgcdlem  16654  3lcm2e6woprm  16663  coprmprod  16709  coprmproddvdslem  16710  cncongr1  16715  cncongr2  16716  prmind2  16733  isprm5  16756  divgcdodd  16759  prmdvdsexpr  16766  qmuldeneqnum  16796  divnumden  16797  qnumgt0  16799  numdensq  16803  numdenexp  16809  hashdvds  16824  phiprmpw  16825  prmdiv  16834  prmdivdiv  16836  phisum  16840  modprm0  16855  pythagtriplem4  16869  pythagtriplem6  16871  pythagtriplem7  16872  pythagtriplem14  16878  pythagtriplem15  16879  pythagtriplem19  16883  pythagtrip  16884  pcprendvds2  16891  pcpre1  16892  pcpremul  16893  pceulem  16895  pcdiv  16902  pcqmul  16903  pcelnn  16920  pcid  16923  pc2dvds  16929  dvdsprmpweqnn  16935  dvdsprmpweqle  16936  pcaddlem  16938  pcadd  16939  pcfaclem  16948  qexpz  16951  expnprm  16952  oddprmdvds  16953  prmpwdvds  16954  pockthlem  16955  pockthg  16956  infpnlem1  16960  prmreclem1  16966  prmreclem2  16967  prmreclem3  16968  prmreclem4  16969  prmreclem6  16971  4sqlem6  16993  4sqlem7  16994  4sqlem10  16997  mul4sqlem  17003  4sqlem11  17005  4sqlem12  17006  4sqlem14  17008  4sqlem17  17011  4sqlem18  17012  vdwlem1  17031  vdwlem2  17032  vdwlem3  17033  vdwlem5  17035  vdwlem6  17036  vdwlem8  17038  vdwlem9  17039  vdwlem10  17040  vdwlem12  17042  ramub1lem2  17077  ramcl  17079  prmop1  17088  prmdvdsprmo  17092  prmgaplem7  17107  prmgaplem8  17108  chnub  18668  gsumsgrpccat  18889  mulgnndir  19160  mulgnnass  19166  psgnunilem5  19555  odf1o2  19634  pgp0  19657  sylow1lem1  19659  odcau  19665  sylow2blem3  19683  sylow3lem3  19690  sylow3lem4  19691  gexexlem  19913  ablfacrp2  20130  ablfac1lem  20131  ablfac1eu  20136  pgpfac1lem3a  20139  pgpfac1lem3  20140  fincygsubgodexd  20176  zringlpirlem3  21574  znrrg  21675  psdpw  22293  cpmadugsumlemF  22994  lebnumlem3  25083  ovollb2lem  25608  ovolunlem1a  25616  ovolunlem1  25617  uniioombllem3  25705  uniioombllem4  25706  dyaddisjlem  25715  mbfi1fseqlem3  25837  mbfi1fseqlem4  25838  itgpowd  26170  dgrcolem1  26391  vieta1lem1  26432  vieta1lem2  26433  elqaalem2  26442  elqaalem3  26443  aalioulem1  26454  aaliou3lem2  26465  aaliou3lem8  26467  aaliou3lem6  26470  aaliou3lem9  26472  taylfvallem1  26478  tayl0  26483  taylply2  26489  taylply  26490  dvtaylp  26491  taylthlem1  26494  taylthlem2  26495  pserdvlem2  26549  advlogexp  26778  cxpmul2  26812  cxpeq  26880  rtprmirr  26883  atantayl3  27062  leibpi  27065  log2cnv  27067  log2tlbnd  27068  birthdaylem2  27075  birthdaylem3  27076  amgmlem  27112  amgm  27113  emcllem5  27122  fsumharmonic  27134  zetacvg  27137  dmgmdivn0  27150  lgamgulmlem3  27153  lgamgulmlem4  27154  lgamgulmlem5  27155  lgamgulmlem6  27156  lgamgulm2  27158  lgamcvg2  27177  gamcvg  27178  gamcvg2lem  27181  facgam  27188  wilthlem1  27190  wilthlem2  27191  wilthlem3  27192  wilthimp  27194  basellem1  27203  basellem2  27204  basellem3  27205  basellem4  27206  basellem5  27207  basellem8  27210  vmaprm  27239  sgmval2  27265  0sgm  27266  sgmf  27267  vma1  27288  fsumdvdsdiaglem  27305  dvdsflf1o  27309  muinv  27315  mpodvdsmulf1o  27316  dvdsmulf1o  27318  sgmppw  27319  1sgmprm  27321  1sgm2ppw  27322  sgmmul  27323  chtublem  27333  fsumvma2  27336  chpchtsum  27341  logfaclbnd  27344  logexprlim  27347  mersenne  27349  perfect1  27350  perfectlem1  27351  perfectlem2  27352  perfect  27353  dchrsum2  27390  dchrhash  27393  bcmono  27399  bcp1ctr  27401  bclbnd  27402  bposlem1  27406  bposlem2  27407  bposlem3  27408  bposlem5  27410  bposlem6  27411  lgsval2lem  27429  lgsqrlem2  27469  gausslemma2dlem6  27494  gausslemma2dlem7  27495  gausslemma2d  27496  lgseisenlem1  27497  lgseisenlem4  27500  lgsquadlem1  27502  lgsquadlem2  27503  lgsquadlem3  27504  lgsquad2  27508  m1lgs  27510  2sqlem3  27542  2sqlem4  27543  chebbnd1lem1  27591  chebbnd1  27594  rplogsumlem1  27606  rplogsumlem2  27607  rpvmasumlem  27609  dchrisumlem1  27611  dchrmusum2  27616  dchrvmasumlem1  27617  dchrvmasum2lem  27618  dchrvmasum2if  27619  dchrvmasumlem2  27620  dchrvmasumlem3  27621  dchrvmasumiflem1  27623  dchrisum0flblem1  27630  dchrisum0flblem2  27631  dchrisum0fno1  27633  rpvmasum2  27634  rplogsum  27649  mulogsumlem  27653  mulogsum  27654  mulog2sumlem2  27657  vmalogdivsum2  27660  vmalogdivsum  27661  2vmadivsumlem  27662  logsqvma  27664  selberglem2  27668  selberglem3  27669  selberg  27670  selberg2lem  27672  logdivbnd  27678  selberg3lem1  27679  selberg4lem1  27682  pntrsumo1  27687  pntrsumbnd2  27689  selberg3r  27691  selberg4r  27692  selberg34r  27693  pntsval2  27698  pntrlog2bndlem2  27700  pntrlog2bndlem4  27702  pntrlog2bndlem6  27705  pntpbnd1  27708  pntpbnd2  27709  pntlemg  27720  pntlemn  27722  pntlemf  27727  pnt  27736  padicabvf  27753  ostth2lem2  27756  ostth3  27760  fusgrhashclwwlkn  30339  eucrct2eupth  30505  nrt2irr  30733  elq2  33069  numdenneg  33072  ltesubnnd  33080  2exple2exp  33091  oexpled  33093  gsummptp1  33290  1arithidomlem2  33743  1arithidom  33744  zringfrac  33761  cos9thpiminplylem1  34089  cos9thpiminplylem2  34090  1smat1  34111  madjusmdetlem2  34135  madjusmdetlem4  34137  qqhnm  34297  oddpwdc  34661  eulerpartlemsv2  34665  eulerpartlems  34667  eulerpartlemsv3  34668  eulerpartlemgc  34669  eulerpartlemv  34671  eulerpartlemgs2  34687  fibp1  34708  ballotlemfc0  34800  ballotlemfcc  34801  signsvtn0  34874  reprpmtf1o  34930  vtscl  34942  hgt750lemb  34960  tgoldbachgt  34967  subfacp1lem1  35542  subfacp1lem5  35547  subfacval2  35550  subfaclim  35551  cvmliftlem2  35649  cvmliftlem7  35654  cvmliftlem10  35657  cvmliftlem11  35658  cvmliftlem13  35659  bcm1nt  36100  bcprod  36101  iprodgam  36105  faclimlem1  36106  faclimlem2  36107  faclim2  36111  nn0prpwlem  36695  nn0prpw  36696  knoppcnlem10  36953  knoppndvlem16  36978  poimirlem1  38132  poimirlem2  38133  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem9  38140  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem13  38144  poimirlem15  38146  poimirlem16  38147  poimirlem17  38148  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem23  38154  poimirlem24  38155  poimirlem25  38156  poimirlem26  38157  poimirlem27  38158  poimirlem31  38162  nnproddivdvdsd  42629  lcmfunnnd  42641  lcmineqlem3  42660  lcmineqlem4  42661  lcmineqlem6  42663  lcmineqlem8  42665  lcmineqlem10  42667  lcmineqlem11  42668  lcmineqlem12  42669  lcmineqlem16  42673  lcmineqlem18  42675  lcmineqlem23  42680  dvrelogpow2b  42697  aks4d1p1p2  42699  aks4d1p1  42705  aks4d1p8  42716  primrootsunit1  42726  primrootscoprmpow  42728  posbezout  42729  primrootscoprbij  42731  primrootspoweq0  42735  aks6d1c1p3  42739  aks6d1c1p8  42744  aks6d1c2p2  42748  hashscontpow1  42750  2np3bcnp1  42773  2ap1caineq  42774  sticksstones10  42784  sticksstones12a  42786  sticksstones16  42791  sticksstones22  42797  bcled  42807  bcle2d  42808  aks6d1c7lem1  42809  aks6d1c7  42813  unitscyglem2  42825  unitscyglem4  42827  unitscyglem5  42828  aks5lem8  42830  oddnumth  42932  nicomachus  42933  zaddcom  43098  fltabcoprmex  43233  fltaccoprm  43234  fltbccoprm  43235  fltne  43238  flt4lem3  43242  flt4lem5elem  43245  flt4lem5a  43246  flt4lem5b  43247  flt4lem5c  43248  flt4lem5d  43249  flt4lem5e  43250  flt4lem5f  43251  flt4lem6  43252  flt4lem7  43253  nna4b4nsq  43254  fltltc  43255  fltnltalem  43256  fltnlta  43257  irrapxlem4  43414  irrapxlem5  43415  pellexlem2  43419  pellexlem6  43423  pell1234qrne0  43442  pell1234qrreccl  43443  pell1234qrmulcl  43444  pell1234qrdich  43450  pell14qrdich  43458  pell1qrge1  43459  pell1qr1  43460  pell14qrgapw  43465  rmxyneg  43509  rmxm1  43523  rmxluc  43525  rmxdbl  43528  jm2.19lem1  43578  jm2.27c  43596  relexpmulnn  44297  relexpmulg  44298  inductionexd  44743  hashnzfzclim  44896  bcccl  44913  bcc0  44914  bccp1k  44915  bccm1k  44916  binomcxplemwb  44922  fsumnncl  46146  mccllem  46171  clim1fr1  46175  sumnnodd  46204  dvsinexp  46483  dvxpaek  46512  dvnxpaek  46514  dvnprodlem2  46519  itgsinexplem1  46526  itgsinexp  46527  stoweidlem1  46573  stoweidlem11  46583  stoweidlem25  46597  stoweidlem26  46598  stoweidlem34  46606  stoweidlem37  46609  stoweidlem38  46610  stoweidlem42  46614  wallispi2lem1  46643  wallispi2  46645  stirlinglem4  46649  stirlinglem5  46650  stirlinglem10  46655  stirlinglem15  46660  dirkertrigeqlem3  46672  dirkertrigeq  46673  dirkercncflem2  46676  dirkercncflem4  46678  fourierdlem11  46690  fourierdlem15  46694  fourierdlem79  46757  fourierdlem83  46761  sqwvfourb  46801  etransclem14  46820  etransclem15  46821  etransclem20  46826  etransclem21  46827  etransclem22  46828  etransclem23  46829  etransclem24  46830  etransclem25  46831  etransclem28  46834  etransclem31  46837  etransclem32  46838  etransclem33  46839  etransclem34  46840  etransclem35  46841  etransclem38  46844  etransclem41  46847  etransclem44  46850  etransclem45  46851  etransclem47  46853  etransclem48  46854  nnfoctbdjlem  47027  deccarry  47903  iccpartgtprec  48024  fmtnoodd  48140  fmtnorec2lem  48149  fmtnorec2  48150  fmtnodvds  48151  goldbachthlem2  48153  fmtnorec3  48155  fmtnorec4  48156  fmtnoprmfac1lem  48171  fmtnoprmfac1  48172  fmtnoprmfac2lem1  48173  fmtnoprmfac2  48174  2pwp1prm  48196  sfprmdvdsmersenne  48210  lighneallem4b  48216  lighneal  48218  proththdlem  48220  proththd  48221  ppivalnnprm  48232  oexpnegALTV  48297  perfectALTVlem1  48341  perfectALTVlem2  48342  perfectALTV  48343  nnpw2pmod  49214  nnolog2flm1  49221  blennn0em1  49222  blengt1fldiv2p1  49224  nn0sumshdiglemB  49251  amgmlemALT  50432