Theorem nncnd 12035

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

Syntax hints:   → wi 4   ∈ wcel 2104  ℂcc 10915  ℕcn 12019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7620  ax-1cn 10975  ax-addcl 10977

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-ov 7310  df-om 7745  df-2nd 7864  df-frecs 8128  df-wrecs 8159  df-recs 8233  df-rdg 8272  df-nn 12020

This theorem is referenced by:  facdiv  14047  facndiv  14048  faclbnd  14050  faclbnd5  14058  faclbnd6  14059  facubnd  14060  facavg  14061  bccmpl  14069  bcn0  14070  bcn1  14073  bcm1k  14075  bcp1n  14076  bcp1nk  14077  bcval5  14078  bcpasc  14081  permnn  14086  hashf1  14216  hashfac  14217  relexpaddnn  14807  binom11  15589  binom1dif  15590  climcndslem2  15607  arisum2  15618  trireciplem  15619  trirecip  15620  geo2sum  15630  geo2lim  15632  fprodfac  15728  risefacfac  15790  fallfacfwd  15791  fallfacval4  15798  bcfallfac  15799  fallfacfac  15800  bpolycl  15807  bpolysum  15808  bpolydiflem  15809  fsumkthpow  15811  eftcl  15828  eftabs  15830  efcllem  15832  ege2le3  15844  efcj  15846  efaddlem  15847  eftlub  15863  eirrlem  15958  sqrt2irrlem  16002  oexpneg  16099  pwp1fsum  16145  bitsp1  16183  bitsfzolem  16186  bitsfzo  16187  bitsmod  16188  bitscmp  16190  bitsinv1lem  16193  bitsinv1  16194  2ebits  16199  bitsinvp1  16201  sadcaddlem  16209  sadadd3  16213  bitsres  16225  bitsuz  16226  bitsshft  16227  dvdsgcdidd  16290  mulgcd  16301  rplpwr  16312  sqgcd  16315  lcmgcdlem  16356  3lcm2e6woprm  16365  coprmprod  16411  coprmproddvdslem  16412  cncongr1  16417  cncongr2  16418  prmind2  16435  isprm5  16457  divgcdodd  16460  prmdvdsexpr  16467  qmuldeneqnum  16496  divnumden  16497  qnumgt0  16499  numdensq  16503  hashdvds  16521  phiprmpw  16522  prmdiv  16531  prmdivdiv  16533  phisum  16536  modprm0  16551  pythagtriplem4  16565  pythagtriplem6  16567  pythagtriplem7  16568  pythagtriplem14  16574  pythagtriplem15  16575  pythagtriplem19  16579  pythagtrip  16580  pcprendvds2  16587  pcpre1  16588  pcpremul  16589  pceulem  16591  pcdiv  16598  pcqmul  16599  pcelnn  16616  pcid  16619  pc2dvds  16625  dvdsprmpweqnn  16631  dvdsprmpweqle  16632  pcaddlem  16634  pcadd  16635  pcfaclem  16644  qexpz  16647  expnprm  16648  oddprmdvds  16649  prmpwdvds  16650  pockthlem  16651  pockthg  16652  infpnlem1  16656  prmreclem1  16662  prmreclem2  16663  prmreclem3  16664  prmreclem4  16665  prmreclem6  16667  4sqlem6  16689  4sqlem7  16690  4sqlem10  16693  mul4sqlem  16699  4sqlem11  16701  4sqlem12  16702  4sqlem14  16704  4sqlem17  16707  4sqlem18  16708  vdwlem1  16727  vdwlem2  16728  vdwlem3  16729  vdwlem5  16731  vdwlem6  16732  vdwlem8  16734  vdwlem9  16735  vdwlem10  16736  vdwlem12  16738  ramub1lem2  16773  ramcl  16775  prmop1  16784  prmdvdsprmo  16788  prmgaplem7  16803  prmgaplem8  16804  gsumsgrpccat  18523  gsumccatOLD  18524  mulgnndir  18777  mulgnnass  18783  psgnunilem5  19147  odf1o2  19223  pgp0  19246  sylow1lem1  19248  odcau  19254  sylow2blem3  19272  sylow3lem3  19279  sylow3lem4  19280  gexexlem  19498  ablfacrp2  19715  ablfac1lem  19716  ablfac1eu  19721  pgpfac1lem3a  19724  pgpfac1lem3  19725  fincygsubgodexd  19761  zringlpirlem3  20731  znrrg  20818  cpmadugsumlemF  22070  lebnumlem3  24171  ovollb2lem  24697  ovolunlem1a  24705  ovolunlem1  24706  uniioombllem3  24794  uniioombllem4  24795  dyaddisjlem  24804  mbfi1fseqlem3  24927  mbfi1fseqlem4  24928  itgpowd  25259  dgrcolem1  25479  vieta1lem1  25515  vieta1lem2  25516  elqaalem2  25525  elqaalem3  25526  aalioulem1  25537  aaliou3lem2  25548  aaliou3lem8  25550  aaliou3lem6  25553  aaliou3lem9  25555  taylfvallem1  25561  tayl0  25566  taylply2  25572  taylply  25573  dvtaylp  25574  taylthlem1  25577  taylthlem2  25578  pserdvlem2  25632  advlogexp  25855  cxpmul2  25889  cxpeq  25955  atantayl3  26134  leibpi  26137  log2cnv  26139  log2tlbnd  26140  birthdaylem2  26147  birthdaylem3  26148  amgmlem  26184  amgm  26185  emcllem5  26194  fsumharmonic  26206  zetacvg  26209  dmgmdivn0  26222  lgamgulmlem3  26225  lgamgulmlem4  26226  lgamgulmlem5  26227  lgamgulmlem6  26228  lgamgulm2  26230  lgamcvg2  26249  gamcvg  26250  gamcvg2lem  26253  facgam  26260  wilthlem1  26262  wilthlem2  26263  wilthlem3  26264  wilthimp  26266  basellem1  26275  basellem2  26276  basellem3  26277  basellem4  26278  basellem5  26279  basellem8  26282  vmaprm  26311  sgmval2  26337  0sgm  26338  sgmf  26339  vma1  26360  fsumdvdsdiaglem  26377  dvdsflf1o  26381  muinv  26387  dvdsmulf1o  26388  sgmppw  26390  1sgmprm  26392  1sgm2ppw  26393  sgmmul  26394  chtublem  26404  fsumvma2  26407  chpchtsum  26412  logfaclbnd  26415  logexprlim  26418  mersenne  26420  perfect1  26421  perfectlem1  26422  perfectlem2  26423  perfect  26424  dchrsum2  26461  dchrhash  26464  bcmono  26470  bcp1ctr  26472  bclbnd  26473  bposlem1  26477  bposlem2  26478  bposlem3  26479  bposlem5  26481  bposlem6  26482  lgsval2lem  26500  lgsqrlem2  26540  gausslemma2dlem6  26565  gausslemma2dlem7  26566  gausslemma2d  26567  lgseisenlem1  26568  lgseisenlem4  26571  lgsquadlem1  26573  lgsquadlem2  26574  lgsquadlem3  26575  lgsquad2  26579  m1lgs  26581  2sqlem3  26613  2sqlem4  26614  chebbnd1lem1  26662  chebbnd1  26665  rplogsumlem1  26677  rplogsumlem2  26678  rpvmasumlem  26680  dchrisumlem1  26682  dchrmusum2  26687  dchrvmasumlem1  26688  dchrvmasum2lem  26689  dchrvmasum2if  26690  dchrvmasumlem2  26691  dchrvmasumlem3  26692  dchrvmasumiflem1  26694  dchrisum0flblem1  26701  dchrisum0flblem2  26702  dchrisum0fno1  26704  rpvmasum2  26705  rplogsum  26720  mulogsumlem  26724  mulogsum  26725  mulog2sumlem2  26728  vmalogdivsum2  26731  vmalogdivsum  26732  2vmadivsumlem  26733  logsqvma  26735  selberglem2  26739  selberglem3  26740  selberg  26741  selberg2lem  26743  logdivbnd  26749  selberg3lem1  26750  selberg4lem1  26753  pntrsumo1  26758  pntrsumbnd2  26760  selberg3r  26762  selberg4r  26763  selberg34r  26764  pntsval2  26769  pntrlog2bndlem2  26771  pntrlog2bndlem4  26773  pntrlog2bndlem6  26776  pntpbnd1  26779  pntpbnd2  26780  pntlemg  26791  pntlemn  26793  pntlemf  26798  pnt  26807  padicabvf  26824  ostth2lem2  26827  ostth3  26831  fusgrhashclwwlkn  28488  eucrct2eupth  28654  numdenneg  31176  ltesubnnd  31181  1smat1  31799  madjusmdetlem2  31823  madjusmdetlem4  31825  qqhnm  31985  oddpwdc  32366  eulerpartlemsv2  32370  eulerpartlems  32372  eulerpartlemsv3  32373  eulerpartlemgc  32374  eulerpartlemv  32376  eulerpartlemgs2  32392  fibp1  32413  ballotlemfc0  32504  ballotlemfcc  32505  signsvtn0  32594  reprpmtf1o  32651  vtscl  32663  hgt750lemb  32681  tgoldbachgt  32688  subfacp1lem1  33186  subfacp1lem5  33191  subfacval2  33194  subfaclim  33195  cvmliftlem2  33293  cvmliftlem7  33298  cvmliftlem10  33301  cvmliftlem11  33302  cvmliftlem13  33303  bcm1nt  33748  bcprod  33749  iprodgam  33753  faclimlem1  33754  faclimlem2  33755  faclim2  33759  nn0prpwlem  34556  nn0prpw  34557  knoppndvlem16  34752  poimirlem1  35822  poimirlem2  35823  poimirlem6  35827  poimirlem7  35828  poimirlem8  35829  poimirlem9  35830  poimirlem10  35831  poimirlem11  35832  poimirlem12  35833  poimirlem13  35834  poimirlem15  35836  poimirlem16  35837  poimirlem17  35838  poimirlem18  35839  poimirlem19  35840  poimirlem20  35841  poimirlem21  35842  poimirlem22  35843  poimirlem23  35844  poimirlem24  35845  poimirlem25  35846  poimirlem26  35847  poimirlem27  35848  poimirlem31  35852  nnproddivdvdsd  40051  lcmfunnnd  40062  lcmineqlem3  40081  lcmineqlem4  40082  lcmineqlem6  40084  lcmineqlem8  40086  lcmineqlem10  40088  lcmineqlem11  40089  lcmineqlem12  40090  lcmineqlem16  40094  lcmineqlem18  40096  lcmineqlem23  40101  dvrelogpow2b  40118  aks4d1p1p2  40120  aks4d1p1  40126  aks4d1p8  40137  2np3bcnp1  40142  2ap1caineq  40143  sticksstones10  40153  sticksstones12a  40155  sticksstones16  40160  sticksstones22  40166  metakunt8  40174  metakunt15  40181  metakunt16  40182  metakunt20  40186  metakunt28  40194  metakunt30  40196  nnadddir  40337  nnmul1com  40338  nnmulcom  40339  expgcd  40371  nn0expgcd  40372  numdenexp  40374  fltabcoprmex  40513  fltaccoprm  40514  fltbccoprm  40515  fltne  40518  flt4lem3  40522  flt4lem5elem  40525  flt4lem5a  40526  flt4lem5b  40527  flt4lem5c  40528  flt4lem5d  40529  flt4lem5e  40530  flt4lem5f  40531  flt4lem6  40532  flt4lem7  40533  nna4b4nsq  40534  fltltc  40535  fltnltalem  40536  fltnlta  40537  irrapxlem4  40684  irrapxlem5  40685  pellexlem2  40689  pellexlem6  40693  pell1234qrne0  40712  pell1234qrreccl  40713  pell1234qrmulcl  40714  pell1234qrdich  40720  pell14qrdich  40728  pell1qrge1  40729  pell1qr1  40730  pell14qrgapw  40735  rmxyneg  40780  rmxm1  40794  rmxluc  40796  rmxdbl  40799  jm2.19lem1  40849  jm2.27c  40867  relexpmulnn  41355  relexpmulg  41356  inductionexd  41803  hashnzfzclim  41978  bcccl  41995  bcc0  41996  bccp1k  41997  bccm1k  41998  binomcxplemwb  42004  fsumnncl  43162  mccllem  43187  clim1fr1  43191  sumnnodd  43220  dvsinexp  43501  dvxpaek  43530  dvnxpaek  43532  dvnprodlem2  43537  itgsinexplem1  43544  itgsinexp  43545  stoweidlem1  43591  stoweidlem11  43601  stoweidlem25  43615  stoweidlem26  43616  stoweidlem34  43624  stoweidlem37  43627  stoweidlem38  43628  stoweidlem42  43632  wallispi2lem1  43661  wallispi2  43663  stirlinglem4  43667  stirlinglem5  43668  stirlinglem10  43673  stirlinglem15  43678  dirkertrigeqlem3  43690  dirkertrigeq  43691  dirkercncflem2  43694  dirkercncflem4  43696  fourierdlem11  43708  fourierdlem15  43712  fourierdlem79  43775  fourierdlem83  43779  sqwvfourb  43819  etransclem14  43838  etransclem15  43839  etransclem20  43844  etransclem21  43845  etransclem22  43846  etransclem23  43847  etransclem24  43848  etransclem25  43849  etransclem28  43852  etransclem31  43855  etransclem32  43856  etransclem33  43857  etransclem34  43858  etransclem35  43859  etransclem38  43862  etransclem41  43865  etransclem44  43868  etransclem45  43869  etransclem47  43871  etransclem48  43872  nnfoctbdjlem  44043  deccarry  44861  iccpartgtprec  44930  fmtnoodd  45043  fmtnorec2lem  45052  fmtnorec2  45053  fmtnodvds  45054  goldbachthlem2  45056  fmtnorec3  45058  fmtnorec4  45059  fmtnoprmfac1lem  45074  fmtnoprmfac1  45075  fmtnoprmfac2lem1  45076  fmtnoprmfac2  45077  2pwp1prm  45099  sfprmdvdsmersenne  45113  lighneallem4b  45119  lighneal  45121  proththdlem  45123  proththd  45124  oexpnegALTV  45187  perfectALTVlem1  45231  perfectALTVlem2  45232  perfectALTV  45233  nnpw2pmod  45987  nnolog2flm1  45994  blennn0em1  45995  blengt1fldiv2p1  45997  nn0sumshdiglemB  46024  amgmlemALT  46565