Theorem nncn 12269

Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.)

Assertion

Ref	Expression
nncn	⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)

Proof of Theorem nncn

Step	Hyp	Ref	Expression
1		nnsscn 12266	. 2 ⊢ ℕ ⊆ ℂ
2	1	sseli 3930	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℂcc 11126  ℕcn 12261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402  ax-un 7740  ax-1cn 11186  ax-addcl 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7420  df-om 7867  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-nn 12262

This theorem is used by:  nncni  12271  nn1m1nn  12282  nn1suc  12283  nnaddcl  12284  nnmulcl  12285  nnadd1com  12287  nnaddcom  12288  nnmtmip  12290  nnneneg  12299  nnsub  12308  nndiv  12310  nndivtr  12311  nnnn0addcl  12562  nn0nnaddcl  12563  elnnnn0  12575  nn0sub  12582  nnnegz  12622  elz2  12637  zaddcl  12662  nnaddm1cl  12682  zdiv  12695  zdivadd  12696  zdivmul  12697  nneo  12709  peano5uzi  12714  elq  13003  qmulz  13004  qaddcl  13019  qnegcl  13020  qmulcl  13021  qreccl  13023  rpnnen1lem5  13035  nnledivrp  13160  nn0ledivnn  13161  fseq1m1p1  13658  ubmelm1fzo  13823  subfzo0  13853  quoremz  13920  quoremnn0ALT  13922  intfracq  13924  fldiv  13925  fldiv2  13926  modmulnn  13954  addmodid  13987  addmodidr  13988  modaddmodup  14002  modfzo0difsn  14011  modsumfzodifsn  14012  addmodlteq  14014  nn0ennn  14047  ser1const  14126  expneg  14137  expm1t  14158  nnsqcl  14196  nnlesq  14273  digit2  14304  digit1  14305  expnngt1  14309  facdiv  14355  facndiv  14356  faclbnd  14358  faclbnd4lem1  14361  faclbnd4lem4  14364  bcn1  14381  bcm1k  14383  bcp1n  14384  bcval5  14386  bcn2m1  14392  cshwidxmod  14878  cshwidxm  14883  cshwidxn  14884  repswcshw  14887  isercoll2  15760  divcnv  15946  harmonic  15952  arisum  15953  arisum2  15954  expcnv  15957  pwdif  15961  geomulcvg  15969  mertenslem2  15978  ef0lem  16170  efexp  16195  ruclem12  16335  sqrt2irr  16343  nndivides  16358  modmulconst  16384  dvdsflip  16413  nn0enne  16473  nno  16478  pwp1fsum  16487  divalgmod  16502  ndvdsadd  16506  modgcd  16628  gcdmultiplez  16631  gcddiv  16647  rpmulgcd  16653  rplpwr  16654  sqgcd  16658  expgcd  16659  nn0expgcd  16660  lcmgcdlem  16702  qredeq  16753  qredeu  16754  cncongrcoprm  16766  prmind2  16781  isprm6  16811  divnumden  16845  divdenle  16846  nn0gcdsq  16849  hashgcdlem  16885  pythagtriplem1  16914  pythagtriplem2  16915  pythagtriplem6  16919  pythagtriplem7  16920  pythagtriplem12  16924  pythagtriplem14  16926  pythagtriplem15  16927  pythagtriplem16  16928  pythagtriplem17  16929  pythagtriplem19  16931  pcqcl  16954  pcexp  16957  pcneg  16972  fldivp1  16995  oddprmdvds  17001  prmpwdvds  17002  infpnlem2  17009  prmreclem1  17014  prmreclem6  17019  4sqlem19  17061  vdwapun  17072  vdwapid1  17073  prmonn2  17137  prmgaplem7  17155  mulgnegnn  19213  mulgnnass  19238  mulgmodid  19242  odmod  19679  cnfldmulg  21623  prmirredlem  21691  znidomb  21780  znrrg  21784  cply1mul  22527  chfacfscmul0  23089  chfacfscmulfsupp  23090  chfacfscmulgsum  23091  chfacfpmmul0  23093  chfacfpmmulfsupp  23094  chfacfpmmulgsum  23095  cayhamlem1  23097  cpmadugsumlemF  23107  ovolunlem1  25731  uniioombllem3  25819  vitali  25847  mbfi1fseqlem3  25951  dvexp  26187  dvexp3  26212  plyeq0lem  26443  dgrcolem1  26506  aaliou3lem2  26586  aaliou3lem7  26592  pserdv2  26673  abelthlem6  26679  logtayl  26905  logtaylsum  26906  logtayl2  26907  cxpexp  26913  cxproot  26935  root1id  26999  root1eq1  27000  cxpeq  27002  logbgcd1irr  27039  atantayl  27182  atantayl2  27183  birthdaylem2  27197  dfef2  27215  emcllem2  27241  emcllem3  27242  zetacvg  27259  lgam1  27308  gamfac  27311  basellem2  27326  basellem3  27327  basellem5  27329  basellem8  27332  mumul  27425  fsumdvdscom  27429  muinv  27437  chtublem  27455  perfect  27475  pcbcctr  27520  bclbnd  27524  bposlem1  27528  bposlem6  27533  lgssq2  27582  gausslemma2dlem1a  27609  gausslemma2dlem3  27612  2lgslem1a1  27633  2sqlem6  27667  2sqlem10  27672  2sqnn  27683  2sqreunnltlem  27694  rplogsumlem1  27728  dchrmusumlema  27737  dchrmusum2  27738  dchrvmasumiflem1  27745  dchrvmaeq0  27748  dchrisum0re  27757  logdivbnd  27800  cusgrsize2inds  29921  wlkdlem2  30149  crctcshwlkn0lem1  30286  crctcshwlkn0lem6  30291  0enwwlksnge1  30340  wspthsnonn0vne  30393  clwwlknwwlksn  30516  clwwlkinwwlk  30518  clwwlkel  30524  clwwlkf  30525  clwwlkf1  30527  wwlksubclwwlk  30536  eucrctshift  30731  eucrct2eupth  30733  numclwwlk2lem1  30864  numclwlk2lem2f  30865  numclwlk2lem2f1o  30867  ipasslem4  31323  ipasslem5  31324  isarchi3  33635  oddpwdc  34873  eulerpartlemb  34887  fibp1  34920  subfacp1lem6  35772  subfaclim  35775  snmlff  35916  circum  36261  divcnvlin  36320  bcprod  36325  iprodgam  36329  faclim  36333  faclim2  36335  nn0prpwlem  36949  nndivsub  37084  knoppndvlem13  37229  poimirlem13  38390  poimirlem14  38391  poimirlem29  38406  poimirlem30  38407  poimirlem31  38408  poimirlem32  38409  mblfinlem2  38415  ovoliunnfl  38419  voliunnfl  38421  facp2  43017  dvdsexpnn0  43217  renegmulnnass  43361  fimgmcyc  43424  dffltz  43488  irrapxlem1  43671  pellexlem1  43678  pellqrex  43728  2nn0ind  43794  jm2.17c  43811  acongrep  43829  jm2.18  43837  jm2.20nn  43846  jm2.16nn0  43853  proot1ex  44045  hashnzfzclim  45154  binomcxplemnotnn0  45188  nnsplit  46196  clim1fr1  46439  sumnnodd  46468  wallispilem4  46904  wallispilem5  46905  wallispi  46906  wallispi2lem1  46907  wallispi2lem2  46908  wallispi2  46909  stirlinglem1  46910  stirlinglem3  46912  stirlinglem4  46913  stirlinglem5  46914  stirlinglem6  46915  stirlinglem7  46916  stirlinglem8  46917  stirlinglem10  46919  stirlinglem11  46920  stirlinglem12  46921  stirlinglem13  46922  stirlinglem14  46923  stirlinglem15  46924  dirkerper  46932  dirkertrigeqlem1  46934  fouriersw  47067  nnfoctbdjlem  47291  sqrtnnaa  47739  deccarry  48207  subsubelfzo0  48223  submodlt  48252  mod0mul  48258  m1modmmod  48260  modlt0b  48265  sqrtpwpw2p  48449  fmtnodvds  48455  fmtnoprmfac1  48476  fmtnoprmfac2lem1  48477  fmtnoprmfac2  48478  lighneallem2  48517  lighneallem3  48518  lighneallem4  48521  nnennexALTV  48625  perfectALTV  48647  fppr2odd  48655  fpprwppr  48663  fpprwpprb  48664  tgoldbachlt  48740  gpgedgvtx0  48985  gpg3kgrtriexlem2  49008  gpg3kgrtriexlem5  49011  gpg3kgrtriex  49013  nnsgrp  49100  nnsgrpnmnd  49101  bcpascm1  49289  altgsumbcALT  49291  eluz2cnn0n1  49449  pw2m1lepw2m1  49458  nnennex  49463  logbpw2m1  49505  blenpw2m1  49517  nnpw2blen  49518  nnpw2pmod  49521  blennnt2  49527  blennn0em1  49529  nn0digval  49538  dignn0fr  49539  dignn0ldlem  49540  dig0  49544  nn0sumshdiglemA  49557  nn0sumshdiglemB  49558  nn0sumshdiglem1  49559