Theorem nncnd 11846

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

Syntax hints:   → wi 4   ∈ wcel 2110  ℂcc 10727  ℕcn 11830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523  ax-1cn 10787  ax-addcl 10789

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-ov 7216  df-om 7645  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-nn 11831

This theorem is referenced by:  facdiv  13853  facndiv  13854  faclbnd  13856  faclbnd5  13864  faclbnd6  13865  facubnd  13866  facavg  13867  bccmpl  13875  bcn0  13876  bcn1  13879  bcm1k  13881  bcp1n  13882  bcp1nk  13883  bcval5  13884  bcpasc  13887  permnn  13892  hashf1  14023  hashfac  14024  relexpaddnn  14614  binom11  15396  binom1dif  15397  climcndslem2  15414  arisum2  15425  trireciplem  15426  trirecip  15427  geo2sum  15437  geo2lim  15439  fprodfac  15535  risefacfac  15597  fallfacfwd  15598  fallfacval4  15605  bcfallfac  15606  fallfacfac  15607  bpolycl  15614  bpolysum  15615  bpolydiflem  15616  fsumkthpow  15618  eftcl  15635  eftabs  15637  efcllem  15639  ege2le3  15651  efcj  15653  efaddlem  15654  eftlub  15670  eirrlem  15765  sqrt2irrlem  15809  oexpneg  15906  pwp1fsum  15952  bitsp1  15990  bitsfzolem  15993  bitsfzo  15994  bitsmod  15995  bitscmp  15997  bitsinv1lem  16000  bitsinv1  16001  2ebits  16006  bitsinvp1  16008  sadcaddlem  16016  sadadd3  16020  bitsres  16032  bitsuz  16033  bitsshft  16034  dvdsgcdidd  16097  mulgcd  16108  rplpwr  16119  sqgcd  16122  lcmgcdlem  16163  3lcm2e6woprm  16172  coprmprod  16218  coprmproddvdslem  16219  cncongr1  16224  cncongr2  16225  prmind2  16242  isprm5  16264  divgcdodd  16267  prmdvdsexpr  16274  qmuldeneqnum  16303  divnumden  16304  qnumgt0  16306  numdensq  16310  hashdvds  16328  phiprmpw  16329  prmdiv  16338  prmdivdiv  16340  phisum  16343  modprm0  16358  pythagtriplem4  16372  pythagtriplem6  16374  pythagtriplem7  16375  pythagtriplem14  16381  pythagtriplem15  16382  pythagtriplem19  16386  pythagtrip  16387  pcprendvds2  16394  pcpre1  16395  pcpremul  16396  pceulem  16398  pcdiv  16405  pcqmul  16406  pcelnn  16423  pcid  16426  pc2dvds  16432  dvdsprmpweqnn  16438  dvdsprmpweqle  16439  pcaddlem  16441  pcadd  16442  pcfaclem  16451  qexpz  16454  expnprm  16455  oddprmdvds  16456  prmpwdvds  16457  pockthlem  16458  pockthg  16459  infpnlem1  16463  prmreclem1  16469  prmreclem2  16470  prmreclem3  16471  prmreclem4  16472  prmreclem6  16474  4sqlem6  16496  4sqlem7  16497  4sqlem10  16500  mul4sqlem  16506  4sqlem11  16508  4sqlem12  16509  4sqlem14  16511  4sqlem17  16514  4sqlem18  16515  vdwlem1  16534  vdwlem2  16535  vdwlem3  16536  vdwlem5  16538  vdwlem6  16539  vdwlem8  16541  vdwlem9  16542  vdwlem10  16543  vdwlem12  16545  ramub1lem2  16580  ramcl  16582  prmop1  16591  prmdvdsprmo  16595  prmgaplem7  16610  prmgaplem8  16611  gsumsgrpccat  18266  gsumccatOLD  18267  mulgnndir  18520  mulgnnass  18526  psgnunilem5  18886  odf1o2  18962  pgp0  18985  sylow1lem1  18987  odcau  18993  sylow2blem3  19011  sylow3lem3  19018  sylow3lem4  19019  gexexlem  19237  ablfacrp2  19454  ablfac1lem  19455  ablfac1eu  19460  pgpfac1lem3a  19463  pgpfac1lem3  19464  fincygsubgodexd  19500  zringlpirlem3  20451  znrrg  20530  cpmadugsumlemF  21773  lebnumlem3  23860  ovollb2lem  24385  ovolunlem1a  24393  ovolunlem1  24394  uniioombllem3  24482  uniioombllem4  24483  dyaddisjlem  24492  mbfi1fseqlem3  24615  mbfi1fseqlem4  24616  itgpowd  24947  dgrcolem1  25167  vieta1lem1  25203  vieta1lem2  25204  elqaalem2  25213  elqaalem3  25214  aalioulem1  25225  aaliou3lem2  25236  aaliou3lem8  25238  aaliou3lem6  25241  aaliou3lem9  25243  taylfvallem1  25249  tayl0  25254  taylply2  25260  taylply  25261  dvtaylp  25262  taylthlem1  25265  taylthlem2  25266  pserdvlem2  25320  advlogexp  25543  cxpmul2  25577  cxpeq  25643  atantayl3  25822  leibpi  25825  log2cnv  25827  log2tlbnd  25828  birthdaylem2  25835  birthdaylem3  25836  amgmlem  25872  amgm  25873  emcllem5  25882  fsumharmonic  25894  zetacvg  25897  dmgmdivn0  25910  lgamgulmlem3  25913  lgamgulmlem4  25914  lgamgulmlem5  25915  lgamgulmlem6  25916  lgamgulm2  25918  lgamcvg2  25937  gamcvg  25938  gamcvg2lem  25941  facgam  25948  wilthlem1  25950  wilthlem2  25951  wilthlem3  25952  wilthimp  25954  basellem1  25963  basellem2  25964  basellem3  25965  basellem4  25966  basellem5  25967  basellem8  25970  vmaprm  25999  sgmval2  26025  0sgm  26026  sgmf  26027  vma1  26048  fsumdvdsdiaglem  26065  dvdsflf1o  26069  muinv  26075  dvdsmulf1o  26076  sgmppw  26078  1sgmprm  26080  1sgm2ppw  26081  sgmmul  26082  chtublem  26092  fsumvma2  26095  chpchtsum  26100  logfaclbnd  26103  logexprlim  26106  mersenne  26108  perfect1  26109  perfectlem1  26110  perfectlem2  26111  perfect  26112  dchrsum2  26149  dchrhash  26152  bcmono  26158  bcp1ctr  26160  bclbnd  26161  bposlem1  26165  bposlem2  26166  bposlem3  26167  bposlem5  26169  bposlem6  26170  lgsval2lem  26188  lgsqrlem2  26228  gausslemma2dlem6  26253  gausslemma2dlem7  26254  gausslemma2d  26255  lgseisenlem1  26256  lgseisenlem4  26259  lgsquadlem1  26261  lgsquadlem2  26262  lgsquadlem3  26263  lgsquad2  26267  m1lgs  26269  2sqlem3  26301  2sqlem4  26302  chebbnd1lem1  26350  chebbnd1  26353  rplogsumlem1  26365  rplogsumlem2  26366  rpvmasumlem  26368  dchrisumlem1  26370  dchrmusum2  26375  dchrvmasumlem1  26376  dchrvmasum2lem  26377  dchrvmasum2if  26378  dchrvmasumlem2  26379  dchrvmasumlem3  26380  dchrvmasumiflem1  26382  dchrisum0flblem1  26389  dchrisum0flblem2  26390  dchrisum0fno1  26392  rpvmasum2  26393  rplogsum  26408  mulogsumlem  26412  mulogsum  26413  mulog2sumlem2  26416  vmalogdivsum2  26419  vmalogdivsum  26420  2vmadivsumlem  26421  logsqvma  26423  selberglem2  26427  selberglem3  26428  selberg  26429  selberg2lem  26431  logdivbnd  26437  selberg3lem1  26438  selberg4lem1  26441  pntrsumo1  26446  pntrsumbnd2  26448  selberg3r  26450  selberg4r  26451  selberg34r  26452  pntsval2  26457  pntrlog2bndlem2  26459  pntrlog2bndlem4  26461  pntrlog2bndlem6  26464  pntpbnd1  26467  pntpbnd2  26468  pntlemg  26479  pntlemn  26481  pntlemf  26486  pnt  26495  padicabvf  26512  ostth2lem2  26515  ostth3  26519  fusgrhashclwwlkn  28162  eucrct2eupth  28328  numdenneg  30851  ltesubnnd  30856  1smat1  31468  madjusmdetlem2  31492  madjusmdetlem4  31494  qqhnm  31652  oddpwdc  32033  eulerpartlemsv2  32037  eulerpartlems  32039  eulerpartlemsv3  32040  eulerpartlemgc  32041  eulerpartlemv  32043  eulerpartlemgs2  32059  fibp1  32080  ballotlemfc0  32171  ballotlemfcc  32172  signsvtn0  32261  reprpmtf1o  32318  vtscl  32330  hgt750lemb  32348  tgoldbachgt  32355  subfacp1lem1  32854  subfacp1lem5  32859  subfacval2  32862  subfaclim  32863  cvmliftlem2  32961  cvmliftlem7  32966  cvmliftlem10  32969  cvmliftlem11  32970  cvmliftlem13  32971  bcm1nt  33421  bcprod  33422  iprodgam  33426  faclimlem1  33427  faclimlem2  33428  faclim2  33432  nn0prpwlem  34248  nn0prpw  34249  knoppndvlem16  34444  poimirlem1  35515  poimirlem2  35516  poimirlem6  35520  poimirlem7  35521  poimirlem8  35522  poimirlem9  35523  poimirlem10  35524  poimirlem11  35525  poimirlem12  35526  poimirlem13  35527  poimirlem15  35529  poimirlem16  35530  poimirlem17  35531  poimirlem18  35532  poimirlem19  35533  poimirlem20  35534  poimirlem21  35535  poimirlem22  35536  poimirlem23  35537  poimirlem24  35538  poimirlem25  35539  poimirlem26  35540  poimirlem27  35541  poimirlem31  35545  nnproddivdvdsd  39743  lcmfunnnd  39754  lcmineqlem3  39773  lcmineqlem4  39774  lcmineqlem6  39776  lcmineqlem8  39778  lcmineqlem10  39780  lcmineqlem11  39781  lcmineqlem12  39782  lcmineqlem16  39786  lcmineqlem18  39788  lcmineqlem23  39793  dvrelogpow2b  39809  aks4d1p1p2  39811  aks4d1p1  39817  2np3bcnp1  39822  2ap1caineq  39823  sticksstones10  39833  sticksstones12a  39835  sticksstones16  39840  sticksstones22  39846  metakunt8  39854  metakunt15  39861  metakunt16  39862  metakunt20  39866  metakunt28  39874  metakunt30  39876  nnadddir  40007  nnmul1com  40008  nnmulcom  40009  expgcd  40042  nn0expgcd  40043  numdenexp  40045  fltabcoprmex  40179  fltaccoprm  40180  fltbccoprm  40181  fltne  40184  flt4lem3  40188  flt4lem5elem  40191  flt4lem5a  40192  flt4lem5b  40193  flt4lem5c  40194  flt4lem5d  40195  flt4lem5e  40196  flt4lem5f  40197  flt4lem6  40198  flt4lem7  40199  nna4b4nsq  40200  fltltc  40201  fltnltalem  40202  fltnlta  40203  irrapxlem4  40350  irrapxlem5  40351  pellexlem2  40355  pellexlem6  40359  pell1234qrne0  40378  pell1234qrreccl  40379  pell1234qrmulcl  40380  pell1234qrdich  40386  pell14qrdich  40394  pell1qrge1  40395  pell1qr1  40396  pell14qrgapw  40401  rmxyneg  40445  rmxm1  40459  rmxluc  40461  rmxdbl  40464  jm2.19lem1  40514  jm2.27c  40532  relexpmulnn  40994  relexpmulg  40995  inductionexd  41442  hashnzfzclim  41613  bcccl  41630  bcc0  41631  bccp1k  41632  bccm1k  41633  binomcxplemwb  41639  fsumnncl  42788  mccllem  42813  clim1fr1  42817  sumnnodd  42846  dvsinexp  43127  dvxpaek  43156  dvnxpaek  43158  dvnprodlem2  43163  itgsinexplem1  43170  itgsinexp  43171  stoweidlem1  43217  stoweidlem11  43227  stoweidlem25  43241  stoweidlem26  43242  stoweidlem34  43250  stoweidlem37  43253  stoweidlem38  43254  stoweidlem42  43258  wallispi2lem1  43287  wallispi2  43289  stirlinglem4  43293  stirlinglem5  43294  stirlinglem10  43299  stirlinglem15  43304  dirkertrigeqlem3  43316  dirkertrigeq  43317  dirkercncflem2  43320  dirkercncflem4  43322  fourierdlem11  43334  fourierdlem15  43338  fourierdlem79  43401  fourierdlem83  43405  sqwvfourb  43445  etransclem14  43464  etransclem15  43465  etransclem20  43470  etransclem21  43471  etransclem22  43472  etransclem23  43473  etransclem24  43474  etransclem25  43475  etransclem28  43478  etransclem31  43481  etransclem32  43482  etransclem33  43483  etransclem34  43484  etransclem35  43485  etransclem38  43488  etransclem41  43491  etransclem44  43494  etransclem45  43495  etransclem47  43497  etransclem48  43498  nnfoctbdjlem  43668  deccarry  44476  iccpartgtprec  44545  fmtnoodd  44658  fmtnorec2lem  44667  fmtnorec2  44668  fmtnodvds  44669  goldbachthlem2  44671  fmtnorec3  44673  fmtnorec4  44674  fmtnoprmfac1lem  44689  fmtnoprmfac1  44690  fmtnoprmfac2lem1  44691  fmtnoprmfac2  44692  2pwp1prm  44714  sfprmdvdsmersenne  44728  lighneallem4b  44734  lighneal  44736  proththdlem  44738  proththd  44739  oexpnegALTV  44802  perfectALTVlem1  44846  perfectALTVlem2  44847  perfectALTV  44848  nnpw2pmod  45602  nnolog2flm1  45609  blennn0em1  45610  blengt1fldiv2p1  45612  nn0sumshdiglemB  45639  amgmlemALT  46178