Theorem nncn 12373

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℂcc 11228  ℕcn 12365

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396  ax-un 7778  ax-1cn 11288  ax-addcl 11290

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7449  df-om 7905  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-nn 12366

This theorem is used by:  nncni  12375  nn1m1nn  12386  nn1suc  12387  nnaddcl  12388  nnmulcl  12389  nnadd1com  12391  nnaddcom  12392  nnmtmip  12394  nnneneg  12403  nnsub  12412  nndiv  12414  nndivtr  12415  nnnn0addcl  12666  nn0nnaddcl  12667  elnnnn0  12679  nn0sub  12686  nnnegz  12726  elz2  12741  zaddcl  12766  nnaddm1cl  12786  zdiv  12799  zdivadd  12800  zdivmul  12801  nneo  12813  peano5uzi  12818  elq  13107  qmulz  13108  qaddcl  13123  qnegcl  13124  qmulcl  13125  qreccl  13127  rpnnen1lem5  13139  nnledivrp  13264  nn0ledivnn  13265  fseq1m1p1  13763  ubmelm1fzo  13928  subfzo0  13958  quoremz  14025  quoremnn0ALT  14027  intfracq  14029  fldiv  14030  fldiv2  14031  modmulnn  14059  addmodid  14092  addmodidr  14093  modaddmodup  14107  modfzo0difsn  14116  modsumfzodifsn  14117  addmodlteq  14119  nn0ennn  14152  ser1const  14231  expneg  14242  expm1t  14263  nnsqcl  14301  nnlesq  14379  digit2  14410  digit1  14411  expnngt1  14415  facdiv  14461  facndiv  14462  faclbnd  14464  faclbnd4lem1  14467  faclbnd4lem4  14470  bcn1  14487  bcm1k  14489  bcp1n  14490  bcval5  14492  bcn2m1  14498  cshwidxmod  14985  cshwidxm  14990  cshwidxn  14991  repswcshw  14994  isercoll2  15868  divcnv  16054  harmonic  16060  arisum  16061  arisum2  16062  expcnv  16065  pwdif  16069  geomulcvg  16077  mertenslem2  16086  ef0lem  16276  efexp  16301  ruclem12  16441  sqrt2irr  16449  nndivides  16464  modmulconst  16490  dvdsflip  16519  nn0enne  16579  nno  16584  pwp1fsum  16593  divalgmod  16608  ndvdsadd  16612  modgcd  16737  gcdmultiplez  16740  gcddiv  16756  rpmulgcd  16763  rplpwr  16764  sqgcd  16768  expgcd  16769  nn0expgcd  16770  lcmgcdlem  16813  qredeq  16864  qredeu  16865  cncongrcoprm  16877  prmind2  16892  isprm6  16922  divnumden  16956  divdenle  16957  nn0gcdsq  16960  hashgcdlem  16997  pythagtriplem1  17026  pythagtriplem2  17027  pythagtriplem6  17031  pythagtriplem7  17032  pythagtriplem12  17036  pythagtriplem14  17038  pythagtriplem15  17039  pythagtriplem16  17040  pythagtriplem17  17041  pythagtriplem19  17043  pcqcl  17066  pcexp  17069  pcneg  17084  fldivp1  17107  oddprmdvds  17113  prmpwdvds  17114  infpnlem2  17121  prmreclem1  17126  prmreclem6  17131  4sqlem19  17173  vdwapun  17184  vdwapid1  17185  prmonn2  17249  prmgaplem7  17267  mulgnegnn  19326  mulgnnass  19351  mulgmodid  19355  odmod  19793  cnfldmulg  21743  prmirredlem  21811  znidomb  21900  znrrg  21904  cply1mul  22647  chfacfscmul0  23209  chfacfscmulfsupp  23210  chfacfscmulgsum  23211  chfacfpmmul0  23213  chfacfpmmulfsupp  23214  chfacfpmmulgsum  23215  cayhamlem1  23217  cpmadugsumlemF  23227  ovolunlem1  25851  uniioombllem3  25939  vitali  25967  mbfi1fseqlem3  26071  dvexp  26306  dvexp3  26331  plyeq0lem  26562  dgrcolem1  26625  aaliou3lem2  26703  aaliou3lem7  26709  pserdv2  26790  abelthlem6  26796  logtayl  27021  logtaylsum  27022  logtayl2  27023  cxpexp  27029  cxproot  27051  root1id  27115  root1eq1  27116  cxpeq  27118  logbgcd1irr  27155  atantayl  27298  atantayl2  27299  birthdaylem2  27313  dfef2  27331  emcllem2  27357  emcllem3  27358  zetacvg  27375  lgam1  27424  gamfac  27427  basellem2  27442  basellem3  27443  basellem5  27445  basellem8  27448  fsumdvdscom  27545  muinv  27553  chtublem  27571  perfect  27591  pcbcctr  27636  bclbnd  27640  bposlem1  27644  bposlem6  27649  lgssq2  27698  gausslemma2dlem1a  27725  gausslemma2dlem3  27728  2lgslem1a1  27749  2sqlem6  27783  2sqlem10  27788  2sqnn  27799  2sqreunnltlem  27810  rplogsumlem1  27844  dchrmusumlema  27853  dchrmusum2  27854  dchrvmasumiflem1  27861  dchrvmaeq0  27864  dchrisum0re  27873  logdivbnd  27916  cusgrsize2inds  30067  wlkdlem2  30295  crctcshwlkn0lem1  30432  crctcshwlkn0lem6  30437  0enwwlksnge1  30486  wspthsnonn0vne  30539  clwwlknwwlksn  30662  clwwlkinwwlk  30664  clwwlkel  30670  clwwlkf  30671  clwwlkf1  30673  wwlksubclwwlk  30682  eucrctshift  30877  eucrct2eupth  30879  numclwwlk2lem1  31010  numclwlk2lem2f  31011  numclwlk2lem2f1o  31013  ipasslem4  31469  ipasslem5  31470  isarchi3  33824  oddpwdc  35069  eulerpartlemb  35083  fibp1  35116  subfacp1lem6  36130  subfaclim  36133  snmlff  36274  circum  36619  divcnvlin  36689  bcprod  36694  iprodgam  36698  faclim  36702  faclim2  36704  nn0prpwlem  37301  nndivsub  37436  knoppndvlem13  37581  poimirlem13  38756  poimirlem14  38757  poimirlem29  38772  poimirlem30  38773  poimirlem31  38774  poimirlem32  38775  mblfinlem2  38781  ovoliunnfl  38785  voliunnfl  38787  facp2  43396  dvdsexpnn0  43590  renegmulnnass  43733  fimgmcyc  43802  dffltz  43874  irrapxlem1  44033  pellexlem1  44040  pellqrex  44090  2nn0ind  44156  jm2.17c  44173  acongrep  44191  jm2.18  44199  jm2.20nn  44208  jm2.16nn0  44215  proot1ex  44401  hashnzfzclim  45509  binomcxplemnotnn0  45543  nnsplit  46585  clim1fr1  46828  sumnnodd  46857  wallispilem4  47293  wallispilem5  47294  wallispi  47295  wallispi2lem1  47296  wallispi2lem2  47297  wallispi2  47298  stirlinglem1  47299  stirlinglem3  47301  stirlinglem4  47302  stirlinglem5  47303  stirlinglem6  47304  stirlinglem7  47305  stirlinglem8  47306  stirlinglem10  47308  stirlinglem11  47309  stirlinglem12  47310  stirlinglem13  47311  stirlinglem14  47312  stirlinglem15  47313  dirkerper  47321  dirkertrigeqlem1  47323  fouriersw  47456  nnfoctbdjlem  47680  sqrtnnaa  48128  deccarry  48596  subsubelfzo0  48612  submodlt  48641  mod0mul  48647  m1modmmod  48649  modlt0b  48654  sqrtpwpw2p  48838  fmtnodvds  48844  fmtnoprmfac1  48865  fmtnoprmfac2lem1  48866  fmtnoprmfac2  48867  lighneallem2  48906  lighneallem3  48907  lighneallem4  48910  nnennexALTV  49014  perfectALTV  49036  fppr2odd  49044  fpprwppr  49052  fpprwpprb  49053  tgoldbachlt  49129  gpgedgvtx0  49374  gpg3kgrtriexlem2  49397  gpg3kgrtriexlem5  49400  gpg3kgrtriex  49402  nnsgrp  49489  nnsgrpnmnd  49490  bcpascm1  49678  altgsumbcALT  49680  eluz2cnn0n1  49838  pw2m1lepw2m1  49847  nnennex  49852  logbpw2m1  49894  blenpw2m1  49906  nnpw2blen  49907  nnpw2pmod  49910  blennnt2  49916  blennn0em1  49918  nn0digval  49927  dignn0fr  49928  dignn0ldlem  49929  dig0  49933  nn0sumshdiglemA  49946  nn0sumshdiglemB  49947  nn0sumshdiglem1  49948