Theorem nncn 11028

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

Syntax hints:   → wi 4   ∈ wcel 1990  ℂcc 9934  ℕcn 11020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-nn 11021

This theorem is referenced by:  nn1m1nn  11040  nn1suc  11041  nnaddcl  11042  nnmulcl  11043  nnsub  11059  nndiv  11061  nndivtr  11062  nnnn0addcl  11323  nn0nnaddcl  11324  elnnnn0  11336  nn0sub  11343  nnnegz  11380  elz2  11394  zaddcl  11417  nnaddm1cl  11434  zdiv  11447  zdivadd  11448  zdivmul  11449  nneo  11461  peano5uzi  11466  elq  11790  qmulz  11791  qaddcl  11804  qnegcl  11805  qmulcl  11806  qreccl  11808  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  nnledivrp  11940  nn0ledivnn  11941  fseq1m1p1  12415  ubmelm1fzo  12564  subfzo0  12590  quoremz  12654  quoremnn0ALT  12656  intfracq  12658  fldiv  12659  fldiv2  12660  modmulnn  12688  addmodid  12718  addmodidr  12719  modaddmodup  12733  modfzo0difsn  12742  modsumfzodifsn  12743  addmodlteq  12745  nn0ennn  12778  ser1const  12857  expneg  12868  expm1t  12888  nnsqcl  12933  nnlesq  12968  digit2  12997  digit1  12998  facdiv  13074  facndiv  13075  faclbnd  13077  faclbnd4lem1  13080  faclbnd4lem4  13083  bcn1  13100  bcm1k  13102  bcp1n  13103  bcval5  13105  bcn2m1  13111  swrdccatwrd  13468  cshwidxmod  13549  cshwidxm  13554  cshwidxn  13555  repswcshw  13558  isercoll2  14399  divcnv  14585  harmonic  14591  arisum  14592  arisum2  14593  expcnv  14596  geomulcvg  14607  mertenslem2  14617  ef0lem  14809  efexp  14831  ruclem12  14970  sqrt2irr  14979  nndivides  14990  modmulconst  15013  dvdsflip  15039  nn0enne  15094  nno  15098  pwp1fsum  15114  divalgmod  15129  divalgmodOLD  15130  ndvdsadd  15134  modgcd  15253  gcddiv  15268  gcdmultiple  15269  gcdmultiplez  15270  rpmulgcd  15275  rplpwr  15276  sqgcd  15278  lcmgcdlem  15319  qredeq  15371  qredeu  15372  cncongrcoprm  15384  prmind2  15398  isprm6  15426  divnumden  15456  divdenle  15457  nn0gcdsq  15460  hashgcdlem  15493  pythagtriplem1  15521  pythagtriplem2  15522  pythagtriplem6  15526  pythagtriplem7  15527  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem15  15534  pythagtriplem16  15535  pythagtriplem17  15536  pythagtriplem19  15538  pcqcl  15561  pcexp  15564  pcneg  15578  fldivp1  15601  oddprmdvds  15607  prmpwdvds  15608  infpnlem2  15615  prmreclem1  15620  prmreclem6  15625  4sqlem19  15667  vdwapun  15678  vdwapid1  15679  prmonn2  15743  prmgaplem7  15761  mulgnegnn  17551  mulgnnass  17576  mulgnnassOLD  17577  mulgmodid  17581  odmod  17965  cply1mul  19664  cnfldmulg  19778  prmirredlem  19841  znidomb  19910  znrrg  19914  chfacfscmul0  20663  chfacfscmulfsupp  20664  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulfsupp  20668  chfacfpmmulgsum  20669  cayhamlem1  20671  cpmadugsumlemF  20681  ovolunlem1  23265  uniioombllem3  23353  vitali  23382  mbfi1fseqlem3  23484  dvexp  23716  dvexp3  23741  plyeq0lem  23966  dgrcolem1  24029  aaliou3lem2  24098  aaliou3lem7  24104  pserdv2  24184  abelthlem6  24190  logtayl  24406  logtaylsum  24407  logtayl2  24408  cxpexp  24414  cxproot  24436  root1id  24495  root1eq1  24496  cxpeq  24498  atantayl  24664  atantayl2  24665  birthdaylem2  24679  dfef2  24697  emcllem2  24723  emcllem3  24724  zetacvg  24741  lgam1  24790  gamfac  24793  basellem2  24808  basellem3  24809  basellem5  24811  basellem8  24814  mumul  24907  fsumdvdscom  24911  muinv  24919  chtublem  24936  perfect  24956  pcbcctr  25001  bclbnd  25005  bposlem1  25009  bposlem6  25014  lgssq2  25063  gausslemma2dlem1a  25090  gausslemma2dlem3  25093  2lgslem1a1  25114  2sqlem6  25148  2sqlem10  25153  rplogsumlem1  25173  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumiflem1  25190  dchrvmaeq0  25193  dchrisum0re  25202  logdivbnd  25245  cusgrsize2inds  26349  wlkdlem2  26580  crctcshwlkn0lem1  26702  crctcshwlkn0lem6  26707  0enwwlksnge1  26749  wspthsnonn0vne  26813  clwwlkinwwlk  26905  clwwlksel  26914  clwwlksf  26915  clwwlksf1  26917  wwlksubclwwlks  26925  eucrctshift  27103  eucrct2eupth  27105  clwwlksnwwlksn  27209  numclwwlk2lem1  27235  numclwlk2lem2f  27236  numclwlk2lem2f1o  27238  ipasslem4  27689  ipasslem5  27690  isarchi3  29741  oddpwdc  30416  eulerpartlemb  30430  fibp1  30463  subfacp1lem6  31167  subfaclim  31170  snmlff  31311  circum  31568  divcnvlin  31618  bcprod  31624  iprodgam  31628  faclim  31632  faclim2  31634  nn0prpwlem  32317  nndivsub  32456  knoppndvlem13  32515  poimirlem13  33422  poimirlem14  33423  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  irrapxlem1  37386  pellexlem1  37393  pellqrex  37443  2nn0ind  37510  jm2.17c  37529  acongrep  37547  jm2.18  37555  jm2.20nn  37564  jm2.16nn0  37571  proot1ex  37779  hashnzfzclim  38521  binomcxplemnotnn0  38555  nnsplit  39574  clim1fr1  39833  sumnnodd  39862  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem14  40304  stirlinglem15  40305  dirkerper  40313  dirkertrigeqlem1  40315  fouriersw  40448  nnfoctbdjlem  40672  deccarry  41321  subsubelfzo0  41336  sqrtpwpw2p  41450  fmtnodvds  41456  fmtnoprmfac1  41477  fmtnoprmfac2lem1  41478  fmtnoprmfac2  41479  pwdif  41501  lighneallem2  41523  lighneallem3  41524  lighneallem4  41527  perfectALTV  41632  tgoldbachlt  41704  tgoldbachltOLD  41710  nnsgrp  41817  nnsgrpnmnd  41818  bcpascm1  42129  altgsumbcALT  42131  eluz2cnn0n1  42301  pw2m1lepw2m1  42310  mod0mul  42314  m1modmmod  42316  logbpw2m1  42361  blenpw2m1  42373  nnpw2blen  42374  nnpw2pmod  42377  blennnt2  42383  blennn0em1  42385  nn0digval  42394  dignn0fr  42395  dignn0ldlem  42396  dig0  42400  nn0sumshdiglemA  42413  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415