Theorem nncnd 10913

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

Syntax hints:   → wi 4   ∈ wcel 1977  ℂcc 9813  ℕcn 10897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-nn 10898

This theorem is referenced by:  facdiv  12936  facndiv  12937  faclbnd  12939  faclbnd5  12947  faclbnd6  12948  facubnd  12949  facavg  12950  bccmpl  12958  bcn0  12959  bcn1  12962  bcm1k  12964  bcp1n  12965  bcp1nk  12966  bcval5  12967  bcpasc  12970  permnn  12975  hashf1  13098  hashfac  13099  relexpaddnn  13639  binom11  14403  binom1dif  14404  climcndslem2  14421  arisum2  14432  trireciplem  14433  trirecip  14434  geo2sum  14443  geo2lim  14445  fprodfac  14542  risefacfac  14605  fallfacfwd  14606  fallfacval4  14613  bcfallfac  14614  fallfacfac  14615  bpolycl  14622  bpolysum  14623  bpolydiflem  14624  fsumkthpow  14626  eftcl  14643  eftabs  14645  efcllem  14647  ege2le3  14659  efcj  14661  efaddlem  14662  eftlub  14678  eirrlem  14771  sqr2irrlem  14816  oexpneg  14907  pwp1fsum  14952  bitsp1  14991  bitsfzolem  14994  bitsfzo  14995  bitsmod  14996  bitscmp  14998  bitsinv1lem  15001  bitsinv1  15002  2ebits  15007  bitsinvp1  15009  sadcaddlem  15017  sadadd3  15021  bitsres  15033  bitsuz  15034  bitsshft  15035  mulgcd  15103  rplpwr  15114  sqgcd  15116  lcmgcdlem  15157  3lcm2e6woprm  15166  coprmprod  15213  coprmproddvdslem  15214  cncongr1  15219  cncongr2  15220  prmind2  15236  isprm5  15257  divgcdodd  15260  prmdvdsexpr  15267  qmuldeneqnum  15293  divnumden  15294  qnumgt0  15296  numdensq  15300  hashdvds  15318  phiprmpw  15319  prmdiv  15328  prmdivdiv  15330  phisum  15333  modprm0  15348  pythagtriplem4  15362  pythagtriplem6  15364  pythagtriplem7  15365  pythagtriplem14  15371  pythagtriplem15  15372  pythagtriplem19  15376  pythagtrip  15377  pcprendvds2  15384  pcpre1  15385  pcpremul  15386  pceulem  15388  pcdiv  15395  pcqmul  15396  pcelnn  15412  pcid  15415  pc2dvds  15421  dvdsprmpweqnn  15427  dvdsprmpweqle  15428  pcaddlem  15430  pcadd  15431  pcfaclem  15440  qexpz  15443  expnprm  15444  oddprmdvds  15445  prmpwdvds  15446  pockthlem  15447  pockthg  15448  infpnlem1  15452  prmreclem1  15458  prmreclem2  15459  prmreclem3  15460  prmreclem4  15461  prmreclem6  15463  4sqlem6  15485  4sqlem7  15486  4sqlem10  15489  mul4sqlem  15495  4sqlem11  15497  4sqlem12  15498  4sqlem14  15500  4sqlem17  15503  4sqlem18  15504  vdwlem1  15523  vdwlem2  15524  vdwlem3  15525  vdwlem5  15527  vdwlem6  15528  vdwlem8  15530  vdwlem9  15531  vdwlem10  15532  vdwlem12  15534  ramub1lem2  15569  ramcl  15571  prmop1  15580  prmdvdsprmo  15584  prmgaplem7  15599  prmgaplem8  15600  gsumccat  17201  mulgnndir  17392  mulgnndirOLD  17393  mulgnnass  17399  mulgnnassOLD  17400  psgnunilem5  17737  odf1o2  17811  pgp0  17834  sylow1lem1  17836  odcau  17842  sylow2blem3  17860  sylow3lem3  17867  sylow3lem4  17868  gexexlem  18078  ablfacrp2  18289  ablfac1lem  18290  ablfac1eu  18295  pgpfac1lem3a  18298  pgpfac1lem3  18299  zringlpirlem3  19653  znrrg  19733  cpmadugsumlemF  20500  lebnumlem3  22570  ovollb2lem  23063  ovolunlem1a  23071  ovolunlem1  23072  uniioombllem3  23159  uniioombllem4  23160  dyaddisjlem  23169  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  dgrcolem1  23833  vieta1lem1  23869  vieta1lem2  23870  elqaalem2  23879  elqaalem3  23880  aalioulem1  23891  aaliou3lem2  23902  aaliou3lem8  23904  aaliou3lem6  23907  aaliou3lem9  23909  taylfvallem1  23915  tayl0  23920  taylply2  23926  taylply  23927  dvtaylp  23928  taylthlem1  23931  taylthlem2  23932  pserdvlem2  23986  advlogexp  24201  cxpmul2  24235  cxpeq  24298  atantayl3  24466  leibpi  24469  log2cnv  24471  log2tlbnd  24472  birthdaylem2  24479  birthdaylem3  24480  amgmlem  24516  amgm  24517  emcllem5  24526  fsumharmonic  24538  zetacvg  24541  dmgmdivn0  24554  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamgulm2  24562  lgamcvg2  24581  gamcvg  24582  gamcvg2lem  24585  facgam  24592  wilthlem1  24594  wilthlem2  24595  wilthlem3  24596  wilthimp  24598  basellem1  24607  basellem2  24608  basellem3  24609  basellem4  24610  basellem5  24611  basellem8  24614  vmaprm  24643  sgmval2  24669  0sgm  24670  sgmf  24671  vma1  24692  fsumdvdsdiaglem  24709  dvdsflf1o  24713  muinv  24719  dvdsmulf1o  24720  sgmppw  24722  1sgmprm  24724  1sgm2ppw  24725  sgmmul  24726  chtublem  24736  fsumvma2  24739  chpchtsum  24744  logfaclbnd  24747  logexprlim  24750  mersenne  24752  perfect1  24753  perfectlem1  24754  perfectlem2  24755  perfect  24756  dchrsum2  24793  dchrhash  24796  bcmono  24802  bcp1ctr  24804  bclbnd  24805  bposlem1  24809  bposlem2  24810  bposlem3  24811  bposlem5  24813  bposlem6  24814  lgsval2lem  24832  lgsqrlem2  24872  gausslemma2dlem6  24897  gausslemma2dlem7  24898  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem4  24903  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2  24911  m1lgs  24913  2sqlem3  24945  2sqlem4  24946  chebbnd1lem1  24958  chebbnd1  24961  rplogsumlem1  24973  rplogsumlem2  24974  rpvmasumlem  24976  dchrisumlem1  24978  dchrmusum2  24983  dchrvmasumlem1  24984  dchrvmasum2lem  24985  dchrvmasum2if  24986  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0fno1  25000  rpvmasum2  25001  rplogsum  25016  mulogsumlem  25020  mulogsum  25021  mulog2sumlem2  25024  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  logsqvma  25031  selberglem2  25035  selberglem3  25036  selberg  25037  selberg2lem  25039  logdivbnd  25045  selberg3lem1  25046  selberg4lem1  25049  pntrsumo1  25054  pntrsumbnd2  25056  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntsval2  25065  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  pntrlog2bndlem6  25072  pntpbnd1  25075  pntpbnd2  25076  pntlemg  25087  pntlemn  25089  pntlemf  25094  pnt  25103  padicabvf  25120  ostth2lem2  25123  ostth3  25127  hashclwwlkn  26363  eupares  26502  numdenneg  28950  ltesubnnd  28955  1smat1  29198  madjusmdetlem2  29222  madjusmdetlem4  29224  qqhnm  29362  oddpwdc  29743  eulerpartlemsv2  29747  eulerpartlems  29749  eulerpartlemsv3  29750  eulerpartlemgc  29751  eulerpartlemv  29753  eulerpartlemgs2  29769  fibp1  29790  ballotlemfc0  29881  ballotlemfcc  29882  signsvtn0  29973  subfacp1lem1  30415  subfacp1lem5  30420  subfacval2  30423  subfaclim  30424  cvmliftlem2  30522  cvmliftlem7  30527  cvmliftlem10  30530  cvmliftlem11  30531  cvmliftlem13  30532  bcm1nt  30876  bcprod  30877  iprodgam  30881  faclimlem1  30882  faclimlem2  30883  faclim2  30887  nn0prpwlem  31487  nn0prpw  31488  knoppndvlem16  31688  poimirlem1  32580  poimirlem2  32581  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem31  32610  irrapxlem4  36407  irrapxlem5  36408  pellexlem2  36412  pellexlem6  36416  pell1234qrne0  36435  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell1234qrdich  36443  pell14qrdich  36451  pell1qrge1  36452  pell1qr1  36453  pell14qrgapw  36458  rmxyneg  36503  rmxm1  36517  rmxluc  36519  rmxdbl  36522  jm2.19lem1  36574  jm2.27c  36592  itgpowd  36819  relexpmulnn  37020  relexpmulg  37021  inductionexd  37473  hashnzfzclim  37543  bcccl  37560  bcc0  37561  bccp1k  37562  bccm1k  37563  binomcxplemwb  37569  fsumnncl  38638  mccllem  38664  clim1fr1  38668  sumnnodd  38697  dvsinexp  38798  dvxpaek  38830  dvnxpaek  38832  dvnprodlem2  38837  itgsinexplem1  38845  itgsinexp  38846  stoweidlem1  38894  stoweidlem11  38904  stoweidlem25  38918  stoweidlem26  38919  stoweidlem34  38927  stoweidlem37  38930  stoweidlem38  38931  stoweidlem42  38935  wallispi2lem1  38964  wallispi2  38966  stirlinglem4  38970  stirlinglem5  38971  stirlinglem10  38976  stirlinglem15  38981  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem11  39011  fourierdlem15  39015  fourierdlem79  39078  fourierdlem83  39082  sqwvfourb  39122  etransclem14  39141  etransclem15  39142  etransclem20  39147  etransclem21  39148  etransclem22  39149  etransclem23  39150  etransclem24  39151  etransclem25  39152  etransclem28  39155  etransclem31  39158  etransclem32  39159  etransclem33  39160  etransclem34  39161  etransclem35  39162  etransclem38  39165  etransclem41  39168  etransclem44  39171  etransclem45  39172  etransclem47  39174  etransclem48  39175  nnfoctbdjlem  39348  deccarry  39941  iccpartgtprec  39958  fmtnoodd  39983  fmtnorec2lem  39992  fmtnorec2  39993  fmtnodvds  39994  goldbachthlem2  39996  fmtnorec3  39998  fmtnorec4  39999  fmtnoprmfac1lem  40014  fmtnoprmfac1  40015  fmtnoprmfac2lem1  40016  fmtnoprmfac2  40017  2pwp1prm  40041  sfprmdvdsmersenne  40058  lighneallem4b  40064  lighneal  40066  proththdlem  40068  proththd  40069  oexpnegALTV  40126  perfectALTVlem1  40164  perfectALTVlem2  40165  perfectALTV  40166  fusgrhashclwwlkn  41263  eucrct2eupth  41413  nnpw2pmod  42175  nnolog2flm1  42182  blennn0em1  42183  blengt1fldiv2p1  42185  nn0sumshdiglemB  42212  amgmlemALT  42358