Theorem nncn 12232

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℂcc 11086  ℕcn 12224

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722  ax-1cn 11146  ax-addcl 11148

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-nn 12225

This theorem is referenced by:  nncni  12234  nn1m1nn  12245  nn1suc  12246  nnaddcl  12247  nnmulcl  12248  nnadd1com  12250  nnaddcom  12251  nnmtmip  12253  nnneneg  12262  nnsub  12271  nndiv  12273  nndivtr  12274  nnnn0addcl  12525  nn0nnaddcl  12526  elnnnn0  12538  nn0sub  12545  nnnegz  12585  elz2  12600  zaddcl  12625  nnaddm1cl  12644  zdiv  12657  zdivadd  12658  zdivmul  12659  nneo  12671  peano5uzi  12676  elq  12965  qmulz  12966  qaddcl  12980  qnegcl  12981  qmulcl  12982  qreccl  12984  rpnnen1lem5  12996  nnledivrp  13121  nn0ledivnn  13122  fseq1m1p1  13618  ubmelm1fzo  13783  subfzo0  13812  quoremz  13879  quoremnn0ALT  13881  intfracq  13883  fldiv  13884  fldiv2  13885  modmulnn  13913  addmodid  13946  addmodidr  13947  modaddmodup  13961  modfzo0difsn  13970  modsumfzodifsn  13971  addmodlteq  13973  nn0ennn  14006  ser1const  14085  expneg  14096  expm1t  14117  nnsqcl  14155  nnlesq  14232  digit2  14263  digit1  14264  expnngt1  14268  facdiv  14314  facndiv  14315  faclbnd  14317  faclbnd4lem1  14320  faclbnd4lem4  14323  bcn1  14340  bcm1k  14342  bcp1n  14343  bcval5  14345  bcn2m1  14351  cshwidxmod  14830  cshwidxm  14835  cshwidxn  14836  repswcshw  14839  isercoll2  15710  divcnv  15897  harmonic  15903  arisum  15904  arisum2  15905  expcnv  15908  pwdif  15912  geomulcvg  15920  mertenslem2  15929  ef0lem  16122  efexp  16147  ruclem12  16287  sqrt2irr  16295  nndivides  16310  modmulconst  16336  dvdsflip  16365  nn0enne  16425  nno  16430  pwp1fsum  16439  divalgmod  16454  ndvdsadd  16458  modgcd  16580  gcdmultiplez  16583  gcddiv  16599  rpmulgcd  16605  rplpwr  16606  sqgcd  16610  expgcd  16611  nn0expgcd  16612  lcmgcdlem  16654  qredeq  16705  qredeu  16706  cncongrcoprm  16718  prmind2  16733  isprm6  16763  divnumden  16797  divdenle  16798  nn0gcdsq  16801  hashgcdlem  16837  pythagtriplem1  16866  pythagtriplem2  16867  pythagtriplem6  16871  pythagtriplem7  16872  pythagtriplem12  16876  pythagtriplem14  16878  pythagtriplem15  16879  pythagtriplem16  16880  pythagtriplem17  16881  pythagtriplem19  16883  pcqcl  16906  pcexp  16909  pcneg  16924  fldivp1  16947  oddprmdvds  16953  prmpwdvds  16954  infpnlem2  16961  prmreclem1  16966  prmreclem6  16971  4sqlem19  17013  vdwapun  17024  vdwapid1  17025  prmonn2  17089  prmgaplem7  17107  mulgnegnn  19141  mulgnnass  19166  mulgmodid  19170  odmod  19607  cnfldmulg  21514  prmirredlem  21582  znidomb  21671  znrrg  21675  cply1mul  22417  chfacfscmul0  22976  chfacfscmulfsupp  22977  chfacfscmulgsum  22978  chfacfpmmul0  22980  chfacfpmmulfsupp  22981  chfacfpmmulgsum  22982  cayhamlem1  22984  cpmadugsumlemF  22994  ovolunlem1  25617  uniioombllem3  25705  vitali  25733  mbfi1fseqlem3  25837  dvexp  26073  dvexp3  26098  plyeq0lem  26328  dgrcolem1  26391  aaliou3lem2  26465  aaliou3lem7  26471  pserdv2  26551  abelthlem6  26557  logtayl  26783  logtaylsum  26784  logtayl2  26785  cxpexp  26791  cxproot  26813  root1id  26877  root1eq1  26878  cxpeq  26880  logbgcd1irr  26917  atantayl  27060  atantayl2  27061  birthdaylem2  27075  dfef2  27093  emcllem2  27119  emcllem3  27120  zetacvg  27137  lgam1  27186  gamfac  27189  basellem2  27204  basellem3  27205  basellem5  27207  basellem8  27210  mumul  27303  fsumdvdscom  27307  muinv  27315  chtublem  27333  perfect  27353  pcbcctr  27398  bclbnd  27402  bposlem1  27406  bposlem6  27411  lgssq2  27460  gausslemma2dlem1a  27487  gausslemma2dlem3  27490  2lgslem1a1  27511  2sqlem6  27545  2sqlem10  27550  2sqnn  27561  2sqreunnltlem  27572  rplogsumlem1  27606  dchrmusumlema  27615  dchrmusum2  27616  dchrvmasumiflem1  27623  dchrvmaeq0  27626  dchrisum0re  27635  logdivbnd  27678  cusgrsize2inds  29712  wlkdlem2  29940  crctcshwlkn0lem1  30068  crctcshwlkn0lem6  30073  0enwwlksnge1  30122  wspthsnonn0vne  30175  clwwlknwwlksn  30298  clwwlkinwwlk  30300  clwwlkel  30306  clwwlkf  30307  clwwlkf1  30309  wwlksubclwwlk  30318  eucrctshift  30503  eucrct2eupth  30505  numclwwlk2lem1  30636  numclwlk2lem2f  30637  numclwlk2lem2f1o  30639  ipasslem4  31095  ipasslem5  31096  isarchi3  33420  oddpwdc  34661  eulerpartlemb  34675  fibp1  34708  subfacp1lem6  35548  subfaclim  35551  snmlff  35692  circum  36037  divcnvlin  36096  bcprod  36101  iprodgam  36105  faclim  36109  faclim2  36111  nn0prpwlem  36695  nndivsub  36830  knoppndvlem13  36975  poimirlem13  38144  poimirlem14  38145  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  mblfinlem2  38169  ovoliunnfl  38173  voliunnfl  38175  facp2  42772  dvdsexpnn0  42955  renegmulnnass  43099  fimgmcyc  43164  dffltz  43228  irrapxlem1  43411  pellexlem1  43418  pellqrex  43468  2nn0ind  43534  jm2.17c  43551  acongrep  43569  jm2.18  43577  jm2.20nn  43586  jm2.16nn0  43593  proot1ex  43785  hashnzfzclim  44896  binomcxplemnotnn0  44930  nnsplit  45932  clim1fr1  46175  sumnnodd  46204  wallispilem4  46640  wallispilem5  46641  wallispi  46642  wallispi2lem1  46643  wallispi2lem2  46644  wallispi2  46645  stirlinglem1  46646  stirlinglem3  46648  stirlinglem4  46649  stirlinglem5  46650  stirlinglem6  46651  stirlinglem7  46652  stirlinglem8  46653  stirlinglem10  46655  stirlinglem11  46656  stirlinglem12  46657  stirlinglem13  46658  stirlinglem14  46659  stirlinglem15  46660  dirkerper  46668  dirkertrigeqlem1  46670  fouriersw  46803  nnfoctbdjlem  47027  deccarry  47903  subsubelfzo0  47919  submodlt  47948  mod0mul  47954  m1modmmod  47956  modlt0b  47961  sqrtpwpw2p  48145  fmtnodvds  48151  fmtnoprmfac1  48172  fmtnoprmfac2lem1  48173  fmtnoprmfac2  48174  lighneallem2  48213  lighneallem3  48214  lighneallem4  48217  nnennexALTV  48321  perfectALTV  48343  fppr2odd  48351  fpprwppr  48359  fpprwpprb  48360  tgoldbachlt  48436  gpgedgvtx0  48681  gpg3kgrtriexlem2  48704  gpg3kgrtriexlem5  48707  gpg3kgrtriex  48709  nnsgrp  48797  nnsgrpnmnd  48798  bcpascm1  48982  altgsumbcALT  48984  eluz2cnn0n1  49142  pw2m1lepw2m1  49151  nnennex  49156  logbpw2m1  49198  blenpw2m1  49210  nnpw2blen  49211  nnpw2pmod  49214  blennnt2  49220  blennn0em1  49222  nn0digval  49231  dignn0fr  49232  dignn0ldlem  49233  dig0  49237  nn0sumshdiglemA  49250  nn0sumshdiglemB  49251  nn0sumshdiglem1  49252