Theorem nncnd 12378

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11225  ℕcn 12362

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775  ax-1cn 11285  ax-addcl 11287

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-nn 12363

This theorem is used by:  nnadddir  12421  nnmul1com  12422  nnmulcom  12423  nneo  12810  facdiv  14458  facndiv  14459  faclbnd  14461  faclbnd5  14469  faclbnd6  14470  facubnd  14471  facavg  14472  bccmpl  14480  bcn0  14481  bcn1  14484  bcm1k  14486  bcp1n  14487  bcp1nk  14488  bcval5  14489  bcpasc  14492  permnn  14497  hashf1  14629  hashfac  14630  relexpaddnn  15233  binom11  16030  binom1dif  16031  climcndslem2  16048  arisum2  16059  trireciplem  16060  trirecip  16061  geo2sum  16071  geo2lim  16073  fprodfac  16169  risefacfac  16230  fallfacfwd  16231  fallfacval4  16238  bcfallfac  16239  fallfacfac  16240  bpolycl  16247  bpolysum  16248  bpolydiflem  16249  fsumkthpow  16251  eftcl  16268  eftabs  16270  efcllem  16272  ege2le3  16285  efcj  16287  efaddlem  16288  eftlub  16306  eirrlem  16401  sqrt2irrlem  16445  oexpneg  16544  pwp1fsum  16590  bitsp1  16630  bitsfzolem  16633  bitsfzo  16634  bitsmod  16635  bitscmp  16637  bitsinv1lem  16640  bitsinv1  16641  2ebits  16646  bitsinvp1  16648  sadcaddlem  16656  sadadd3  16660  bitsres  16672  bitsuz  16673  bitsshft  16674  dvdsgcdidd  16739  mulgcd  16750  rplpwr  16761  sqgcd  16765  expgcd  16766  nn0expgcd  16767  lcmgcdlem  16810  3lcm2e6woprm  16819  coprmprod  16865  coprmproddvdslem  16866  cncongr1  16871  cncongr2  16872  prmind2  16889  isprm5  16912  divgcdodd  16915  prmdvdsexpr  16922  qmuldeneqnum  16952  divnumden  16953  qnumgt0  16955  numdensq  16959  numdenexp  16966  hashdvds  16981  phiprmpw  16982  prmdiv  16991  prmdivdiv  16993  phisum  16997  modprm0  17012  pythagtriplem4  17026  pythagtriplem6  17028  pythagtriplem7  17029  pythagtriplem14  17035  pythagtriplem15  17036  pythagtriplem19  17040  pythagtrip  17041  pcprendvds2  17048  pcpre1  17049  pcpremul  17050  pceulem  17052  pcdiv  17059  pcqmul  17060  pcelnn  17077  pcid  17080  pc2dvds  17086  dvdsprmpweqnn  17092  dvdsprmpweqle  17093  pcaddlem  17095  pcadd  17096  pcfaclem  17105  qexpz  17108  expnprm  17109  oddprmdvds  17110  prmpwdvds  17111  pockthlem  17112  pockthg  17113  infpnlem1  17117  prmreclem1  17123  prmreclem2  17124  prmreclem3  17125  prmreclem4  17126  prmreclem6  17128  4sqlem6  17150  4sqlem7  17151  4sqlem10  17154  mul4sqlem  17160  4sqlem11  17162  4sqlem12  17163  4sqlem14  17165  4sqlem17  17168  4sqlem18  17169  vdwlem1  17188  vdwlem2  17189  vdwlem3  17190  vdwlem5  17192  vdwlem6  17193  vdwlem8  17195  vdwlem9  17196  vdwlem10  17197  vdwlem12  17199  ramub1lem2  17234  ramcl  17236  prmop1  17245  prmdvdsprmo  17249  prmgaplem7  17264  prmgaplem8  17265  chnub  18825  gsumsgrpccat  19065  mulgnndir  19342  mulgnnass  19348  psgnunilem5  19738  odf1o2  19817  pgp0  19840  sylow1lem1  19842  odcau  19848  sylow2blem3  19866  sylow3lem3  19873  sylow3lem4  19874  gexexlem  20096  ablfacrp2  20313  ablfac1lem  20314  ablfac1eu  20319  pgpfac1lem3a  20322  pgpfac1lem3  20323  fincygsubgodexd  20359  zringlpirlem3  21800  znrrg  21901  psdpw  22521  cpmadugsumlemF  23224  lebnumlem3  25314  ovollb2lem  25839  ovolunlem1a  25847  ovolunlem1  25848  uniioombllem3  25936  uniioombllem4  25937  dyaddisjlem  25946  mbfi1fseqlem3  26068  mbfi1fseqlem4  26069  itgpowd  26400  dgrcolem1  26622  vieta1lem1  26663  vieta1lem2  26664  elqaalem2  26673  elqaalem3  26674  aalioulem1  26689  aaliou3lem2  26700  aaliou3lem8  26702  aaliou3lem6  26705  aaliou3lem9  26707  taylfvallem1  26714  tayl0  26719  taylply2  26725  taylply  26726  dvtaylp  26727  taylthlem1  26730  taylthlem2  26731  pserdvlem2  26785  advlogexp  27013  cxpmul2  27047  cxpeq  27115  rtprmirr  27118  atantayl3  27297  leibpi  27300  log2cnv  27302  log2tlbnd  27303  birthdaylem2  27310  birthdaylem3  27311  amgmlem  27347  amgm  27348  emcllem5  27357  fsumharmonic  27369  zetacvg  27372  dmgmdivn0  27385  lgamgulmlem3  27388  lgamgulmlem4  27389  lgamgulmlem5  27390  lgamgulmlem6  27391  lgamgulm2  27393  lgamcvg2  27412  gamcvg  27413  gamcvg2lem  27416  facgam  27423  wilthlem1  27425  wilthlem2  27426  wilthlem3  27427  wilthimp  27429  basellem1  27438  basellem2  27439  basellem3  27440  basellem4  27441  basellem5  27442  basellem8  27445  vmaprm  27474  sgmval2  27500  0sgm  27501  sgmf  27502  vma1  27523  fsumdvdsdiaglem  27540  dvdsflf1o  27544  muinv  27550  mpodvdsmulf1o  27551  dvdsmulf1o  27553  sgmppw  27554  1sgmprm  27556  1sgm2ppw  27557  sgmmul  27558  chtublem  27568  fsumvma2  27571  chpchtsum  27576  logfaclbnd  27579  logexprlim  27582  mersenne  27584  perfect1  27585  perfectlem1  27586  perfectlem2  27587  perfect  27588  dchrsum2  27625  dchrhash  27628  bcmono  27634  bcp1ctr  27636  bclbnd  27637  bposlem1  27641  bposlem2  27642  bposlem3  27643  bposlem5  27645  bposlem6  27646  lgsval2lem  27664  lgsqrlem2  27704  gausslemma2dlem6  27729  gausslemma2dlem7  27730  gausslemma2d  27731  lgseisenlem1  27732  lgseisenlem4  27735  lgsquadlem1  27737  lgsquadlem2  27738  lgsquadlem3  27739  lgsquad2  27743  m1lgs  27745  2sqlem3  27777  2sqlem4  27778  chebbnd1lem1  27826  chebbnd1  27829  rplogsumlem1  27841  rplogsumlem2  27842  rpvmasumlem  27844  dchrisumlem1  27846  dchrmusum2  27851  dchrvmasumlem1  27852  dchrvmasum2lem  27853  dchrvmasum2if  27854  dchrvmasumlem2  27855  dchrvmasumlem3  27856  dchrvmasumiflem1  27858  dchrisum0flblem1  27865  dchrisum0flblem2  27866  dchrisum0fno1  27868  rpvmasum2  27869  rplogsum  27884  mulogsumlem  27888  mulogsum  27889  mulog2sumlem2  27892  vmalogdivsum2  27895  vmalogdivsum  27896  2vmadivsumlem  27897  logsqvma  27899  selberglem2  27903  selberglem3  27904  selberg  27905  selberg2lem  27907  logdivbnd  27913  selberg3lem1  27914  selberg4lem1  27917  pntrsumo1  27922  pntrsumbnd2  27924  selberg3r  27926  selberg4r  27927  selberg34r  27928  pntsval2  27933  pntrlog2bndlem2  27935  pntrlog2bndlem4  27937  pntrlog2bndlem6  27940  pntpbnd1  27943  pntpbnd2  27944  pntlemg  27955  pntlemn  27957  pntlemf  27962  pnt  27971  padicabvf  27988  ostth2lem2  27991  ostth3  27995  fltabcoprmex  28001  fltaccoprm  28002  fltbccoprm  28003  fltne  28005  flt4lem3  28008  flt4lem5elem  28011  flt4lem5a  28012  flt4lem5b  28013  flt4lem5c  28014  flt4lem5d  28015  flt4lem5e  28016  flt4lem5f  28017  flt4lem6  28018  flt4lem7  28019  nna4b4nsq  28020  flt4  28021  flt4ALT  28022  fltoprm  28025  fusgrhashclwwlkn  30700  eucrct2eupth  30876  nrt2irr  31104  elq2  33473  numdenneg  33476  ltesubnnd  33484  2exple2exp  33495  oexpled  33497  gsummptp1  33688  1arithidomlem2  34138  1arithidom  34139  zringfrac  34156  cos9thpiminplylem1  34484  cos9thpiminplylem2  34485  1smat1  34506  madjusmdetlem2  34530  madjusmdetlem4  34532  qqhnm  34692  oddpwdc  35056  eulerpartlemsv2  35060  eulerpartlems  35062  eulerpartlemsv3  35063  eulerpartlemgc  35064  eulerpartlemv  35066  eulerpartlemgs2  35082  fibp1  35103  ballotlemfc0  35195  ballotlemfcc  35196  signsvtn0  35269  reprpmtf1o  35325  vtscl  35337  hgt750lemb  35355  tgoldbachgt  35362  subfacp1lem1  36111  subfacp1lem5  36116  subfacval2  36119  subfaclim  36120  cvmliftlem2  36218  cvmliftlem7  36223  cvmliftlem10  36226  cvmliftlem11  36227  cvmliftlem13  36228  bcm1nt  36680  bcprod  36681  iprodgam  36685  faclimlem1  36686  faclimlem2  36687  faclim2  36691  nn0prpwlem  37288  nn0prpw  37289  knoppcnlem10  37546  knoppndvlem16  37571  poimirlem1  38731  poimirlem2  38732  poimirlem6  38736  poimirlem7  38737  poimirlem8  38738  poimirlem9  38739  poimirlem10  38740  poimirlem11  38741  poimirlem12  38742  poimirlem13  38743  poimirlem15  38745  poimirlem16  38746  poimirlem17  38747  poimirlem18  38748  poimirlem19  38749  poimirlem20  38750  poimirlem21  38751  poimirlem22  38752  poimirlem23  38753  poimirlem24  38754  poimirlem25  38755  poimirlem26  38756  poimirlem27  38757  poimirlem31  38761  nnproddivdvdsd  43242  lcmfunnnd  43254  lcmineqlem3  43273  lcmineqlem4  43274  lcmineqlem6  43276  lcmineqlem8  43278  lcmineqlem10  43280  lcmineqlem11  43281  lcmineqlem12  43282  lcmineqlem16  43286  lcmineqlem18  43288  lcmineqlem23  43293  dvrelogpow2b  43310  aks4d1p1p2  43312  aks4d1p1  43318  aks4d1p8  43329  primrootsunit1  43339  primrootscoprmpow  43341  posbezout  43342  primrootscoprbij  43344  primrootspoweq0  43348  aks6d1c1p3  43352  aks6d1c1p8  43357  aks6d1c2p2  43361  hashscontpow1  43363  2np3bcnp1  43386  2ap1caineq  43387  sticksstones10  43397  sticksstones12a  43399  sticksstones16  43404  sticksstones22  43410  bcled  43420  bcle2d  43421  aks6d1c7lem1  43422  aks6d1c7  43426  unitscyglem2  43438  unitscyglem4  43440  unitscyglem5  43441  aks5lem8  43443  oddnumth  43561  nicomachus  43562  zaddcom  43721  fltltc  43865  fltnltalem  43866  fltnlta  43867  irrapxlem4  44025  irrapxlem5  44026  pellexlem2  44030  pellexlem6  44034  pell1234qrne0  44053  pell1234qrreccl  44054  pell1234qrmulcl  44055  pell1234qrdich  44061  pell14qrdich  44069  pell1qrge1  44070  pell1qr1  44071  pell14qrgapw  44076  rmxyneg  44120  rmxm1  44134  rmxluc  44136  rmxdbl  44139  jm2.19lem1  44189  jm2.27c  44207  relexpmulnn  44901  relexpmulg  44902  inductionexd  45347  hashnzfzclim  45498  bcccl  45515  bcc0  45516  bccp1k  45517  bccm1k  45518  binomcxplemwb  45524  fsumnncl  46789  mccllem  46814  clim1fr1  46818  sumnnodd  46847  dvsinexp  47126  dvxpaek  47155  dvnxpaek  47157  dvnprodlem2  47162  itgsinexplem1  47169  itgsinexp  47170  stoweidlem1  47216  stoweidlem11  47226  stoweidlem25  47240  stoweidlem26  47241  stoweidlem34  47249  stoweidlem37  47252  stoweidlem38  47253  stoweidlem42  47257  wallispi2lem1  47286  wallispi2  47288  stirlinglem4  47292  stirlinglem5  47293  stirlinglem10  47298  stirlinglem15  47303  dirkertrigeqlem3  47315  dirkertrigeq  47316  dirkercncflem2  47319  dirkercncflem4  47321  fourierdlem11  47333  fourierdlem15  47337  fourierdlem79  47400  fourierdlem83  47404  sqwvfourb  47444  etransclem14  47463  etransclem15  47464  etransclem20  47469  etransclem21  47470  etransclem22  47471  etransclem23  47472  etransclem24  47473  etransclem25  47474  etransclem28  47477  etransclem31  47480  etransclem32  47481  etransclem33  47482  etransclem34  47483  etransclem35  47484  etransclem38  47487  etransclem41  47490  etransclem44  47493  etransclem45  47494  etransclem47  47496  etransclem48  47497  nnfoctbdjlem  47670  deccarry  48586  iccpartgtprec  48707  fmtnoodd  48823  fmtnorec2lem  48832  fmtnorec2  48833  fmtnodvds  48834  goldbachthlem2  48836  fmtnorec3  48838  fmtnorec4  48839  fmtnoprmfac1lem  48854  fmtnoprmfac1  48855  fmtnoprmfac2lem1  48856  fmtnoprmfac2  48857  2pwp1prm  48879  sfprmdvdsmersenne  48893  lighneallem4b  48899  lighneal  48901  proththdlem  48903  proththd  48904  ppivalnnprm  48915  oexpnegALTV  48980  perfectALTVlem1  49024  perfectALTVlem2  49025  perfectALTV  49026  nnpw2pmod  49900  nnolog2flm1  49907  blennn0em1  49908  blengt1fldiv2p1  49910  nn0sumshdiglemB  49937  amgmlemALT  51268