Theorem nncnd 12228

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℂcc 11108  ℕcn 12212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-1cn 11168  ax-addcl 11170

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-nn 12213

This theorem is referenced by:  nneo  12646  facdiv  14247  facndiv  14248  faclbnd  14250  faclbnd5  14258  faclbnd6  14259  facubnd  14260  facavg  14261  bccmpl  14269  bcn0  14270  bcn1  14273  bcm1k  14275  bcp1n  14276  bcp1nk  14277  bcval5  14278  bcpasc  14281  permnn  14286  hashf1  14418  hashfac  14419  relexpaddnn  14998  binom11  15778  binom1dif  15779  climcndslem2  15796  arisum2  15807  trireciplem  15808  trirecip  15809  geo2sum  15819  geo2lim  15821  fprodfac  15917  risefacfac  15979  fallfacfwd  15980  fallfacval4  15987  bcfallfac  15988  fallfacfac  15989  bpolycl  15996  bpolysum  15997  bpolydiflem  15998  fsumkthpow  16000  eftcl  16017  eftabs  16019  efcllem  16021  ege2le3  16033  efcj  16035  efaddlem  16036  eftlub  16052  eirrlem  16147  sqrt2irrlem  16191  oexpneg  16288  pwp1fsum  16334  bitsp1  16372  bitsfzolem  16375  bitsfzo  16376  bitsmod  16377  bitscmp  16379  bitsinv1lem  16382  bitsinv1  16383  2ebits  16388  bitsinvp1  16390  sadcaddlem  16398  sadadd3  16402  bitsres  16414  bitsuz  16415  bitsshft  16416  dvdsgcdidd  16479  mulgcd  16490  rplpwr  16499  sqgcd  16502  lcmgcdlem  16543  3lcm2e6woprm  16552  coprmprod  16598  coprmproddvdslem  16599  cncongr1  16604  cncongr2  16605  prmind2  16622  isprm5  16644  divgcdodd  16647  prmdvdsexpr  16654  qmuldeneqnum  16683  divnumden  16684  qnumgt0  16686  numdensq  16690  hashdvds  16708  phiprmpw  16709  prmdiv  16718  prmdivdiv  16720  phisum  16723  modprm0  16738  pythagtriplem4  16752  pythagtriplem6  16754  pythagtriplem7  16755  pythagtriplem14  16761  pythagtriplem15  16762  pythagtriplem19  16766  pythagtrip  16767  pcprendvds2  16774  pcpre1  16775  pcpremul  16776  pceulem  16778  pcdiv  16785  pcqmul  16786  pcelnn  16803  pcid  16806  pc2dvds  16812  dvdsprmpweqnn  16818  dvdsprmpweqle  16819  pcaddlem  16821  pcadd  16822  pcfaclem  16831  qexpz  16834  expnprm  16835  oddprmdvds  16836  prmpwdvds  16837  pockthlem  16838  pockthg  16839  infpnlem1  16843  prmreclem1  16849  prmreclem2  16850  prmreclem3  16851  prmreclem4  16852  prmreclem6  16854  4sqlem6  16876  4sqlem7  16877  4sqlem10  16880  mul4sqlem  16886  4sqlem11  16888  4sqlem12  16889  4sqlem14  16891  4sqlem17  16894  4sqlem18  16895  vdwlem1  16914  vdwlem2  16915  vdwlem3  16916  vdwlem5  16918  vdwlem6  16919  vdwlem8  16921  vdwlem9  16922  vdwlem10  16923  vdwlem12  16925  ramub1lem2  16960  ramcl  16962  prmop1  16971  prmdvdsprmo  16975  prmgaplem7  16990  prmgaplem8  16991  gsumsgrpccat  18721  mulgnndir  18983  mulgnnass  18989  psgnunilem5  19362  odf1o2  19441  pgp0  19464  sylow1lem1  19466  odcau  19472  sylow2blem3  19490  sylow3lem3  19497  sylow3lem4  19498  gexexlem  19720  ablfacrp2  19937  ablfac1lem  19938  ablfac1eu  19943  pgpfac1lem3a  19946  pgpfac1lem3  19947  fincygsubgodexd  19983  zringlpirlem3  21034  znrrg  21121  cpmadugsumlemF  22378  lebnumlem3  24479  ovollb2lem  25005  ovolunlem1a  25013  ovolunlem1  25014  uniioombllem3  25102  uniioombllem4  25103  dyaddisjlem  25112  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  itgpowd  25567  dgrcolem1  25787  vieta1lem1  25823  vieta1lem2  25824  elqaalem2  25833  elqaalem3  25834  aalioulem1  25845  aaliou3lem2  25856  aaliou3lem8  25858  aaliou3lem6  25861  aaliou3lem9  25863  taylfvallem1  25869  tayl0  25874  taylply2  25880  taylply  25881  dvtaylp  25882  taylthlem1  25885  taylthlem2  25886  pserdvlem2  25940  advlogexp  26163  cxpmul2  26197  cxpeq  26265  atantayl3  26444  leibpi  26447  log2cnv  26449  log2tlbnd  26450  birthdaylem2  26457  birthdaylem3  26458  amgmlem  26494  amgm  26495  emcllem5  26504  fsumharmonic  26516  zetacvg  26519  dmgmdivn0  26532  lgamgulmlem3  26535  lgamgulmlem4  26536  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamgulm2  26540  lgamcvg2  26559  gamcvg  26560  gamcvg2lem  26563  facgam  26570  wilthlem1  26572  wilthlem2  26573  wilthlem3  26574  wilthimp  26576  basellem1  26585  basellem2  26586  basellem3  26587  basellem4  26588  basellem5  26589  basellem8  26592  vmaprm  26621  sgmval2  26647  0sgm  26648  sgmf  26649  vma1  26670  fsumdvdsdiaglem  26687  dvdsflf1o  26691  muinv  26697  dvdsmulf1o  26698  sgmppw  26700  1sgmprm  26702  1sgm2ppw  26703  sgmmul  26704  chtublem  26714  fsumvma2  26717  chpchtsum  26722  logfaclbnd  26725  logexprlim  26728  mersenne  26730  perfect1  26731  perfectlem1  26732  perfectlem2  26733  perfect  26734  dchrsum2  26771  dchrhash  26774  bcmono  26780  bcp1ctr  26782  bclbnd  26783  bposlem1  26787  bposlem2  26788  bposlem3  26789  bposlem5  26791  bposlem6  26792  lgsval2lem  26810  lgsqrlem2  26850  gausslemma2dlem6  26875  gausslemma2dlem7  26876  gausslemma2d  26877  lgseisenlem1  26878  lgseisenlem4  26881  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  lgsquad2  26889  m1lgs  26891  2sqlem3  26923  2sqlem4  26924  chebbnd1lem1  26972  chebbnd1  26975  rplogsumlem1  26987  rplogsumlem2  26988  rpvmasumlem  26990  dchrisumlem1  26992  dchrmusum2  26997  dchrvmasumlem1  26998  dchrvmasum2lem  26999  dchrvmasum2if  27000  dchrvmasumlem2  27001  dchrvmasumlem3  27002  dchrvmasumiflem1  27004  dchrisum0flblem1  27011  dchrisum0flblem2  27012  dchrisum0fno1  27014  rpvmasum2  27015  rplogsum  27030  mulogsumlem  27034  mulogsum  27035  mulog2sumlem2  27038  vmalogdivsum2  27041  vmalogdivsum  27042  2vmadivsumlem  27043  logsqvma  27045  selberglem2  27049  selberglem3  27050  selberg  27051  selberg2lem  27053  logdivbnd  27059  selberg3lem1  27060  selberg4lem1  27063  pntrsumo1  27068  pntrsumbnd2  27070  selberg3r  27072  selberg4r  27073  selberg34r  27074  pntsval2  27079  pntrlog2bndlem2  27081  pntrlog2bndlem4  27083  pntrlog2bndlem6  27086  pntpbnd1  27089  pntpbnd2  27090  pntlemg  27101  pntlemn  27103  pntlemf  27108  pnt  27117  padicabvf  27134  ostth2lem2  27137  ostth3  27141  fusgrhashclwwlkn  29332  eucrct2eupth  29498  nrt2irr  29726  numdenneg  32023  ltesubnnd  32028  1smat1  32784  madjusmdetlem2  32808  madjusmdetlem4  32810  qqhnm  32970  oddpwdc  33353  eulerpartlemsv2  33357  eulerpartlems  33359  eulerpartlemsv3  33360  eulerpartlemgc  33361  eulerpartlemv  33363  eulerpartlemgs2  33379  fibp1  33400  ballotlemfc0  33491  ballotlemfcc  33492  signsvtn0  33581  reprpmtf1o  33638  vtscl  33650  hgt750lemb  33668  tgoldbachgt  33675  subfacp1lem1  34170  subfacp1lem5  34175  subfacval2  34178  subfaclim  34179  cvmliftlem2  34277  cvmliftlem7  34282  cvmliftlem10  34285  cvmliftlem11  34286  cvmliftlem13  34287  bcm1nt  34707  bcprod  34708  iprodgam  34712  faclimlem1  34713  faclimlem2  34714  faclim2  34718  nn0prpwlem  35207  nn0prpw  35208  knoppndvlem16  35403  poimirlem1  36489  poimirlem2  36490  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem9  36497  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  nnproddivdvdsd  40866  lcmfunnnd  40877  lcmineqlem3  40896  lcmineqlem4  40897  lcmineqlem6  40899  lcmineqlem8  40901  lcmineqlem10  40903  lcmineqlem11  40904  lcmineqlem12  40905  lcmineqlem16  40909  lcmineqlem18  40911  lcmineqlem23  40916  dvrelogpow2b  40933  aks4d1p1p2  40935  aks4d1p1  40941  aks4d1p8  40952  aks6d1c2p2  40957  2np3bcnp1  40960  2ap1caineq  40961  sticksstones10  40971  sticksstones12a  40973  sticksstones16  40978  sticksstones22  40984  metakunt8  40992  metakunt15  40999  metakunt16  41000  metakunt20  41004  metakunt28  41012  metakunt30  41014  nnadddir  41184  nnmul1com  41185  nnmulcom  41186  oddnumth  41209  nicomachus  41210  expgcd  41225  nn0expgcd  41226  numdenexp  41228  zaddcom  41325  fltabcoprmex  41381  fltaccoprm  41382  fltbccoprm  41383  fltne  41386  flt4lem3  41390  flt4lem5elem  41393  flt4lem5a  41394  flt4lem5b  41395  flt4lem5c  41396  flt4lem5d  41397  flt4lem5e  41398  flt4lem5f  41399  flt4lem6  41400  flt4lem7  41401  nna4b4nsq  41402  fltltc  41403  fltnltalem  41404  fltnlta  41405  irrapxlem4  41563  irrapxlem5  41564  pellexlem2  41568  pellexlem6  41572  pell1234qrne0  41591  pell1234qrreccl  41592  pell1234qrmulcl  41593  pell1234qrdich  41599  pell14qrdich  41607  pell1qrge1  41608  pell1qr1  41609  pell14qrgapw  41614  rmxyneg  41659  rmxm1  41673  rmxluc  41675  rmxdbl  41678  jm2.19lem1  41728  jm2.27c  41746  relexpmulnn  42460  relexpmulg  42461  inductionexd  42906  hashnzfzclim  43081  bcccl  43098  bcc0  43099  bccp1k  43100  bccm1k  43101  binomcxplemwb  43107  fsumnncl  44288  mccllem  44313  clim1fr1  44317  sumnnodd  44346  dvsinexp  44627  dvxpaek  44656  dvnxpaek  44658  dvnprodlem2  44663  itgsinexplem1  44670  itgsinexp  44671  stoweidlem1  44717  stoweidlem11  44727  stoweidlem25  44741  stoweidlem26  44742  stoweidlem34  44750  stoweidlem37  44753  stoweidlem38  44754  stoweidlem42  44758  wallispi2lem1  44787  wallispi2  44789  stirlinglem4  44793  stirlinglem5  44794  stirlinglem10  44799  stirlinglem15  44804  dirkertrigeqlem3  44816  dirkertrigeq  44817  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem11  44834  fourierdlem15  44838  fourierdlem79  44901  fourierdlem83  44905  sqwvfourb  44945  etransclem14  44964  etransclem15  44965  etransclem20  44970  etransclem21  44971  etransclem22  44972  etransclem23  44973  etransclem24  44974  etransclem25  44975  etransclem28  44978  etransclem31  44981  etransclem32  44982  etransclem33  44983  etransclem34  44984  etransclem35  44985  etransclem38  44988  etransclem41  44991  etransclem44  44994  etransclem45  44995  etransclem47  44997  etransclem48  44998  nnfoctbdjlem  45171  deccarry  46019  iccpartgtprec  46088  fmtnoodd  46201  fmtnorec2lem  46210  fmtnorec2  46211  fmtnodvds  46212  goldbachthlem2  46214  fmtnorec3  46216  fmtnorec4  46217  fmtnoprmfac1lem  46232  fmtnoprmfac1  46233  fmtnoprmfac2lem1  46234  fmtnoprmfac2  46235  2pwp1prm  46257  sfprmdvdsmersenne  46271  lighneallem4b  46277  lighneal  46279  proththdlem  46281  proththd  46282  oexpnegALTV  46345  perfectALTVlem1  46389  perfectALTVlem2  46390  perfectALTV  46391  nnpw2pmod  47269  nnolog2flm1  47276  blennn0em1  47277  blengt1fldiv2p1  47279  nn0sumshdiglemB  47306  amgmlemALT  47850