Theorem nncn 12220

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 12217	. 2 ⊢ ℕ ⊆ ℂ
2	1	sseli 3979	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:  nncni  12222  nn1m1nn  12233  nn1suc  12234  nnaddcl  12235  nnmulcl  12236  nnmtmip  12238  nnneneg  12247  nnsub  12256  nndiv  12258  nndivtr  12259  nnnn0addcl  12502  nn0nnaddcl  12503  elnnnn0  12515  nn0sub  12522  nnnegz  12561  elz2  12576  zaddcl  12602  nnaddm1cl  12619  zdiv  12632  zdivadd  12633  zdivmul  12634  nneo  12646  peano5uzi  12651  elq  12934  qmulz  12935  qaddcl  12949  qnegcl  12950  qmulcl  12951  qreccl  12953  rpnnen1lem5  12965  nnledivrp  13086  nn0ledivnn  13087  fseq1m1p1  13576  ubmelm1fzo  13728  subfzo0  13754  quoremz  13820  quoremnn0ALT  13822  intfracq  13824  fldiv  13825  fldiv2  13826  modmulnn  13854  addmodid  13884  addmodidr  13885  modaddmodup  13899  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  nn0ennn  13944  ser1const  14024  expneg  14035  expm1t  14056  nnsqcl  14093  nnlesq  14169  digit2  14199  digit1  14200  expnngt1  14204  facdiv  14247  facndiv  14248  faclbnd  14250  faclbnd4lem1  14253  faclbnd4lem4  14256  bcn1  14273  bcm1k  14275  bcp1n  14276  bcval5  14278  bcn2m1  14284  cshwidxmod  14753  cshwidxm  14758  cshwidxn  14759  repswcshw  14762  isercoll2  15615  divcnv  15799  harmonic  15805  arisum  15806  arisum2  15807  expcnv  15810  pwdif  15814  geomulcvg  15822  mertenslem2  15831  ef0lem  16022  efexp  16044  ruclem12  16184  sqrt2irr  16192  nndivides  16207  modmulconst  16231  dvdsflip  16260  nn0enne  16320  nno  16325  pwp1fsum  16334  divalgmod  16349  ndvdsadd  16353  modgcd  16474  gcdmultiplez  16477  gcddiv  16493  rpmulgcd  16498  rplpwr  16499  sqgcd  16502  lcmgcdlem  16543  qredeq  16594  qredeu  16595  cncongrcoprm  16607  prmind2  16622  isprm6  16651  divnumden  16684  divdenle  16685  nn0gcdsq  16688  hashgcdlem  16721  pythagtriplem1  16749  pythagtriplem2  16750  pythagtriplem6  16754  pythagtriplem7  16755  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem15  16762  pythagtriplem16  16763  pythagtriplem17  16764  pythagtriplem19  16766  pcqcl  16789  pcexp  16792  pcneg  16807  fldivp1  16830  oddprmdvds  16836  prmpwdvds  16837  infpnlem2  16844  prmreclem1  16849  prmreclem6  16854  4sqlem19  16896  vdwapun  16907  vdwapid1  16908  prmonn2  16972  prmgaplem7  16990  mulgnegnn  18964  mulgnnass  18989  mulgmodid  18993  odmod  19414  cnfldmulg  20977  prmirredlem  21042  znidomb  21117  znrrg  21121  cply1mul  21818  chfacfscmul0  22360  chfacfscmulfsupp  22361  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulfsupp  22365  chfacfpmmulgsum  22366  cayhamlem1  22368  cpmadugsumlemF  22378  ovolunlem1  25014  uniioombllem3  25102  vitali  25130  mbfi1fseqlem3  25235  dvexp  25470  dvexp3  25495  plyeq0lem  25724  dgrcolem1  25787  aaliou3lem2  25856  aaliou3lem7  25862  pserdv2  25942  abelthlem6  25948  logtayl  26168  logtaylsum  26169  logtayl2  26170  cxpexp  26176  cxproot  26198  root1id  26262  root1eq1  26263  cxpeq  26265  logbgcd1irr  26299  atantayl  26442  atantayl2  26443  birthdaylem2  26457  dfef2  26475  emcllem2  26501  emcllem3  26502  zetacvg  26519  lgam1  26568  gamfac  26571  basellem2  26586  basellem3  26587  basellem5  26589  basellem8  26592  mumul  26685  fsumdvdscom  26689  muinv  26697  chtublem  26714  perfect  26734  pcbcctr  26779  bclbnd  26783  bposlem1  26787  bposlem6  26792  lgssq2  26841  gausslemma2dlem1a  26868  gausslemma2dlem3  26871  2lgslem1a1  26892  2sqlem6  26926  2sqlem10  26931  2sqnn  26942  2sqreunnltlem  26953  rplogsumlem1  26987  dchrmusumlema  26996  dchrmusum2  26997  dchrvmasumiflem1  27004  dchrvmaeq0  27007  dchrisum0re  27016  logdivbnd  27059  cusgrsize2inds  28710  wlkdlem2  28940  crctcshwlkn0lem1  29064  crctcshwlkn0lem6  29069  0enwwlksnge1  29118  wspthsnonn0vne  29171  clwwlknwwlksn  29291  clwwlkinwwlk  29293  clwwlkel  29299  clwwlkf  29300  clwwlkf1  29302  wwlksubclwwlk  29311  eucrctshift  29496  eucrct2eupth  29498  numclwwlk2lem1  29629  numclwlk2lem2f  29630  numclwlk2lem2f1o  29632  ipasslem4  30087  ipasslem5  30088  isarchi3  32333  oddpwdc  33353  eulerpartlemb  33367  fibp1  33400  subfacp1lem6  34176  subfaclim  34179  snmlff  34320  circum  34659  divcnvlin  34702  bcprod  34708  iprodgam  34712  faclim  34716  faclim2  34718  nn0prpwlem  35207  nndivsub  35342  knoppndvlem13  35400  poimirlem13  36501  poimirlem14  36502  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  mblfinlem2  36526  ovoliunnfl  36530  voliunnfl  36532  facp2  40959  metakunt16  41000  metakunt30  41014  fac2xp3  41020  nnadd1com  41181  nnaddcom  41182  expgcd  41225  nn0expgcd  41226  dvdsexpnn0  41232  renegmulnnass  41326  dffltz  41376  irrapxlem1  41560  pellexlem1  41567  pellqrex  41617  2nn0ind  41684  jm2.17c  41701  acongrep  41719  jm2.18  41727  jm2.20nn  41736  jm2.16nn0  41743  proot1ex  41943  hashnzfzclim  43081  binomcxplemnotnn0  43115  nnsplit  44068  clim1fr1  44317  sumnnodd  44346  wallispilem4  44784  wallispilem5  44785  wallispi  44786  wallispi2lem1  44787  wallispi2lem2  44788  wallispi2  44789  stirlinglem1  44790  stirlinglem3  44792  stirlinglem4  44793  stirlinglem5  44794  stirlinglem6  44795  stirlinglem7  44796  stirlinglem8  44797  stirlinglem10  44799  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  stirlinglem14  44803  stirlinglem15  44804  dirkerper  44812  dirkertrigeqlem1  44814  fouriersw  44947  nnfoctbdjlem  45171  deccarry  46019  subsubelfzo0  46034  sqrtpwpw2p  46206  fmtnodvds  46212  fmtnoprmfac1  46233  fmtnoprmfac2lem1  46234  fmtnoprmfac2  46235  lighneallem2  46274  lighneallem3  46275  lighneallem4  46278  nnennexALTV  46369  perfectALTV  46391  fppr2odd  46399  fpprwppr  46407  fpprwpprb  46408  tgoldbachlt  46484  nnsgrp  46587  nnsgrpnmnd  46588  bcpascm1  47027  altgsumbcALT  47029  eluz2cnn0n1  47192  pw2m1lepw2m1  47201  mod0mul  47205  m1modmmod  47207  nnennex  47211  logbpw2m1  47253  blenpw2m1  47265  nnpw2blen  47266  nnpw2pmod  47269  blennnt2  47275  blennn0em1  47277  nn0digval  47286  dignn0fr  47287  dignn0ldlem  47288  dig0  47292  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306  nn0sumshdiglem1  47307