Theorem nncn 12251

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℂcc 11108  ℕcn 12243

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-nul 5272  ax-pr 5407  ax-un 7738  ax-1cn 11168  ax-addcl 11170

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-iun 4961  df-br 5113  df-opab 5177  df-mpt 5196  df-tr 5222  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-nn 12244

This theorem is used by:  nncni  12253  nn1m1nn  12264  nn1suc  12265  nnaddcl  12266  nnmulcl  12267  nnadd1com  12269  nnaddcom  12270  nnmtmip  12272  nnneneg  12281  nnsub  12290  nndiv  12292  nndivtr  12293  nnnn0addcl  12544  nn0nnaddcl  12545  elnnnn0  12557  nn0sub  12564  nnnegz  12604  elz2  12619  zaddcl  12644  nnaddm1cl  12663  zdiv  12676  zdivadd  12677  zdivmul  12678  nneo  12690  peano5uzi  12695  elq  12984  qmulz  12985  qaddcl  12999  qnegcl  13000  qmulcl  13001  qreccl  13003  rpnnen1lem5  13015  nnledivrp  13140  nn0ledivnn  13141  fseq1m1p1  13638  ubmelm1fzo  13803  subfzo0  13832  quoremz  13899  quoremnn0ALT  13901  intfracq  13903  fldiv  13904  fldiv2  13905  modmulnn  13933  addmodid  13966  addmodidr  13967  modaddmodup  13981  modfzo0difsn  13990  modsumfzodifsn  13991  addmodlteq  13993  nn0ennn  14026  ser1const  14105  expneg  14116  expm1t  14137  nnsqcl  14175  nnlesq  14252  digit2  14283  digit1  14284  expnngt1  14288  facdiv  14334  facndiv  14335  faclbnd  14337  faclbnd4lem1  14340  faclbnd4lem4  14343  bcn1  14360  bcm1k  14362  bcp1n  14363  bcval5  14365  bcn2m1  14371  cshwidxmod  14851  cshwidxm  14856  cshwidxn  14857  repswcshw  14860  isercoll2  15731  divcnv  15918  harmonic  15924  arisum  15925  arisum2  15926  expcnv  15929  pwdif  15933  geomulcvg  15941  mertenslem2  15950  ef0lem  16142  efexp  16167  ruclem12  16307  sqrt2irr  16315  nndivides  16330  modmulconst  16356  dvdsflip  16385  nn0enne  16445  nno  16450  pwp1fsum  16459  divalgmod  16474  ndvdsadd  16478  modgcd  16600  gcdmultiplez  16603  gcddiv  16619  rpmulgcd  16625  rplpwr  16626  sqgcd  16630  expgcd  16631  nn0expgcd  16632  lcmgcdlem  16674  qredeq  16725  qredeu  16726  cncongrcoprm  16738  prmind2  16753  isprm6  16783  divnumden  16817  divdenle  16818  nn0gcdsq  16821  hashgcdlem  16857  pythagtriplem1  16886  pythagtriplem2  16887  pythagtriplem6  16891  pythagtriplem7  16892  pythagtriplem12  16896  pythagtriplem14  16898  pythagtriplem15  16899  pythagtriplem16  16900  pythagtriplem17  16901  pythagtriplem19  16903  pcqcl  16926  pcexp  16929  pcneg  16944  fldivp1  16967  oddprmdvds  16973  prmpwdvds  16974  infpnlem2  16981  prmreclem1  16986  prmreclem6  16991  4sqlem19  17033  vdwapun  17044  vdwapid1  17045  prmonn2  17109  prmgaplem7  17127  mulgnegnn  19160  mulgnnass  19185  mulgmodid  19189  odmod  19626  cnfldmulg  21569  prmirredlem  21637  znidomb  21726  znrrg  21730  cply1mul  22471  chfacfscmul0  23030  chfacfscmulfsupp  23031  chfacfscmulgsum  23032  chfacfpmmul0  23034  chfacfpmmulfsupp  23035  chfacfpmmulgsum  23036  cayhamlem1  23038  cpmadugsumlemF  23048  ovolunlem1  25671  uniioombllem3  25759  vitali  25787  mbfi1fseqlem3  25891  dvexp  26127  dvexp3  26152  plyeq0lem  26382  dgrcolem1  26445  aaliou3lem2  26521  aaliou3lem7  26527  pserdv2  26608  abelthlem6  26614  logtayl  26840  logtaylsum  26841  logtayl2  26842  cxpexp  26848  cxproot  26870  root1id  26934  root1eq1  26935  cxpeq  26937  logbgcd1irr  26974  atantayl  27117  atantayl2  27118  birthdaylem2  27132  dfef2  27150  emcllem2  27176  emcllem3  27177  zetacvg  27194  lgam1  27243  gamfac  27246  basellem2  27261  basellem3  27262  basellem5  27264  basellem8  27267  mumul  27360  fsumdvdscom  27364  muinv  27372  chtublem  27390  perfect  27410  pcbcctr  27455  bclbnd  27459  bposlem1  27463  bposlem6  27468  lgssq2  27517  gausslemma2dlem1a  27544  gausslemma2dlem3  27547  2lgslem1a1  27568  2sqlem6  27602  2sqlem10  27607  2sqnn  27618  2sqreunnltlem  27629  rplogsumlem1  27663  dchrmusumlema  27672  dchrmusum2  27673  dchrvmasumiflem1  27680  dchrvmaeq0  27683  dchrisum0re  27692  logdivbnd  27735  cusgrsize2inds  29818  wlkdlem2  30046  crctcshwlkn0lem1  30174  crctcshwlkn0lem6  30179  0enwwlksnge1  30228  wspthsnonn0vne  30281  clwwlknwwlksn  30404  clwwlkinwwlk  30406  clwwlkel  30412  clwwlkf  30413  clwwlkf1  30415  wwlksubclwwlk  30424  eucrctshift  30609  eucrct2eupth  30611  numclwwlk2lem1  30742  numclwlk2lem2f  30743  numclwlk2lem2f1o  30745  ipasslem4  31201  ipasslem5  31202  isarchi3  33520  oddpwdc  34757  eulerpartlemb  34771  fibp1  34804  subfacp1lem6  35689  subfaclim  35692  snmlff  35833  circum  36178  divcnvlin  36237  bcprod  36242  iprodgam  36246  faclim  36250  faclim2  36252  nn0prpwlem  36865  nndivsub  37000  knoppndvlem13  37145  poimirlem13  38316  poimirlem14  38317  poimirlem29  38332  poimirlem30  38333  poimirlem31  38334  poimirlem32  38335  mblfinlem2  38341  ovoliunnfl  38345  voliunnfl  38347  facp2  42942  dvdsexpnn0  43127  renegmulnnass  43271  fimgmcyc  43334  dffltz  43398  irrapxlem1  43581  pellexlem1  43588  pellqrex  43638  2nn0ind  43704  jm2.17c  43721  acongrep  43739  jm2.18  43747  jm2.20nn  43756  jm2.16nn0  43763  proot1ex  43955  hashnzfzclim  45064  binomcxplemnotnn0  45098  nnsplit  46106  clim1fr1  46349  sumnnodd  46378  wallispilem4  46814  wallispilem5  46815  wallispi  46816  wallispi2lem1  46817  wallispi2lem2  46818  wallispi2  46819  stirlinglem1  46820  stirlinglem3  46822  stirlinglem4  46823  stirlinglem5  46824  stirlinglem6  46825  stirlinglem7  46826  stirlinglem8  46827  stirlinglem10  46829  stirlinglem11  46830  stirlinglem12  46831  stirlinglem13  46832  stirlinglem14  46833  stirlinglem15  46834  dirkerper  46842  dirkertrigeqlem1  46844  fouriersw  46977  nnfoctbdjlem  47201  sqrtnnaa  47636  deccarry  48080  subsubelfzo0  48096  submodlt  48125  mod0mul  48131  m1modmmod  48133  modlt0b  48138  sqrtpwpw2p  48322  fmtnodvds  48328  fmtnoprmfac1  48349  fmtnoprmfac2lem1  48350  fmtnoprmfac2  48351  lighneallem2  48390  lighneallem3  48391  lighneallem4  48394  nnennexALTV  48498  perfectALTV  48520  fppr2odd  48528  fpprwppr  48536  fpprwpprb  48537  tgoldbachlt  48613  gpgedgvtx0  48858  gpg3kgrtriexlem2  48881  gpg3kgrtriexlem5  48884  gpg3kgrtriex  48886  nnsgrp  48974  nnsgrpnmnd  48975  bcpascm1  49163  altgsumbcALT  49165  eluz2cnn0n1  49323  pw2m1lepw2m1  49332  nnennex  49337  logbpw2m1  49379  blenpw2m1  49391  nnpw2blen  49392  nnpw2pmod  49395  blennnt2  49401  blennn0em1  49403  nn0digval  49412  dignn0fr  49413  dignn0ldlem  49414  dig0  49418  nn0sumshdiglemA  49431  nn0sumshdiglemB  49432  nn0sumshdiglem1  49433