Theorem nncnd 12133

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℂcc 10996  ℕcn 12117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663  ax-1cn 11056  ax-addcl 11058

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-pss 3920  df-nul 4282  df-if 4474  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6244  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6433  df-fun 6479  df-fn 6480  df-f 6481  df-f1 6482  df-fo 6483  df-f1o 6484  df-fv 6485  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-nn 12118

This theorem is referenced by:  nneo  12549  facdiv  14186  facndiv  14187  faclbnd  14189  faclbnd5  14197  faclbnd6  14198  facubnd  14199  facavg  14200  bccmpl  14208  bcn0  14209  bcn1  14212  bcm1k  14214  bcp1n  14215  bcp1nk  14216  bcval5  14217  bcpasc  14220  permnn  14225  hashf1  14356  hashfac  14357  relexpaddnn  14950  binom11  15731  binom1dif  15732  climcndslem2  15749  arisum2  15760  trireciplem  15761  trirecip  15762  geo2sum  15772  geo2lim  15774  fprodfac  15872  risefacfac  15934  fallfacfwd  15935  fallfacval4  15942  bcfallfac  15943  fallfacfac  15944  bpolycl  15951  bpolysum  15952  bpolydiflem  15953  fsumkthpow  15955  eftcl  15972  eftabs  15974  efcllem  15976  ege2le3  15989  efcj  15991  efaddlem  15992  eftlub  16010  eirrlem  16105  sqrt2irrlem  16149  oexpneg  16248  pwp1fsum  16294  bitsp1  16334  bitsfzolem  16337  bitsfzo  16338  bitsmod  16339  bitscmp  16341  bitsinv1lem  16344  bitsinv1  16345  2ebits  16350  bitsinvp1  16352  sadcaddlem  16360  sadadd3  16364  bitsres  16376  bitsuz  16377  bitsshft  16378  dvdsgcdidd  16440  mulgcd  16451  rplpwr  16461  sqgcd  16465  expgcd  16466  nn0expgcd  16467  lcmgcdlem  16509  3lcm2e6woprm  16518  coprmprod  16564  coprmproddvdslem  16565  cncongr1  16570  cncongr2  16571  prmind2  16588  isprm5  16610  divgcdodd  16613  prmdvdsexpr  16620  qmuldeneqnum  16650  divnumden  16651  qnumgt0  16653  numdensq  16657  numdenexp  16663  hashdvds  16678  phiprmpw  16679  prmdiv  16688  prmdivdiv  16690  phisum  16694  modprm0  16709  pythagtriplem4  16723  pythagtriplem6  16725  pythagtriplem7  16726  pythagtriplem14  16732  pythagtriplem15  16733  pythagtriplem19  16737  pythagtrip  16738  pcprendvds2  16745  pcpre1  16746  pcpremul  16747  pceulem  16749  pcdiv  16756  pcqmul  16757  pcelnn  16774  pcid  16777  pc2dvds  16783  dvdsprmpweqnn  16789  dvdsprmpweqle  16790  pcaddlem  16792  pcadd  16793  pcfaclem  16802  qexpz  16805  expnprm  16806  oddprmdvds  16807  prmpwdvds  16808  pockthlem  16809  pockthg  16810  infpnlem1  16814  prmreclem1  16820  prmreclem2  16821  prmreclem3  16822  prmreclem4  16823  prmreclem6  16825  4sqlem6  16847  4sqlem7  16848  4sqlem10  16851  mul4sqlem  16857  4sqlem11  16859  4sqlem12  16860  4sqlem14  16862  4sqlem17  16865  4sqlem18  16866  vdwlem1  16885  vdwlem2  16886  vdwlem3  16887  vdwlem5  16889  vdwlem6  16890  vdwlem8  16892  vdwlem9  16893  vdwlem10  16894  vdwlem12  16896  ramub1lem2  16931  ramcl  16933  prmop1  16942  prmdvdsprmo  16946  prmgaplem7  16961  prmgaplem8  16962  chnub  18520  gsumsgrpccat  18740  mulgnndir  19008  mulgnnass  19014  psgnunilem5  19399  odf1o2  19478  pgp0  19501  sylow1lem1  19503  odcau  19509  sylow2blem3  19527  sylow3lem3  19534  sylow3lem4  19535  gexexlem  19757  ablfacrp2  19974  ablfac1lem  19975  ablfac1eu  19980  pgpfac1lem3a  19983  pgpfac1lem3  19984  fincygsubgodexd  20020  zringlpirlem3  21394  znrrg  21495  psdpw  22078  cpmadugsumlemF  22784  lebnumlem3  24882  ovollb2lem  25409  ovolunlem1a  25417  ovolunlem1  25418  uniioombllem3  25506  uniioombllem4  25507  dyaddisjlem  25516  mbfi1fseqlem3  25638  mbfi1fseqlem4  25639  itgpowd  25977  dgrcolem1  26199  vieta1lem1  26238  vieta1lem2  26239  elqaalem2  26248  elqaalem3  26249  aalioulem1  26260  aaliou3lem2  26271  aaliou3lem8  26273  aaliou3lem6  26276  aaliou3lem9  26278  taylfvallem1  26284  tayl0  26289  taylply2  26295  taylply2OLD  26296  taylply  26297  dvtaylp  26298  taylthlem1  26301  taylthlem2  26302  taylthlem2OLD  26303  pserdvlem2  26358  advlogexp  26584  cxpmul2  26618  cxpeq  26687  rtprmirr  26690  atantayl3  26869  leibpi  26872  log2cnv  26874  log2tlbnd  26875  birthdaylem2  26882  birthdaylem3  26883  amgmlem  26920  amgm  26921  emcllem5  26930  fsumharmonic  26942  zetacvg  26945  dmgmdivn0  26958  lgamgulmlem3  26961  lgamgulmlem4  26962  lgamgulmlem5  26963  lgamgulmlem6  26964  lgamgulm2  26966  lgamcvg2  26985  gamcvg  26986  gamcvg2lem  26989  facgam  26996  wilthlem1  26998  wilthlem2  26999  wilthlem3  27000  wilthimp  27002  basellem1  27011  basellem2  27012  basellem3  27013  basellem4  27014  basellem5  27015  basellem8  27018  vmaprm  27047  sgmval2  27073  0sgm  27074  sgmf  27075  vma1  27096  fsumdvdsdiaglem  27113  dvdsflf1o  27117  muinv  27123  mpodvdsmulf1o  27124  dvdsmulf1o  27126  sgmppw  27128  1sgmprm  27130  1sgm2ppw  27131  sgmmul  27132  chtublem  27142  fsumvma2  27145  chpchtsum  27150  logfaclbnd  27153  logexprlim  27156  mersenne  27158  perfect1  27159  perfectlem1  27160  perfectlem2  27161  perfect  27162  dchrsum2  27199  dchrhash  27202  bcmono  27208  bcp1ctr  27210  bclbnd  27211  bposlem1  27215  bposlem2  27216  bposlem3  27217  bposlem5  27219  bposlem6  27220  lgsval2lem  27238  lgsqrlem2  27278  gausslemma2dlem6  27303  gausslemma2dlem7  27304  gausslemma2d  27305  lgseisenlem1  27306  lgseisenlem4  27309  lgsquadlem1  27311  lgsquadlem2  27312  lgsquadlem3  27313  lgsquad2  27317  m1lgs  27319  2sqlem3  27351  2sqlem4  27352  chebbnd1lem1  27400  chebbnd1  27403  rplogsumlem1  27415  rplogsumlem2  27416  rpvmasumlem  27418  dchrisumlem1  27420  dchrmusum2  27425  dchrvmasumlem1  27426  dchrvmasum2lem  27427  dchrvmasum2if  27428  dchrvmasumlem2  27429  dchrvmasumlem3  27430  dchrvmasumiflem1  27432  dchrisum0flblem1  27439  dchrisum0flblem2  27440  dchrisum0fno1  27442  rpvmasum2  27443  rplogsum  27458  mulogsumlem  27462  mulogsum  27463  mulog2sumlem2  27466  vmalogdivsum2  27469  vmalogdivsum  27470  2vmadivsumlem  27471  logsqvma  27473  selberglem2  27477  selberglem3  27478  selberg  27479  selberg2lem  27481  logdivbnd  27487  selberg3lem1  27488  selberg4lem1  27491  pntrsumo1  27496  pntrsumbnd2  27498  selberg3r  27500  selberg4r  27501  selberg34r  27502  pntsval2  27507  pntrlog2bndlem2  27509  pntrlog2bndlem4  27511  pntrlog2bndlem6  27514  pntpbnd1  27517  pntpbnd2  27518  pntlemg  27529  pntlemn  27531  pntlemf  27536  pnt  27545  padicabvf  27562  ostth2lem2  27565  ostth3  27569  fusgrhashclwwlkn  30049  eucrct2eupth  30215  nrt2irr  30443  elq2  32784  numdenneg  32787  ltesubnnd  32795  2exple2exp  32818  oexpled  32820  1arithidomlem2  33491  1arithidom  33492  zringfrac  33509  cos9thpiminplylem1  33785  cos9thpiminplylem2  33786  1smat1  33807  madjusmdetlem2  33831  madjusmdetlem4  33833  qqhnm  33993  oddpwdc  34357  eulerpartlemsv2  34361  eulerpartlems  34363  eulerpartlemsv3  34364  eulerpartlemgc  34365  eulerpartlemv  34367  eulerpartlemgs2  34383  fibp1  34404  ballotlemfc0  34496  ballotlemfcc  34497  signsvtn0  34573  reprpmtf1o  34629  vtscl  34641  hgt750lemb  34659  tgoldbachgt  34666  subfacp1lem1  35191  subfacp1lem5  35196  subfacval2  35199  subfaclim  35200  cvmliftlem2  35298  cvmliftlem7  35303  cvmliftlem10  35306  cvmliftlem11  35307  cvmliftlem13  35308  bcm1nt  35749  bcprod  35750  iprodgam  35754  faclimlem1  35755  faclimlem2  35756  faclim2  35760  nn0prpwlem  36335  nn0prpw  36336  knoppcnlem10  36515  knoppndvlem16  36540  poimirlem1  37640  poimirlem2  37641  poimirlem6  37645  poimirlem7  37646  poimirlem8  37647  poimirlem9  37648  poimirlem10  37649  poimirlem11  37650  poimirlem12  37651  poimirlem13  37652  poimirlem15  37654  poimirlem16  37655  poimirlem17  37656  poimirlem18  37657  poimirlem19  37658  poimirlem20  37659  poimirlem21  37660  poimirlem22  37661  poimirlem23  37662  poimirlem24  37663  poimirlem25  37664  poimirlem26  37665  poimirlem27  37666  poimirlem31  37670  nnproddivdvdsd  42012  lcmfunnnd  42024  lcmineqlem3  42043  lcmineqlem4  42044  lcmineqlem6  42046  lcmineqlem8  42048  lcmineqlem10  42050  lcmineqlem11  42051  lcmineqlem12  42052  lcmineqlem16  42056  lcmineqlem18  42058  lcmineqlem23  42063  dvrelogpow2b  42080  aks4d1p1p2  42082  aks4d1p1  42088  aks4d1p8  42099  primrootsunit1  42109  primrootscoprmpow  42111  posbezout  42112  primrootscoprbij  42114  primrootspoweq0  42118  aks6d1c1p3  42122  aks6d1c1p8  42127  aks6d1c2p2  42131  hashscontpow1  42133  2np3bcnp1  42156  2ap1caineq  42157  sticksstones10  42167  sticksstones12a  42169  sticksstones16  42174  sticksstones22  42180  bcled  42190  bcle2d  42191  aks6d1c7lem1  42192  aks6d1c7  42196  unitscyglem2  42208  unitscyglem4  42210  unitscyglem5  42211  aks5lem8  42213  nnadddir  42282  nnmul1com  42283  nnmulcom  42284  oddnumth  42323  nicomachus  42324  zaddcom  42476  fltabcoprmex  42651  fltaccoprm  42652  fltbccoprm  42653  fltne  42656  flt4lem3  42660  flt4lem5elem  42663  flt4lem5a  42664  flt4lem5b  42665  flt4lem5c  42666  flt4lem5d  42667  flt4lem5e  42668  flt4lem5f  42669  flt4lem6  42670  flt4lem7  42671  nna4b4nsq  42672  fltltc  42673  fltnltalem  42674  fltnlta  42675  irrapxlem4  42837  irrapxlem5  42838  pellexlem2  42842  pellexlem6  42846  pell1234qrne0  42865  pell1234qrreccl  42866  pell1234qrmulcl  42867  pell1234qrdich  42873  pell14qrdich  42881  pell1qrge1  42882  pell1qr1  42883  pell14qrgapw  42888  rmxyneg  42932  rmxm1  42946  rmxluc  42948  rmxdbl  42951  jm2.19lem1  43001  jm2.27c  43019  relexpmulnn  43721  relexpmulg  43722  inductionexd  44167  hashnzfzclim  44334  bcccl  44351  bcc0  44352  bccp1k  44353  bccm1k  44354  binomcxplemwb  44360  fsumnncl  45591  mccllem  45616  clim1fr1  45620  sumnnodd  45649  dvsinexp  45928  dvxpaek  45957  dvnxpaek  45959  dvnprodlem2  45964  itgsinexplem1  45971  itgsinexp  45972  stoweidlem1  46018  stoweidlem11  46028  stoweidlem25  46042  stoweidlem26  46043  stoweidlem34  46051  stoweidlem37  46054  stoweidlem38  46055  stoweidlem42  46059  wallispi2lem1  46088  wallispi2  46090  stirlinglem4  46094  stirlinglem5  46095  stirlinglem10  46100  stirlinglem15  46105  dirkertrigeqlem3  46117  dirkertrigeq  46118  dirkercncflem2  46121  dirkercncflem4  46123  fourierdlem11  46135  fourierdlem15  46139  fourierdlem79  46202  fourierdlem83  46206  sqwvfourb  46246  etransclem14  46265  etransclem15  46266  etransclem20  46271  etransclem21  46272  etransclem22  46273  etransclem23  46274  etransclem24  46275  etransclem25  46276  etransclem28  46279  etransclem31  46282  etransclem32  46283  etransclem33  46284  etransclem34  46285  etransclem35  46286  etransclem38  46289  etransclem41  46292  etransclem44  46295  etransclem45  46296  etransclem47  46298  etransclem48  46299  nnfoctbdjlem  46472  deccarry  47321  iccpartgtprec  47430  fmtnoodd  47543  fmtnorec2lem  47552  fmtnorec2  47553  fmtnodvds  47554  goldbachthlem2  47556  fmtnorec3  47558  fmtnorec4  47559  fmtnoprmfac1lem  47574  fmtnoprmfac1  47575  fmtnoprmfac2lem1  47576  fmtnoprmfac2  47577  2pwp1prm  47599  sfprmdvdsmersenne  47613  lighneallem4b  47619  lighneal  47621  proththdlem  47623  proththd  47624  oexpnegALTV  47687  perfectALTVlem1  47731  perfectALTVlem2  47732  perfectALTV  47733  nnpw2pmod  48594  nnolog2flm1  48601  blennn0em1  48602  blengt1fldiv2p1  48604  nn0sumshdiglemB  48631  amgmlemALT  49814