Theorem nncn 12153

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 12150	. 2 ⊢ ℕ ⊆ ℂ
2	1	sseli 3929	1 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11024  ℕcn 12145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146

This theorem is referenced by:  nncni  12155  nn1m1nn  12166  nn1suc  12167  nnaddcl  12168  nnmulcl  12169  nnmtmip  12171  nnneneg  12180  nnsub  12189  nndiv  12191  nndivtr  12192  nnnn0addcl  12431  nn0nnaddcl  12432  elnnnn0  12444  nn0sub  12451  nnnegz  12491  elz2  12506  zaddcl  12531  nnaddm1cl  12549  zdiv  12562  zdivadd  12563  zdivmul  12564  nneo  12576  peano5uzi  12581  elq  12863  qmulz  12864  qaddcl  12878  qnegcl  12879  qmulcl  12880  qreccl  12882  rpnnen1lem5  12894  nnledivrp  13019  nn0ledivnn  13020  fseq1m1p1  13515  ubmelm1fzo  13679  subfzo0  13708  quoremz  13775  quoremnn0ALT  13777  intfracq  13779  fldiv  13780  fldiv2  13781  modmulnn  13809  addmodid  13842  addmodidr  13843  modaddmodup  13857  modfzo0difsn  13866  modsumfzodifsn  13867  addmodlteq  13869  nn0ennn  13902  ser1const  13981  expneg  13992  expm1t  14013  nnsqcl  14051  nnlesq  14128  digit2  14159  digit1  14160  expnngt1  14164  facdiv  14210  facndiv  14211  faclbnd  14213  faclbnd4lem1  14216  faclbnd4lem4  14219  bcn1  14236  bcm1k  14238  bcp1n  14239  bcval5  14241  bcn2m1  14247  cshwidxmod  14726  cshwidxm  14731  cshwidxn  14732  repswcshw  14735  isercoll2  15592  divcnv  15776  harmonic  15782  arisum  15783  arisum2  15784  expcnv  15787  pwdif  15791  geomulcvg  15799  mertenslem2  15808  ef0lem  16001  efexp  16026  ruclem12  16166  sqrt2irr  16174  nndivides  16189  modmulconst  16215  dvdsflip  16244  nn0enne  16304  nno  16309  pwp1fsum  16318  divalgmod  16333  ndvdsadd  16337  modgcd  16459  gcdmultiplez  16462  gcddiv  16478  rpmulgcd  16484  rplpwr  16485  sqgcd  16489  expgcd  16490  nn0expgcd  16491  lcmgcdlem  16533  qredeq  16584  qredeu  16585  cncongrcoprm  16597  prmind2  16612  isprm6  16641  divnumden  16675  divdenle  16676  nn0gcdsq  16679  hashgcdlem  16715  pythagtriplem1  16744  pythagtriplem2  16745  pythagtriplem6  16749  pythagtriplem7  16750  pythagtriplem12  16754  pythagtriplem14  16756  pythagtriplem15  16757  pythagtriplem16  16758  pythagtriplem17  16759  pythagtriplem19  16761  pcqcl  16784  pcexp  16787  pcneg  16802  fldivp1  16825  oddprmdvds  16831  prmpwdvds  16832  infpnlem2  16839  prmreclem1  16844  prmreclem6  16849  4sqlem19  16891  vdwapun  16902  vdwapid1  16903  prmonn2  16967  prmgaplem7  16985  mulgnegnn  19014  mulgnnass  19039  mulgmodid  19043  odmod  19475  cnfldmulg  21358  prmirredlem  21427  znidomb  21516  znrrg  21520  cply1mul  22240  chfacfscmul0  22802  chfacfscmulfsupp  22803  chfacfscmulgsum  22804  chfacfpmmul0  22806  chfacfpmmulfsupp  22807  chfacfpmmulgsum  22808  cayhamlem1  22810  cpmadugsumlemF  22820  ovolunlem1  25454  uniioombllem3  25542  vitali  25570  mbfi1fseqlem3  25674  dvexp  25913  dvexp3  25938  plyeq0lem  26171  dgrcolem1  26235  aaliou3lem2  26307  aaliou3lem7  26313  pserdv2  26396  abelthlem6  26402  logtayl  26625  logtaylsum  26626  logtayl2  26627  cxpexp  26633  cxproot  26655  root1id  26720  root1eq1  26721  cxpeq  26723  logbgcd1irr  26760  atantayl  26903  atantayl2  26904  birthdaylem2  26918  dfef2  26937  emcllem2  26963  emcllem3  26964  zetacvg  26981  lgam1  27030  gamfac  27033  basellem2  27048  basellem3  27049  basellem5  27051  basellem8  27054  mumul  27147  fsumdvdscom  27151  muinv  27159  chtublem  27178  perfect  27198  pcbcctr  27243  bclbnd  27247  bposlem1  27251  bposlem6  27256  lgssq2  27305  gausslemma2dlem1a  27332  gausslemma2dlem3  27335  2lgslem1a1  27356  2sqlem6  27390  2sqlem10  27395  2sqnn  27406  2sqreunnltlem  27417  rplogsumlem1  27451  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumiflem1  27468  dchrvmaeq0  27471  dchrisum0re  27480  logdivbnd  27523  cusgrsize2inds  29527  wlkdlem2  29755  crctcshwlkn0lem1  29883  crctcshwlkn0lem6  29888  0enwwlksnge1  29937  wspthsnonn0vne  29990  clwwlknwwlksn  30113  clwwlkinwwlk  30115  clwwlkel  30121  clwwlkf  30122  clwwlkf1  30124  wwlksubclwwlk  30133  eucrctshift  30318  eucrct2eupth  30320  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  ipasslem4  30909  ipasslem5  30910  isarchi3  33269  oddpwdc  34511  eulerpartlemb  34525  fibp1  34558  subfacp1lem6  35379  subfaclim  35382  snmlff  35523  circum  35868  divcnvlin  35927  bcprod  35932  iprodgam  35936  faclim  35940  faclim2  35942  nn0prpwlem  36516  nndivsub  36651  knoppndvlem13  36724  poimirlem13  37830  poimirlem14  37831  poimirlem29  37846  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  mblfinlem2  37855  ovoliunnfl  37859  voliunnfl  37861  facp2  42393  nnadd1com  42518  nnaddcom  42519  dvdsexpnn0  42585  renegmulnnass  42716  fimgmcyc  42785  dffltz  42873  irrapxlem1  43060  pellexlem1  43067  pellqrex  43117  2nn0ind  43183  jm2.17c  43200  acongrep  43218  jm2.18  43226  jm2.20nn  43235  jm2.16nn0  43242  proot1ex  43434  hashnzfzclim  44559  binomcxplemnotnn0  44593  nnsplit  45599  clim1fr1  45843  sumnnodd  45872  wallispilem4  46308  wallispilem5  46309  wallispi  46310  wallispi2lem1  46311  wallispi2lem2  46312  wallispi2  46313  stirlinglem1  46314  stirlinglem3  46316  stirlinglem4  46317  stirlinglem5  46318  stirlinglem6  46319  stirlinglem7  46320  stirlinglem8  46321  stirlinglem10  46323  stirlinglem11  46324  stirlinglem12  46325  stirlinglem13  46326  stirlinglem14  46327  stirlinglem15  46328  dirkerper  46336  dirkertrigeqlem1  46338  fouriersw  46471  nnfoctbdjlem  46695  deccarry  47553  subsubelfzo0  47568  submodlt  47592  mod0mul  47598  m1modmmod  47600  modlt0b  47605  sqrtpwpw2p  47780  fmtnodvds  47786  fmtnoprmfac1  47807  fmtnoprmfac2lem1  47808  fmtnoprmfac2  47809  lighneallem2  47848  lighneallem3  47849  lighneallem4  47852  nnennexALTV  47943  perfectALTV  47965  fppr2odd  47973  fpprwppr  47981  fpprwpprb  47982  tgoldbachlt  48058  gpgedgvtx0  48303  gpg3kgrtriexlem2  48326  gpg3kgrtriexlem5  48329  gpg3kgrtriex  48331  nnsgrp  48419  nnsgrpnmnd  48420  bcpascm1  48593  altgsumbcALT  48595  eluz2cnn0n1  48753  pw2m1lepw2m1  48762  nnennex  48767  logbpw2m1  48809  blenpw2m1  48821  nnpw2blen  48822  nnpw2pmod  48825  blennnt2  48831  blennn0em1  48833  nn0digval  48842  dignn0fr  48843  dignn0ldlem  48844  dig0  48848  nn0sumshdiglemA  48861  nn0sumshdiglemB  48862  nn0sumshdiglem1  48863