Theorem nncn 12130

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℂcc 11001  ℕcn 12122

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668  ax-1cn 11061  ax-addcl 11063

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12123

This theorem is referenced by:  nncni  12132  nn1m1nn  12143  nn1suc  12144  nnaddcl  12145  nnmulcl  12146  nnmtmip  12148  nnneneg  12157  nnsub  12166  nndiv  12168  nndivtr  12169  nnnn0addcl  12408  nn0nnaddcl  12409  elnnnn0  12421  nn0sub  12428  nnnegz  12468  elz2  12483  zaddcl  12509  nnaddm1cl  12527  zdiv  12540  zdivadd  12541  zdivmul  12542  nneo  12554  peano5uzi  12559  elq  12845  qmulz  12846  qaddcl  12860  qnegcl  12861  qmulcl  12862  qreccl  12864  rpnnen1lem5  12876  nnledivrp  13001  nn0ledivnn  13002  fseq1m1p1  13496  ubmelm1fzo  13660  subfzo0  13689  quoremz  13756  quoremnn0ALT  13758  intfracq  13760  fldiv  13761  fldiv2  13762  modmulnn  13790  addmodid  13823  addmodidr  13824  modaddmodup  13838  modfzo0difsn  13847  modsumfzodifsn  13848  addmodlteq  13850  nn0ennn  13883  ser1const  13962  expneg  13973  expm1t  13994  nnsqcl  14032  nnlesq  14109  digit2  14140  digit1  14141  expnngt1  14145  facdiv  14191  facndiv  14192  faclbnd  14194  faclbnd4lem1  14197  faclbnd4lem4  14200  bcn1  14217  bcm1k  14219  bcp1n  14220  bcval5  14222  bcn2m1  14228  cshwidxmod  14707  cshwidxm  14712  cshwidxn  14713  repswcshw  14716  isercoll2  15573  divcnv  15757  harmonic  15763  arisum  15764  arisum2  15765  expcnv  15768  pwdif  15772  geomulcvg  15780  mertenslem2  15789  ef0lem  15982  efexp  16007  ruclem12  16147  sqrt2irr  16155  nndivides  16170  modmulconst  16196  dvdsflip  16225  nn0enne  16285  nno  16290  pwp1fsum  16299  divalgmod  16314  ndvdsadd  16318  modgcd  16440  gcdmultiplez  16443  gcddiv  16459  rpmulgcd  16465  rplpwr  16466  sqgcd  16470  expgcd  16471  nn0expgcd  16472  lcmgcdlem  16514  qredeq  16565  qredeu  16566  cncongrcoprm  16578  prmind2  16593  isprm6  16622  divnumden  16656  divdenle  16657  nn0gcdsq  16660  hashgcdlem  16696  pythagtriplem1  16725  pythagtriplem2  16726  pythagtriplem6  16730  pythagtriplem7  16731  pythagtriplem12  16735  pythagtriplem14  16737  pythagtriplem15  16738  pythagtriplem16  16739  pythagtriplem17  16740  pythagtriplem19  16742  pcqcl  16765  pcexp  16768  pcneg  16783  fldivp1  16806  oddprmdvds  16812  prmpwdvds  16813  infpnlem2  16820  prmreclem1  16825  prmreclem6  16830  4sqlem19  16872  vdwapun  16883  vdwapid1  16884  prmonn2  16948  prmgaplem7  16966  mulgnegnn  18994  mulgnnass  19019  mulgmodid  19023  odmod  19456  cnfldmulg  21338  prmirredlem  21407  znidomb  21496  znrrg  21500  cply1mul  22209  chfacfscmul0  22771  chfacfscmulfsupp  22772  chfacfscmulgsum  22773  chfacfpmmul0  22775  chfacfpmmulfsupp  22776  chfacfpmmulgsum  22777  cayhamlem1  22779  cpmadugsumlemF  22789  ovolunlem1  25423  uniioombllem3  25511  vitali  25539  mbfi1fseqlem3  25643  dvexp  25882  dvexp3  25907  plyeq0lem  26140  dgrcolem1  26204  aaliou3lem2  26276  aaliou3lem7  26282  pserdv2  26365  abelthlem6  26371  logtayl  26594  logtaylsum  26595  logtayl2  26596  cxpexp  26602  cxproot  26624  root1id  26689  root1eq1  26690  cxpeq  26692  logbgcd1irr  26729  atantayl  26872  atantayl2  26873  birthdaylem2  26887  dfef2  26906  emcllem2  26932  emcllem3  26933  zetacvg  26950  lgam1  26999  gamfac  27002  basellem2  27017  basellem3  27018  basellem5  27020  basellem8  27023  mumul  27116  fsumdvdscom  27120  muinv  27128  chtublem  27147  perfect  27167  pcbcctr  27212  bclbnd  27216  bposlem1  27220  bposlem6  27225  lgssq2  27274  gausslemma2dlem1a  27301  gausslemma2dlem3  27304  2lgslem1a1  27325  2sqlem6  27359  2sqlem10  27364  2sqnn  27375  2sqreunnltlem  27386  rplogsumlem1  27420  dchrmusumlema  27429  dchrmusum2  27430  dchrvmasumiflem1  27437  dchrvmaeq0  27440  dchrisum0re  27449  logdivbnd  27492  cusgrsize2inds  29430  wlkdlem2  29658  crctcshwlkn0lem1  29786  crctcshwlkn0lem6  29791  0enwwlksnge1  29840  wspthsnonn0vne  29893  clwwlknwwlksn  30013  clwwlkinwwlk  30015  clwwlkel  30021  clwwlkf  30022  clwwlkf1  30024  wwlksubclwwlk  30033  eucrctshift  30218  eucrct2eupth  30220  numclwwlk2lem1  30351  numclwlk2lem2f  30352  numclwlk2lem2f1o  30354  ipasslem4  30809  ipasslem5  30810  isarchi3  33151  oddpwdc  34362  eulerpartlemb  34376  fibp1  34409  subfacp1lem6  35217  subfaclim  35220  snmlff  35361  circum  35706  divcnvlin  35765  bcprod  35770  iprodgam  35774  faclim  35778  faclim2  35780  nn0prpwlem  36355  nndivsub  36490  knoppndvlem13  36557  poimirlem13  37672  poimirlem14  37673  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  mblfinlem2  37697  ovoliunnfl  37701  voliunnfl  37703  facp2  42175  nnadd1com  42299  nnaddcom  42300  dvdsexpnn0  42366  renegmulnnass  42497  fimgmcyc  42566  dffltz  42666  irrapxlem1  42854  pellexlem1  42861  pellqrex  42911  2nn0ind  42977  jm2.17c  42994  acongrep  43012  jm2.18  43020  jm2.20nn  43029  jm2.16nn0  43036  proot1ex  43228  hashnzfzclim  44354  binomcxplemnotnn0  44388  nnsplit  45396  clim1fr1  45640  sumnnodd  45669  wallispilem4  46105  wallispilem5  46106  wallispi  46107  wallispi2lem1  46108  wallispi2lem2  46109  wallispi2  46110  stirlinglem1  46111  stirlinglem3  46113  stirlinglem4  46114  stirlinglem5  46115  stirlinglem6  46116  stirlinglem7  46117  stirlinglem8  46118  stirlinglem10  46120  stirlinglem11  46121  stirlinglem12  46122  stirlinglem13  46123  stirlinglem14  46124  stirlinglem15  46125  dirkerper  46133  dirkertrigeqlem1  46135  fouriersw  46268  nnfoctbdjlem  46492  deccarry  47341  subsubelfzo0  47356  submodlt  47380  mod0mul  47386  m1modmmod  47388  modlt0b  47393  sqrtpwpw2p  47568  fmtnodvds  47574  fmtnoprmfac1  47595  fmtnoprmfac2lem1  47596  fmtnoprmfac2  47597  lighneallem2  47636  lighneallem3  47637  lighneallem4  47640  nnennexALTV  47731  perfectALTV  47753  fppr2odd  47761  fpprwppr  47769  fpprwpprb  47770  tgoldbachlt  47846  gpgedgvtx0  48091  gpg3kgrtriexlem2  48114  gpg3kgrtriexlem5  48117  gpg3kgrtriex  48119  nnsgrp  48207  nnsgrpnmnd  48208  bcpascm1  48381  altgsumbcALT  48383  eluz2cnn0n1  48542  pw2m1lepw2m1  48551  nnennex  48556  logbpw2m1  48598  blenpw2m1  48610  nnpw2blen  48611  nnpw2pmod  48614  blennnt2  48620  blennn0em1  48622  nn0digval  48631  dignn0fr  48632  dignn0ldlem  48633  dig0  48637  nn0sumshdiglemA  48650  nn0sumshdiglemB  48651  nn0sumshdiglem1  48652