Theorem nncnd 12279

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℂcc 11150  ℕcn 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-nn 12264

This theorem is referenced by:  nneo  12699  facdiv  14322  facndiv  14323  faclbnd  14325  faclbnd5  14333  faclbnd6  14334  facubnd  14335  facavg  14336  bccmpl  14344  bcn0  14345  bcn1  14348  bcm1k  14350  bcp1n  14351  bcp1nk  14352  bcval5  14353  bcpasc  14356  permnn  14361  hashf1  14492  hashfac  14493  relexpaddnn  15086  binom11  15864  binom1dif  15865  climcndslem2  15882  arisum2  15893  trireciplem  15894  trirecip  15895  geo2sum  15905  geo2lim  15907  fprodfac  16005  risefacfac  16067  fallfacfwd  16068  fallfacval4  16075  bcfallfac  16076  fallfacfac  16077  bpolycl  16084  bpolysum  16085  bpolydiflem  16086  fsumkthpow  16088  eftcl  16105  eftabs  16107  efcllem  16109  ege2le3  16122  efcj  16124  efaddlem  16125  eftlub  16141  eirrlem  16236  sqrt2irrlem  16280  oexpneg  16378  pwp1fsum  16424  bitsp1  16464  bitsfzolem  16467  bitsfzo  16468  bitsmod  16469  bitscmp  16471  bitsinv1lem  16474  bitsinv1  16475  2ebits  16480  bitsinvp1  16482  sadcaddlem  16490  sadadd3  16494  bitsres  16506  bitsuz  16507  bitsshft  16508  dvdsgcdidd  16570  mulgcd  16581  rplpwr  16591  sqgcd  16595  expgcd  16596  nn0expgcd  16597  lcmgcdlem  16639  3lcm2e6woprm  16648  coprmprod  16694  coprmproddvdslem  16695  cncongr1  16700  cncongr2  16701  prmind2  16718  isprm5  16740  divgcdodd  16743  prmdvdsexpr  16750  qmuldeneqnum  16780  divnumden  16781  qnumgt0  16783  numdensq  16787  numdenexp  16793  hashdvds  16808  phiprmpw  16809  prmdiv  16818  prmdivdiv  16820  phisum  16823  modprm0  16838  pythagtriplem4  16852  pythagtriplem6  16854  pythagtriplem7  16855  pythagtriplem14  16861  pythagtriplem15  16862  pythagtriplem19  16866  pythagtrip  16867  pcprendvds2  16874  pcpre1  16875  pcpremul  16876  pceulem  16878  pcdiv  16885  pcqmul  16886  pcelnn  16903  pcid  16906  pc2dvds  16912  dvdsprmpweqnn  16918  dvdsprmpweqle  16919  pcaddlem  16921  pcadd  16922  pcfaclem  16931  qexpz  16934  expnprm  16935  oddprmdvds  16936  prmpwdvds  16937  pockthlem  16938  pockthg  16939  infpnlem1  16943  prmreclem1  16949  prmreclem2  16950  prmreclem3  16951  prmreclem4  16952  prmreclem6  16954  4sqlem6  16976  4sqlem7  16977  4sqlem10  16980  mul4sqlem  16986  4sqlem11  16988  4sqlem12  16989  4sqlem14  16991  4sqlem17  16994  4sqlem18  16995  vdwlem1  17014  vdwlem2  17015  vdwlem3  17016  vdwlem5  17018  vdwlem6  17019  vdwlem8  17021  vdwlem9  17022  vdwlem10  17023  vdwlem12  17025  ramub1lem2  17060  ramcl  17062  prmop1  17071  prmdvdsprmo  17075  prmgaplem7  17090  prmgaplem8  17091  gsumsgrpccat  18865  mulgnndir  19133  mulgnnass  19139  psgnunilem5  19526  odf1o2  19605  pgp0  19628  sylow1lem1  19630  odcau  19636  sylow2blem3  19654  sylow3lem3  19661  sylow3lem4  19662  gexexlem  19884  ablfacrp2  20101  ablfac1lem  20102  ablfac1eu  20107  pgpfac1lem3a  20110  pgpfac1lem3  20111  fincygsubgodexd  20147  zringlpirlem3  21492  znrrg  21601  cpmadugsumlemF  22897  lebnumlem3  25008  ovollb2lem  25536  ovolunlem1a  25544  ovolunlem1  25545  uniioombllem3  25633  uniioombllem4  25634  dyaddisjlem  25643  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  itgpowd  26105  dgrcolem1  26327  vieta1lem1  26366  vieta1lem2  26367  elqaalem2  26376  elqaalem3  26377  aalioulem1  26388  aaliou3lem2  26399  aaliou3lem8  26401  aaliou3lem6  26404  aaliou3lem9  26406  taylfvallem1  26412  tayl0  26417  taylply2  26423  taylply2OLD  26424  taylply  26425  dvtaylp  26426  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  pserdvlem2  26486  advlogexp  26711  cxpmul2  26745  cxpeq  26814  rtprmirr  26817  atantayl3  26996  leibpi  26999  log2cnv  27001  log2tlbnd  27002  birthdaylem2  27009  birthdaylem3  27010  amgmlem  27047  amgm  27048  emcllem5  27057  fsumharmonic  27069  zetacvg  27072  dmgmdivn0  27085  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamgulm2  27093  lgamcvg2  27112  gamcvg  27113  gamcvg2lem  27116  facgam  27123  wilthlem1  27125  wilthlem2  27126  wilthlem3  27127  wilthimp  27129  basellem1  27138  basellem2  27139  basellem3  27140  basellem4  27141  basellem5  27142  basellem8  27145  vmaprm  27174  sgmval2  27200  0sgm  27201  sgmf  27202  vma1  27223  fsumdvdsdiaglem  27240  dvdsflf1o  27244  muinv  27250  mpodvdsmulf1o  27251  dvdsmulf1o  27253  sgmppw  27255  1sgmprm  27257  1sgm2ppw  27258  sgmmul  27259  chtublem  27269  fsumvma2  27272  chpchtsum  27277  logfaclbnd  27280  logexprlim  27283  mersenne  27285  perfect1  27286  perfectlem1  27287  perfectlem2  27288  perfect  27289  dchrsum2  27326  dchrhash  27329  bcmono  27335  bcp1ctr  27337  bclbnd  27338  bposlem1  27342  bposlem2  27343  bposlem3  27344  bposlem5  27346  bposlem6  27347  lgsval2lem  27365  lgsqrlem2  27405  gausslemma2dlem6  27430  gausslemma2dlem7  27431  gausslemma2d  27432  lgseisenlem1  27433  lgseisenlem4  27436  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  lgsquad2  27444  m1lgs  27446  2sqlem3  27478  2sqlem4  27479  chebbnd1lem1  27527  chebbnd1  27530  rplogsumlem1  27542  rplogsumlem2  27543  rpvmasumlem  27545  dchrisumlem1  27547  dchrmusum2  27552  dchrvmasumlem1  27553  dchrvmasum2lem  27554  dchrvmasum2if  27555  dchrvmasumlem2  27556  dchrvmasumlem3  27557  dchrvmasumiflem1  27559  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0fno1  27569  rpvmasum2  27570  rplogsum  27585  mulogsumlem  27589  mulogsum  27590  mulog2sumlem2  27593  vmalogdivsum2  27596  vmalogdivsum  27597  2vmadivsumlem  27598  logsqvma  27600  selberglem2  27604  selberglem3  27605  selberg  27606  selberg2lem  27608  logdivbnd  27614  selberg3lem1  27615  selberg4lem1  27618  pntrsumo1  27623  pntrsumbnd2  27625  selberg3r  27627  selberg4r  27628  selberg34r  27629  pntsval2  27634  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntrlog2bndlem6  27641  pntpbnd1  27644  pntpbnd2  27645  pntlemg  27656  pntlemn  27658  pntlemf  27663  pnt  27672  padicabvf  27689  ostth2lem2  27692  ostth3  27696  fusgrhashclwwlkn  30107  eucrct2eupth  30273  nrt2irr  30501  numdenneg  32820  ltesubnnd  32828  chnub  32985  1arithidomlem2  33543  1arithidom  33544  zringfrac  33561  1smat1  33764  madjusmdetlem2  33788  madjusmdetlem4  33790  qqhnm  33952  oddpwdc  34335  eulerpartlemsv2  34339  eulerpartlems  34341  eulerpartlemsv3  34342  eulerpartlemgc  34343  eulerpartlemv  34345  eulerpartlemgs2  34361  fibp1  34382  ballotlemfc0  34473  ballotlemfcc  34474  signsvtn0  34563  reprpmtf1o  34619  vtscl  34631  hgt750lemb  34649  tgoldbachgt  34656  subfacp1lem1  35163  subfacp1lem5  35168  subfacval2  35171  subfaclim  35172  cvmliftlem2  35270  cvmliftlem7  35275  cvmliftlem10  35278  cvmliftlem11  35279  cvmliftlem13  35280  bcm1nt  35716  bcprod  35717  iprodgam  35721  faclimlem1  35722  faclimlem2  35723  faclim2  35727  nn0prpwlem  36304  nn0prpw  36305  knoppcnlem10  36484  knoppndvlem16  36509  poimirlem1  37607  poimirlem2  37608  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  nnproddivdvdsd  41981  lcmfunnnd  41993  lcmineqlem3  42012  lcmineqlem4  42013  lcmineqlem6  42015  lcmineqlem8  42017  lcmineqlem10  42019  lcmineqlem11  42020  lcmineqlem12  42021  lcmineqlem16  42025  lcmineqlem18  42027  lcmineqlem23  42032  dvrelogpow2b  42049  aks4d1p1p2  42051  aks4d1p1  42057  aks4d1p8  42068  primrootsunit1  42078  primrootscoprmpow  42080  posbezout  42081  primrootscoprbij  42083  primrootspoweq0  42087  aks6d1c1p3  42091  aks6d1c1p8  42096  aks6d1c2p2  42100  hashscontpow1  42102  2np3bcnp1  42125  2ap1caineq  42126  sticksstones10  42136  sticksstones12a  42138  sticksstones16  42143  sticksstones22  42149  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7  42165  unitscyglem2  42177  unitscyglem4  42179  unitscyglem5  42180  aks5lem8  42182  metakunt8  42193  metakunt15  42200  metakunt16  42201  metakunt20  42205  metakunt28  42213  metakunt30  42215  nnadddir  42283  nnmul1com  42284  nnmulcom  42285  oddnumth  42323  nicomachus  42324  zaddcom  42458  fltabcoprmex  42625  fltaccoprm  42626  fltbccoprm  42627  fltne  42630  flt4lem3  42634  flt4lem5elem  42637  flt4lem5a  42638  flt4lem5b  42639  flt4lem5c  42640  flt4lem5d  42641  flt4lem5e  42642  flt4lem5f  42643  flt4lem6  42644  flt4lem7  42645  nna4b4nsq  42646  fltltc  42647  fltnltalem  42648  fltnlta  42649  irrapxlem4  42812  irrapxlem5  42813  pellexlem2  42817  pellexlem6  42821  pell1234qrne0  42840  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell1234qrdich  42848  pell14qrdich  42856  pell1qrge1  42857  pell1qr1  42858  pell14qrgapw  42863  rmxyneg  42908  rmxm1  42922  rmxluc  42924  rmxdbl  42927  jm2.19lem1  42977  jm2.27c  42995  relexpmulnn  43698  relexpmulg  43699  inductionexd  44144  hashnzfzclim  44317  bcccl  44334  bcc0  44335  bccp1k  44336  bccm1k  44337  binomcxplemwb  44343  fsumnncl  45527  mccllem  45552  clim1fr1  45556  sumnnodd  45585  dvsinexp  45866  dvxpaek  45895  dvnxpaek  45897  dvnprodlem2  45902  itgsinexplem1  45909  itgsinexp  45910  stoweidlem1  45956  stoweidlem11  45966  stoweidlem25  45980  stoweidlem26  45981  stoweidlem34  45989  stoweidlem37  45992  stoweidlem38  45993  stoweidlem42  45997  wallispi2lem1  46026  wallispi2  46028  stirlinglem4  46032  stirlinglem5  46033  stirlinglem10  46038  stirlinglem15  46043  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem11  46073  fourierdlem15  46077  fourierdlem79  46140  fourierdlem83  46144  sqwvfourb  46184  etransclem14  46203  etransclem15  46204  etransclem20  46209  etransclem21  46210  etransclem22  46211  etransclem23  46212  etransclem24  46213  etransclem25  46214  etransclem28  46217  etransclem31  46220  etransclem32  46221  etransclem33  46222  etransclem34  46223  etransclem35  46224  etransclem38  46227  etransclem41  46230  etransclem44  46233  etransclem45  46234  etransclem47  46236  etransclem48  46237  nnfoctbdjlem  46410  deccarry  47260  iccpartgtprec  47344  fmtnoodd  47457  fmtnorec2lem  47466  fmtnorec2  47467  fmtnodvds  47468  goldbachthlem2  47470  fmtnorec3  47472  fmtnorec4  47473  fmtnoprmfac1lem  47488  fmtnoprmfac1  47489  fmtnoprmfac2lem1  47490  fmtnoprmfac2  47491  2pwp1prm  47513  sfprmdvdsmersenne  47527  lighneallem4b  47533  lighneal  47535  proththdlem  47537  proththd  47538  oexpnegALTV  47601  perfectALTVlem1  47645  perfectALTVlem2  47646  perfectALTV  47647  nnpw2pmod  48432  nnolog2flm1  48439  blennn0em1  48440  blengt1fldiv2p1  48442  nn0sumshdiglemB  48469  amgmlemALT  49033