Theorem nncnd 11972

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℂcc 10853  ℕcn 11956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579  ax-1cn 10913  ax-addcl 10915

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-om 7701  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-nn 11957

This theorem is referenced by:  facdiv  13982  facndiv  13983  faclbnd  13985  faclbnd5  13993  faclbnd6  13994  facubnd  13995  facavg  13996  bccmpl  14004  bcn0  14005  bcn1  14008  bcm1k  14010  bcp1n  14011  bcp1nk  14012  bcval5  14013  bcpasc  14016  permnn  14021  hashf1  14152  hashfac  14153  relexpaddnn  14743  binom11  15525  binom1dif  15526  climcndslem2  15543  arisum2  15554  trireciplem  15555  trirecip  15556  geo2sum  15566  geo2lim  15568  fprodfac  15664  risefacfac  15726  fallfacfwd  15727  fallfacval4  15734  bcfallfac  15735  fallfacfac  15736  bpolycl  15743  bpolysum  15744  bpolydiflem  15745  fsumkthpow  15747  eftcl  15764  eftabs  15766  efcllem  15768  ege2le3  15780  efcj  15782  efaddlem  15783  eftlub  15799  eirrlem  15894  sqrt2irrlem  15938  oexpneg  16035  pwp1fsum  16081  bitsp1  16119  bitsfzolem  16122  bitsfzo  16123  bitsmod  16124  bitscmp  16126  bitsinv1lem  16129  bitsinv1  16130  2ebits  16135  bitsinvp1  16137  sadcaddlem  16145  sadadd3  16149  bitsres  16161  bitsuz  16162  bitsshft  16163  dvdsgcdidd  16226  mulgcd  16237  rplpwr  16248  sqgcd  16251  lcmgcdlem  16292  3lcm2e6woprm  16301  coprmprod  16347  coprmproddvdslem  16348  cncongr1  16353  cncongr2  16354  prmind2  16371  isprm5  16393  divgcdodd  16396  prmdvdsexpr  16403  qmuldeneqnum  16432  divnumden  16433  qnumgt0  16435  numdensq  16439  hashdvds  16457  phiprmpw  16458  prmdiv  16467  prmdivdiv  16469  phisum  16472  modprm0  16487  pythagtriplem4  16501  pythagtriplem6  16503  pythagtriplem7  16504  pythagtriplem14  16510  pythagtriplem15  16511  pythagtriplem19  16515  pythagtrip  16516  pcprendvds2  16523  pcpre1  16524  pcpremul  16525  pceulem  16527  pcdiv  16534  pcqmul  16535  pcelnn  16552  pcid  16555  pc2dvds  16561  dvdsprmpweqnn  16567  dvdsprmpweqle  16568  pcaddlem  16570  pcadd  16571  pcfaclem  16580  qexpz  16583  expnprm  16584  oddprmdvds  16585  prmpwdvds  16586  pockthlem  16587  pockthg  16588  infpnlem1  16592  prmreclem1  16598  prmreclem2  16599  prmreclem3  16600  prmreclem4  16601  prmreclem6  16603  4sqlem6  16625  4sqlem7  16626  4sqlem10  16629  mul4sqlem  16635  4sqlem11  16637  4sqlem12  16638  4sqlem14  16640  4sqlem17  16643  4sqlem18  16644  vdwlem1  16663  vdwlem2  16664  vdwlem3  16665  vdwlem5  16667  vdwlem6  16668  vdwlem8  16670  vdwlem9  16671  vdwlem10  16672  vdwlem12  16674  ramub1lem2  16709  ramcl  16711  prmop1  16720  prmdvdsprmo  16724  prmgaplem7  16739  prmgaplem8  16740  gsumsgrpccat  18459  gsumccatOLD  18460  mulgnndir  18713  mulgnnass  18719  psgnunilem5  19083  odf1o2  19159  pgp0  19182  sylow1lem1  19184  odcau  19190  sylow2blem3  19208  sylow3lem3  19215  sylow3lem4  19216  gexexlem  19434  ablfacrp2  19651  ablfac1lem  19652  ablfac1eu  19657  pgpfac1lem3a  19660  pgpfac1lem3  19661  fincygsubgodexd  19697  zringlpirlem3  20667  znrrg  20754  cpmadugsumlemF  22006  lebnumlem3  24107  ovollb2lem  24633  ovolunlem1a  24641  ovolunlem1  24642  uniioombllem3  24730  uniioombllem4  24731  dyaddisjlem  24740  mbfi1fseqlem3  24863  mbfi1fseqlem4  24864  itgpowd  25195  dgrcolem1  25415  vieta1lem1  25451  vieta1lem2  25452  elqaalem2  25461  elqaalem3  25462  aalioulem1  25473  aaliou3lem2  25484  aaliou3lem8  25486  aaliou3lem6  25489  aaliou3lem9  25491  taylfvallem1  25497  tayl0  25502  taylply2  25508  taylply  25509  dvtaylp  25510  taylthlem1  25513  taylthlem2  25514  pserdvlem2  25568  advlogexp  25791  cxpmul2  25825  cxpeq  25891  atantayl3  26070  leibpi  26073  log2cnv  26075  log2tlbnd  26076  birthdaylem2  26083  birthdaylem3  26084  amgmlem  26120  amgm  26121  emcllem5  26130  fsumharmonic  26142  zetacvg  26145  dmgmdivn0  26158  lgamgulmlem3  26161  lgamgulmlem4  26162  lgamgulmlem5  26163  lgamgulmlem6  26164  lgamgulm2  26166  lgamcvg2  26185  gamcvg  26186  gamcvg2lem  26189  facgam  26196  wilthlem1  26198  wilthlem2  26199  wilthlem3  26200  wilthimp  26202  basellem1  26211  basellem2  26212  basellem3  26213  basellem4  26214  basellem5  26215  basellem8  26218  vmaprm  26247  sgmval2  26273  0sgm  26274  sgmf  26275  vma1  26296  fsumdvdsdiaglem  26313  dvdsflf1o  26317  muinv  26323  dvdsmulf1o  26324  sgmppw  26326  1sgmprm  26328  1sgm2ppw  26329  sgmmul  26330  chtublem  26340  fsumvma2  26343  chpchtsum  26348  logfaclbnd  26351  logexprlim  26354  mersenne  26356  perfect1  26357  perfectlem1  26358  perfectlem2  26359  perfect  26360  dchrsum2  26397  dchrhash  26400  bcmono  26406  bcp1ctr  26408  bclbnd  26409  bposlem1  26413  bposlem2  26414  bposlem3  26415  bposlem5  26417  bposlem6  26418  lgsval2lem  26436  lgsqrlem2  26476  gausslemma2dlem6  26501  gausslemma2dlem7  26502  gausslemma2d  26503  lgseisenlem1  26504  lgseisenlem4  26507  lgsquadlem1  26509  lgsquadlem2  26510  lgsquadlem3  26511  lgsquad2  26515  m1lgs  26517  2sqlem3  26549  2sqlem4  26550  chebbnd1lem1  26598  chebbnd1  26601  rplogsumlem1  26613  rplogsumlem2  26614  rpvmasumlem  26616  dchrisumlem1  26618  dchrmusum2  26623  dchrvmasumlem1  26624  dchrvmasum2lem  26625  dchrvmasum2if  26626  dchrvmasumlem2  26627  dchrvmasumlem3  26628  dchrvmasumiflem1  26630  dchrisum0flblem1  26637  dchrisum0flblem2  26638  dchrisum0fno1  26640  rpvmasum2  26641  rplogsum  26656  mulogsumlem  26660  mulogsum  26661  mulog2sumlem2  26664  vmalogdivsum2  26667  vmalogdivsum  26668  2vmadivsumlem  26669  logsqvma  26671  selberglem2  26675  selberglem3  26676  selberg  26677  selberg2lem  26679  logdivbnd  26685  selberg3lem1  26686  selberg4lem1  26689  pntrsumo1  26694  pntrsumbnd2  26696  selberg3r  26698  selberg4r  26699  selberg34r  26700  pntsval2  26705  pntrlog2bndlem2  26707  pntrlog2bndlem4  26709  pntrlog2bndlem6  26712  pntpbnd1  26715  pntpbnd2  26716  pntlemg  26727  pntlemn  26729  pntlemf  26734  pnt  26743  padicabvf  26760  ostth2lem2  26763  ostth3  26767  fusgrhashclwwlkn  28422  eucrct2eupth  28588  numdenneg  31110  ltesubnnd  31115  1smat1  31733  madjusmdetlem2  31757  madjusmdetlem4  31759  qqhnm  31919  oddpwdc  32300  eulerpartlemsv2  32304  eulerpartlems  32306  eulerpartlemsv3  32307  eulerpartlemgc  32308  eulerpartlemv  32310  eulerpartlemgs2  32326  fibp1  32347  ballotlemfc0  32438  ballotlemfcc  32439  signsvtn0  32528  reprpmtf1o  32585  vtscl  32597  hgt750lemb  32615  tgoldbachgt  32622  subfacp1lem1  33120  subfacp1lem5  33125  subfacval2  33128  subfaclim  33129  cvmliftlem2  33227  cvmliftlem7  33232  cvmliftlem10  33235  cvmliftlem11  33236  cvmliftlem13  33237  bcm1nt  33682  bcprod  33683  iprodgam  33687  faclimlem1  33688  faclimlem2  33689  faclim2  33693  nn0prpwlem  34490  nn0prpw  34491  knoppndvlem16  34686  poimirlem1  35757  poimirlem2  35758  poimirlem6  35762  poimirlem7  35763  poimirlem8  35764  poimirlem9  35765  poimirlem10  35766  poimirlem11  35767  poimirlem12  35768  poimirlem13  35769  poimirlem15  35771  poimirlem16  35772  poimirlem17  35773  poimirlem18  35774  poimirlem19  35775  poimirlem20  35776  poimirlem21  35777  poimirlem22  35778  poimirlem23  35779  poimirlem24  35780  poimirlem25  35781  poimirlem26  35782  poimirlem27  35783  poimirlem31  35787  nnproddivdvdsd  39989  lcmfunnnd  40000  lcmineqlem3  40019  lcmineqlem4  40020  lcmineqlem6  40022  lcmineqlem8  40024  lcmineqlem10  40026  lcmineqlem11  40027  lcmineqlem12  40028  lcmineqlem16  40032  lcmineqlem18  40034  lcmineqlem23  40039  dvrelogpow2b  40056  aks4d1p1p2  40058  aks4d1p1  40064  aks4d1p8  40075  2np3bcnp1  40080  2ap1caineq  40081  sticksstones10  40091  sticksstones12a  40093  sticksstones16  40098  sticksstones22  40104  metakunt8  40112  metakunt15  40119  metakunt16  40120  metakunt20  40124  metakunt28  40132  metakunt30  40134  nnadddir  40280  nnmul1com  40281  nnmulcom  40282  expgcd  40314  nn0expgcd  40315  numdenexp  40317  fltabcoprmex  40456  fltaccoprm  40457  fltbccoprm  40458  fltne  40461  flt4lem3  40465  flt4lem5elem  40468  flt4lem5a  40469  flt4lem5b  40470  flt4lem5c  40471  flt4lem5d  40472  flt4lem5e  40473  flt4lem5f  40474  flt4lem6  40475  flt4lem7  40476  nna4b4nsq  40477  fltltc  40478  fltnltalem  40479  fltnlta  40480  irrapxlem4  40627  irrapxlem5  40628  pellexlem2  40632  pellexlem6  40636  pell1234qrne0  40655  pell1234qrreccl  40656  pell1234qrmulcl  40657  pell1234qrdich  40663  pell14qrdich  40671  pell1qrge1  40672  pell1qr1  40673  pell14qrgapw  40678  rmxyneg  40722  rmxm1  40736  rmxluc  40738  rmxdbl  40741  jm2.19lem1  40791  jm2.27c  40809  relexpmulnn  41270  relexpmulg  41271  inductionexd  41718  hashnzfzclim  41893  bcccl  41910  bcc0  41911  bccp1k  41912  bccm1k  41913  binomcxplemwb  41919  fsumnncl  43067  mccllem  43092  clim1fr1  43096  sumnnodd  43125  dvsinexp  43406  dvxpaek  43435  dvnxpaek  43437  dvnprodlem2  43442  itgsinexplem1  43449  itgsinexp  43450  stoweidlem1  43496  stoweidlem11  43506  stoweidlem25  43520  stoweidlem26  43521  stoweidlem34  43529  stoweidlem37  43532  stoweidlem38  43533  stoweidlem42  43537  wallispi2lem1  43566  wallispi2  43568  stirlinglem4  43572  stirlinglem5  43573  stirlinglem10  43578  stirlinglem15  43583  dirkertrigeqlem3  43595  dirkertrigeq  43596  dirkercncflem2  43599  dirkercncflem4  43601  fourierdlem11  43613  fourierdlem15  43617  fourierdlem79  43680  fourierdlem83  43684  sqwvfourb  43724  etransclem14  43743  etransclem15  43744  etransclem20  43749  etransclem21  43750  etransclem22  43751  etransclem23  43752  etransclem24  43753  etransclem25  43754  etransclem28  43757  etransclem31  43760  etransclem32  43761  etransclem33  43762  etransclem34  43763  etransclem35  43764  etransclem38  43767  etransclem41  43770  etransclem44  43773  etransclem45  43774  etransclem47  43776  etransclem48  43777  nnfoctbdjlem  43947  deccarry  44755  iccpartgtprec  44824  fmtnoodd  44937  fmtnorec2lem  44946  fmtnorec2  44947  fmtnodvds  44948  goldbachthlem2  44950  fmtnorec3  44952  fmtnorec4  44953  fmtnoprmfac1lem  44968  fmtnoprmfac1  44969  fmtnoprmfac2lem1  44970  fmtnoprmfac2  44971  2pwp1prm  44993  sfprmdvdsmersenne  45007  lighneallem4b  45013  lighneal  45015  proththdlem  45017  proththd  45018  oexpnegALTV  45081  perfectALTVlem1  45125  perfectALTVlem2  45126  perfectALTV  45127  nnpw2pmod  45881  nnolog2flm1  45888  blennn0em1  45889  blengt1fldiv2p1  45891  nn0sumshdiglemB  45918  amgmlemALT  46459