Theorem nncnd 12282

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℂcc 11153  ℕcn 12266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267

This theorem is referenced by:  nneo  12702  facdiv  14326  facndiv  14327  faclbnd  14329  faclbnd5  14337  faclbnd6  14338  facubnd  14339  facavg  14340  bccmpl  14348  bcn0  14349  bcn1  14352  bcm1k  14354  bcp1n  14355  bcp1nk  14356  bcval5  14357  bcpasc  14360  permnn  14365  hashf1  14496  hashfac  14497  relexpaddnn  15090  binom11  15868  binom1dif  15869  climcndslem2  15886  arisum2  15897  trireciplem  15898  trirecip  15899  geo2sum  15909  geo2lim  15911  fprodfac  16009  risefacfac  16071  fallfacfwd  16072  fallfacval4  16079  bcfallfac  16080  fallfacfac  16081  bpolycl  16088  bpolysum  16089  bpolydiflem  16090  fsumkthpow  16092  eftcl  16109  eftabs  16111  efcllem  16113  ege2le3  16126  efcj  16128  efaddlem  16129  eftlub  16145  eirrlem  16240  sqrt2irrlem  16284  oexpneg  16382  pwp1fsum  16428  bitsp1  16468  bitsfzolem  16471  bitsfzo  16472  bitsmod  16473  bitscmp  16475  bitsinv1lem  16478  bitsinv1  16479  2ebits  16484  bitsinvp1  16486  sadcaddlem  16494  sadadd3  16498  bitsres  16510  bitsuz  16511  bitsshft  16512  dvdsgcdidd  16574  mulgcd  16585  rplpwr  16595  sqgcd  16599  expgcd  16600  nn0expgcd  16601  lcmgcdlem  16643  3lcm2e6woprm  16652  coprmprod  16698  coprmproddvdslem  16699  cncongr1  16704  cncongr2  16705  prmind2  16722  isprm5  16744  divgcdodd  16747  prmdvdsexpr  16754  qmuldeneqnum  16784  divnumden  16785  qnumgt0  16787  numdensq  16791  numdenexp  16797  hashdvds  16812  phiprmpw  16813  prmdiv  16822  prmdivdiv  16824  phisum  16828  modprm0  16843  pythagtriplem4  16857  pythagtriplem6  16859  pythagtriplem7  16860  pythagtriplem14  16866  pythagtriplem15  16867  pythagtriplem19  16871  pythagtrip  16872  pcprendvds2  16879  pcpre1  16880  pcpremul  16881  pceulem  16883  pcdiv  16890  pcqmul  16891  pcelnn  16908  pcid  16911  pc2dvds  16917  dvdsprmpweqnn  16923  dvdsprmpweqle  16924  pcaddlem  16926  pcadd  16927  pcfaclem  16936  qexpz  16939  expnprm  16940  oddprmdvds  16941  prmpwdvds  16942  pockthlem  16943  pockthg  16944  infpnlem1  16948  prmreclem1  16954  prmreclem2  16955  prmreclem3  16956  prmreclem4  16957  prmreclem6  16959  4sqlem6  16981  4sqlem7  16982  4sqlem10  16985  mul4sqlem  16991  4sqlem11  16993  4sqlem12  16994  4sqlem14  16996  4sqlem17  16999  4sqlem18  17000  vdwlem1  17019  vdwlem2  17020  vdwlem3  17021  vdwlem5  17023  vdwlem6  17024  vdwlem8  17026  vdwlem9  17027  vdwlem10  17028  vdwlem12  17030  ramub1lem2  17065  ramcl  17067  prmop1  17076  prmdvdsprmo  17080  prmgaplem7  17095  prmgaplem8  17096  gsumsgrpccat  18853  mulgnndir  19121  mulgnnass  19127  psgnunilem5  19512  odf1o2  19591  pgp0  19614  sylow1lem1  19616  odcau  19622  sylow2blem3  19640  sylow3lem3  19647  sylow3lem4  19648  gexexlem  19870  ablfacrp2  20087  ablfac1lem  20088  ablfac1eu  20093  pgpfac1lem3a  20096  pgpfac1lem3  20097  fincygsubgodexd  20133  zringlpirlem3  21475  znrrg  21584  psdpw  22174  cpmadugsumlemF  22882  lebnumlem3  24995  ovollb2lem  25523  ovolunlem1a  25531  ovolunlem1  25532  uniioombllem3  25620  uniioombllem4  25621  dyaddisjlem  25630  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  itgpowd  26091  dgrcolem1  26313  vieta1lem1  26352  vieta1lem2  26353  elqaalem2  26362  elqaalem3  26363  aalioulem1  26374  aaliou3lem2  26385  aaliou3lem8  26387  aaliou3lem6  26390  aaliou3lem9  26392  taylfvallem1  26398  tayl0  26403  taylply2  26409  taylply2OLD  26410  taylply  26411  dvtaylp  26412  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  pserdvlem2  26472  advlogexp  26697  cxpmul2  26731  cxpeq  26800  rtprmirr  26803  atantayl3  26982  leibpi  26985  log2cnv  26987  log2tlbnd  26988  birthdaylem2  26995  birthdaylem3  26996  amgmlem  27033  amgm  27034  emcllem5  27043  fsumharmonic  27055  zetacvg  27058  dmgmdivn0  27071  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamgulm2  27079  lgamcvg2  27098  gamcvg  27099  gamcvg2lem  27102  facgam  27109  wilthlem1  27111  wilthlem2  27112  wilthlem3  27113  wilthimp  27115  basellem1  27124  basellem2  27125  basellem3  27126  basellem4  27127  basellem5  27128  basellem8  27131  vmaprm  27160  sgmval2  27186  0sgm  27187  sgmf  27188  vma1  27209  fsumdvdsdiaglem  27226  dvdsflf1o  27230  muinv  27236  mpodvdsmulf1o  27237  dvdsmulf1o  27239  sgmppw  27241  1sgmprm  27243  1sgm2ppw  27244  sgmmul  27245  chtublem  27255  fsumvma2  27258  chpchtsum  27263  logfaclbnd  27266  logexprlim  27269  mersenne  27271  perfect1  27272  perfectlem1  27273  perfectlem2  27274  perfect  27275  dchrsum2  27312  dchrhash  27315  bcmono  27321  bcp1ctr  27323  bclbnd  27324  bposlem1  27328  bposlem2  27329  bposlem3  27330  bposlem5  27332  bposlem6  27333  lgsval2lem  27351  lgsqrlem2  27391  gausslemma2dlem6  27416  gausslemma2dlem7  27417  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem4  27422  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  lgsquad2  27430  m1lgs  27432  2sqlem3  27464  2sqlem4  27465  chebbnd1lem1  27513  chebbnd1  27516  rplogsumlem1  27528  rplogsumlem2  27529  rpvmasumlem  27531  dchrisumlem1  27533  dchrmusum2  27538  dchrvmasumlem1  27539  dchrvmasum2lem  27540  dchrvmasum2if  27541  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0fno1  27555  rpvmasum2  27556  rplogsum  27571  mulogsumlem  27575  mulogsum  27576  mulog2sumlem2  27579  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  logsqvma  27586  selberglem2  27590  selberglem3  27591  selberg  27592  selberg2lem  27594  logdivbnd  27600  selberg3lem1  27601  selberg4lem1  27604  pntrsumo1  27609  pntrsumbnd2  27611  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntsval2  27620  pntrlog2bndlem2  27622  pntrlog2bndlem4  27624  pntrlog2bndlem6  27627  pntpbnd1  27630  pntpbnd2  27631  pntlemg  27642  pntlemn  27644  pntlemf  27649  pnt  27658  padicabvf  27675  ostth2lem2  27678  ostth3  27682  fusgrhashclwwlkn  30098  eucrct2eupth  30264  nrt2irr  30492  numdenneg  32816  ltesubnnd  32824  2exple2exp  32834  chnub  33002  1arithidomlem2  33564  1arithidom  33565  zringfrac  33582  1smat1  33803  madjusmdetlem2  33827  madjusmdetlem4  33829  qqhnm  33991  oddpwdc  34356  eulerpartlemsv2  34360  eulerpartlems  34362  eulerpartlemsv3  34363  eulerpartlemgc  34364  eulerpartlemv  34366  eulerpartlemgs2  34382  fibp1  34403  ballotlemfc0  34495  ballotlemfcc  34496  signsvtn0  34585  reprpmtf1o  34641  vtscl  34653  hgt750lemb  34671  tgoldbachgt  34678  subfacp1lem1  35184  subfacp1lem5  35189  subfacval2  35192  subfaclim  35193  cvmliftlem2  35291  cvmliftlem7  35296  cvmliftlem10  35299  cvmliftlem11  35300  cvmliftlem13  35301  bcm1nt  35737  bcprod  35738  iprodgam  35742  faclimlem1  35743  faclimlem2  35744  faclim2  35748  nn0prpwlem  36323  nn0prpw  36324  knoppcnlem10  36503  knoppndvlem16  36528  poimirlem1  37628  poimirlem2  37629  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  nnproddivdvdsd  42001  lcmfunnnd  42013  lcmineqlem3  42032  lcmineqlem4  42033  lcmineqlem6  42035  lcmineqlem8  42037  lcmineqlem10  42039  lcmineqlem11  42040  lcmineqlem12  42041  lcmineqlem16  42045  lcmineqlem18  42047  lcmineqlem23  42052  dvrelogpow2b  42069  aks4d1p1p2  42071  aks4d1p1  42077  aks4d1p8  42088  primrootsunit1  42098  primrootscoprmpow  42100  posbezout  42101  primrootscoprbij  42103  primrootspoweq0  42107  aks6d1c1p3  42111  aks6d1c1p8  42116  aks6d1c2p2  42120  hashscontpow1  42122  2np3bcnp1  42145  2ap1caineq  42146  sticksstones10  42156  sticksstones12a  42158  sticksstones16  42163  sticksstones22  42169  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  aks6d1c7  42185  unitscyglem2  42197  unitscyglem4  42199  unitscyglem5  42200  aks5lem8  42202  metakunt8  42213  metakunt15  42220  metakunt16  42221  metakunt20  42225  metakunt28  42233  metakunt30  42235  nnadddir  42305  nnmul1com  42306  nnmulcom  42307  oddnumth  42345  nicomachus  42346  zaddcom  42482  fltabcoprmex  42649  fltaccoprm  42650  fltbccoprm  42651  fltne  42654  flt4lem3  42658  flt4lem5elem  42661  flt4lem5a  42662  flt4lem5b  42663  flt4lem5c  42664  flt4lem5d  42665  flt4lem5e  42666  flt4lem5f  42667  flt4lem6  42668  flt4lem7  42669  nna4b4nsq  42670  fltltc  42671  fltnltalem  42672  fltnlta  42673  irrapxlem4  42836  irrapxlem5  42837  pellexlem2  42841  pellexlem6  42845  pell1234qrne0  42864  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell1234qrdich  42872  pell14qrdich  42880  pell1qrge1  42881  pell1qr1  42882  pell14qrgapw  42887  rmxyneg  42932  rmxm1  42946  rmxluc  42948  rmxdbl  42951  jm2.19lem1  43001  jm2.27c  43019  relexpmulnn  43722  relexpmulg  43723  inductionexd  44168  hashnzfzclim  44341  bcccl  44358  bcc0  44359  bccp1k  44360  bccm1k  44361  binomcxplemwb  44367  fsumnncl  45587  mccllem  45612  clim1fr1  45616  sumnnodd  45645  dvsinexp  45926  dvxpaek  45955  dvnxpaek  45957  dvnprodlem2  45962  itgsinexplem1  45969  itgsinexp  45970  stoweidlem1  46016  stoweidlem11  46026  stoweidlem25  46040  stoweidlem26  46041  stoweidlem34  46049  stoweidlem37  46052  stoweidlem38  46053  stoweidlem42  46057  wallispi2lem1  46086  wallispi2  46088  stirlinglem4  46092  stirlinglem5  46093  stirlinglem10  46098  stirlinglem15  46103  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem11  46133  fourierdlem15  46137  fourierdlem79  46200  fourierdlem83  46204  sqwvfourb  46244  etransclem14  46263  etransclem15  46264  etransclem20  46269  etransclem21  46270  etransclem22  46271  etransclem23  46272  etransclem24  46273  etransclem25  46274  etransclem28  46277  etransclem31  46280  etransclem32  46281  etransclem33  46282  etransclem34  46283  etransclem35  46284  etransclem38  46287  etransclem41  46290  etransclem44  46293  etransclem45  46294  etransclem47  46296  etransclem48  46297  nnfoctbdjlem  46470  deccarry  47323  iccpartgtprec  47407  fmtnoodd  47520  fmtnorec2lem  47529  fmtnorec2  47530  fmtnodvds  47531  goldbachthlem2  47533  fmtnorec3  47535  fmtnorec4  47536  fmtnoprmfac1lem  47551  fmtnoprmfac1  47552  fmtnoprmfac2lem1  47553  fmtnoprmfac2  47554  2pwp1prm  47576  sfprmdvdsmersenne  47590  lighneallem4b  47596  lighneal  47598  proththdlem  47600  proththd  47601  oexpnegALTV  47664  perfectALTVlem1  47708  perfectALTVlem2  47709  perfectALTV  47710  nnpw2pmod  48504  nnolog2flm1  48511  blennn0em1  48512  blengt1fldiv2p1  48514  nn0sumshdiglemB  48541  amgmlemALT  49322