Theorem nncn 12242

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℂcc 11099  ℕcn 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406  ax-un 7734  ax-1cn 11159  ax-addcl 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-nn 12235

This theorem is referenced by:  nncni  12244  nn1m1nn  12255  nn1suc  12256  nnaddcl  12257  nnmulcl  12258  nnadd1com  12260  nnaddcom  12261  nnmtmip  12263  nnneneg  12272  nnsub  12281  nndiv  12283  nndivtr  12284  nnnn0addcl  12535  nn0nnaddcl  12536  elnnnn0  12548  nn0sub  12555  nnnegz  12595  elz2  12610  zaddcl  12635  nnaddm1cl  12654  zdiv  12667  zdivadd  12668  zdivmul  12669  nneo  12681  peano5uzi  12686  elq  12975  qmulz  12976  qaddcl  12990  qnegcl  12991  qmulcl  12992  qreccl  12994  rpnnen1lem5  13006  nnledivrp  13131  nn0ledivnn  13132  fseq1m1p1  13629  ubmelm1fzo  13794  subfzo0  13823  quoremz  13890  quoremnn0ALT  13892  intfracq  13894  fldiv  13895  fldiv2  13896  modmulnn  13924  addmodid  13957  addmodidr  13958  modaddmodup  13972  modfzo0difsn  13981  modsumfzodifsn  13982  addmodlteq  13984  nn0ennn  14017  ser1const  14096  expneg  14107  expm1t  14128  nnsqcl  14166  nnlesq  14243  digit2  14274  digit1  14275  expnngt1  14279  facdiv  14325  facndiv  14326  faclbnd  14328  faclbnd4lem1  14331  faclbnd4lem4  14334  bcn1  14351  bcm1k  14353  bcp1n  14354  bcval5  14356  bcn2m1  14362  cshwidxmod  14842  cshwidxm  14847  cshwidxn  14848  repswcshw  14851  isercoll2  15722  divcnv  15909  harmonic  15915  arisum  15916  arisum2  15917  expcnv  15920  pwdif  15924  geomulcvg  15932  mertenslem2  15941  ef0lem  16133  efexp  16158  ruclem12  16298  sqrt2irr  16306  nndivides  16321  modmulconst  16347  dvdsflip  16376  nn0enne  16436  nno  16441  pwp1fsum  16450  divalgmod  16465  ndvdsadd  16469  modgcd  16591  gcdmultiplez  16594  gcddiv  16610  rpmulgcd  16616  rplpwr  16617  sqgcd  16621  expgcd  16622  nn0expgcd  16623  lcmgcdlem  16665  qredeq  16716  qredeu  16717  cncongrcoprm  16729  prmind2  16744  isprm6  16774  divnumden  16808  divdenle  16809  nn0gcdsq  16812  hashgcdlem  16848  pythagtriplem1  16877  pythagtriplem2  16878  pythagtriplem6  16882  pythagtriplem7  16883  pythagtriplem12  16887  pythagtriplem14  16889  pythagtriplem15  16890  pythagtriplem16  16891  pythagtriplem17  16892  pythagtriplem19  16894  pcqcl  16917  pcexp  16920  pcneg  16935  fldivp1  16958  oddprmdvds  16964  prmpwdvds  16965  infpnlem2  16972  prmreclem1  16977  prmreclem6  16982  4sqlem19  17024  vdwapun  17035  vdwapid1  17036  prmonn2  17100  prmgaplem7  17118  mulgnegnn  19151  mulgnnass  19176  mulgmodid  19180  odmod  19617  cnfldmulg  21535  prmirredlem  21603  znidomb  21692  znrrg  21696  cply1mul  22437  chfacfscmul0  22996  chfacfscmulfsupp  22997  chfacfscmulgsum  22998  chfacfpmmul0  23000  chfacfpmmulfsupp  23001  chfacfpmmulgsum  23002  cayhamlem1  23004  cpmadugsumlemF  23014  ovolunlem1  25637  uniioombllem3  25725  vitali  25753  mbfi1fseqlem3  25857  dvexp  26093  dvexp3  26118  plyeq0lem  26348  dgrcolem1  26411  aaliou3lem2  26487  aaliou3lem7  26493  pserdv2  26574  abelthlem6  26580  logtayl  26806  logtaylsum  26807  logtayl2  26808  cxpexp  26814  cxproot  26836  root1id  26900  root1eq1  26901  cxpeq  26903  logbgcd1irr  26940  atantayl  27083  atantayl2  27084  birthdaylem2  27098  dfef2  27116  emcllem2  27142  emcllem3  27143  zetacvg  27160  lgam1  27209  gamfac  27212  basellem2  27227  basellem3  27228  basellem5  27230  basellem8  27233  mumul  27326  fsumdvdscom  27330  muinv  27338  chtublem  27356  perfect  27376  pcbcctr  27421  bclbnd  27425  bposlem1  27429  bposlem6  27434  lgssq2  27483  gausslemma2dlem1a  27510  gausslemma2dlem3  27513  2lgslem1a1  27534  2sqlem6  27568  2sqlem10  27573  2sqnn  27584  2sqreunnltlem  27595  rplogsumlem1  27629  dchrmusumlema  27638  dchrmusum2  27639  dchrvmasumiflem1  27646  dchrvmaeq0  27649  dchrisum0re  27658  logdivbnd  27701  cusgrsize2inds  29784  wlkdlem2  30012  crctcshwlkn0lem1  30140  crctcshwlkn0lem6  30145  0enwwlksnge1  30194  wspthsnonn0vne  30247  clwwlknwwlksn  30370  clwwlkinwwlk  30372  clwwlkel  30378  clwwlkf  30379  clwwlkf1  30381  wwlksubclwwlk  30390  eucrctshift  30575  eucrct2eupth  30577  numclwwlk2lem1  30708  numclwlk2lem2f  30709  numclwlk2lem2f1o  30711  ipasslem4  31167  ipasslem5  31168  isarchi3  33488  oddpwdc  34725  eulerpartlemb  34739  fibp1  34772  subfacp1lem6  35658  subfaclim  35661  snmlff  35802  circum  36147  divcnvlin  36206  bcprod  36211  iprodgam  36215  faclim  36219  faclim2  36221  nn0prpwlem  36814  nndivsub  36949  knoppndvlem13  37094  poimirlem13  38265  poimirlem14  38266  poimirlem29  38281  poimirlem30  38282  poimirlem31  38283  poimirlem32  38284  mblfinlem2  38290  ovoliunnfl  38294  voliunnfl  38296  facp2  42891  dvdsexpnn0  43076  renegmulnnass  43220  fimgmcyc  43285  dffltz  43349  irrapxlem1  43532  pellexlem1  43539  pellqrex  43589  2nn0ind  43655  jm2.17c  43672  acongrep  43690  jm2.18  43698  jm2.20nn  43707  jm2.16nn0  43714  proot1ex  43906  hashnzfzclim  45015  binomcxplemnotnn0  45049  nnsplit  46057  clim1fr1  46300  sumnnodd  46329  wallispilem4  46765  wallispilem5  46766  wallispi  46767  wallispi2lem1  46768  wallispi2lem2  46769  wallispi2  46770  stirlinglem1  46771  stirlinglem3  46773  stirlinglem4  46774  stirlinglem5  46775  stirlinglem6  46776  stirlinglem7  46777  stirlinglem8  46778  stirlinglem10  46780  stirlinglem11  46781  stirlinglem12  46782  stirlinglem13  46783  stirlinglem14  46784  stirlinglem15  46785  dirkerper  46793  dirkertrigeqlem1  46795  fouriersw  46928  nnfoctbdjlem  47152  sqrtnnaa  47587  deccarry  48031  subsubelfzo0  48047  submodlt  48076  mod0mul  48082  m1modmmod  48084  modlt0b  48089  sqrtpwpw2p  48273  fmtnodvds  48279  fmtnoprmfac1  48300  fmtnoprmfac2lem1  48301  fmtnoprmfac2  48302  lighneallem2  48341  lighneallem3  48342  lighneallem4  48345  nnennexALTV  48449  perfectALTV  48471  fppr2odd  48479  fpprwppr  48487  fpprwpprb  48488  tgoldbachlt  48564  gpgedgvtx0  48809  gpg3kgrtriexlem2  48832  gpg3kgrtriexlem5  48835  gpg3kgrtriex  48837  nnsgrp  48925  nnsgrpnmnd  48926  bcpascm1  49114  altgsumbcALT  49116  eluz2cnn0n1  49274  pw2m1lepw2m1  49283  nnennex  49288  logbpw2m1  49330  blenpw2m1  49342  nnpw2blen  49343  nnpw2pmod  49346  blennnt2  49352  blennn0em1  49354  nn0digval  49363  dignn0fr  49364  dignn0ldlem  49365  dig0  49369  nn0sumshdiglemA  49382  nn0sumshdiglemB  49383  nn0sumshdiglem1  49384