Theorem nn0cn 12411

Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
nn0cn	⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ)

Proof of Theorem nn0cn

Step	Hyp	Ref	Expression
1		nn0sscn 12406	. 2 ⊢ ℕ0 ⊆ ℂ
2	1	sseli 3929	1 ⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℂcc 11024  ℕ₀cn0 12401

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-i2m1 11094

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-n0 12402

This theorem is referenced by:  nn0nnaddcl  12432  elnn0nn  12443  nn0sub  12451  difgtsumgt  12454  nn0le2x  12455  nn0n0n1ge2  12469  uzaddcl  12817  fzctr  13556  nn0split  13559  elfzoext  13638  zpnn0elfzo1  13655  ubmelm1fzo  13679  subfzo0  13708  quoremnn0ALT  13777  modmuladdnn0  13838  addmodidr  13843  modfzo0difsn  13866  nn0ennn  13902  expadd  14027  expmul  14030  bernneq  14152  bernneq2  14153  faclbnd  14213  faclbnd4lem3  14218  faclbnd4lem4  14219  faclbnd6  14222  bccmpl  14232  bcn0  14233  bcnn  14235  bcnp1n  14237  bcn2  14242  bcp1m1  14243  bcpasc  14244  bcn2p1  14248  hashfzo0  14353  hashfz0  14355  hashxplem  14356  hashdifsnp1  14429  ccatalpha  14517  ccatws1lenp1b  14545  ccatw2s1len  14549  swrdfv2  14585  swrdspsleq  14589  swrdlsw  14591  pfxmpt  14602  pfxswrd  14629  wrdind  14645  wrd2ind  14646  pfxccatin12lem4  14649  pfxccatin12lem1  14651  pfxccatin12lem2  14654  pfxccatin12  14656  swrdccat3blem  14662  repswswrd  14707  repswrevw  14710  cshwidxmodr  14727  2cshw  14736  2cshwcshw  14748  cshwcshid  14750  swrds2  14863  swrd2lsw  14875  iseraltlem2  15606  fsum0diag2  15706  hashiun  15745  ackbijnn  15751  binom1dif  15756  bcxmas  15758  geolim  15793  geomulcvg  15799  risefacval2  15933  fallfacval2  15934  risefaccl  15938  fallfaccl  15939  fallrisefac  15948  risefacp1  15952  fallfacp1  15953  fallfacfac  15968  bpolysum  15976  fsumkthpow  15979  bpoly4  15982  fsumcube  15983  efaddlem  16016  efexp  16026  eftlub  16034  demoivreALT  16126  nn0ob  16311  divalglem4  16323  modremain  16335  mulgcdr  16477  nn0rppwr  16488  nn0seqcvgd  16497  modprmn0modprm0  16735  coprimeprodsq  16736  coprimeprodsq2  16737  pcexp  16787  dvdsprmpweqle  16814  difsqpwdvds  16815  ramub1lem1  16954  prmop1  16966  chnccat  18549  smndex2dlinvh  18842  mulgneg2  19038  mndodcongi  19472  oddvdsnn0  19473  sylow1lem1  19527  efgsrel  19663  fincygsubgodd  20043  srgbinomlem4  20164  cnfldmulg  21358  nn0subm  21377  nn0srg  21392  psrbagconf1o  21885  psrass1lem  21888  psrlidm  21917  psrass1  21919  psrcom  21923  mplsubrglem  21959  mplmonmul  21991  psdmul  22109  psdmvr  22112  psropprmul  22178  coe1sclmul  22224  coe1sclmul2  22226  dvnadd  25887  ply1divex  26098  elqaalem2  26284  geolim3  26303  dvradcnv  26386  pserdv2  26396  logtayllem  26624  logtayl  26625  cxpmul2  26654  atantayl3  26905  leibpilem2  26907  leibpi  26908  log2cnv  26910  dmgmaddn0  26989  chpp1  27121  0sgmppw  27165  logexprlim  27192  dchrhash  27238  bcctr  27242  bcmono  27244  bcmax  27245  bcp1ctr  27246  2lgslem1c  27360  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgslem3d1  27370  2sqreultlem  27414  2sqreulem2  27419  dchrisumlem1  27456  ostth2lem2  27601  wlklenvclwlk  29727  upgrwlkdvdelem  29809  wwlknp  29916  wwlknlsw  29920  wlkiswwlks1  29940  wlklnwwlkln2lem  29955  wlknwwlksnbij  29961  wwlksnred  29965  wwlksnext  29966  wwlksnredwwlkn  29968  wwlksnextwrd  29970  wwlksnextinj  29972  wwlksnextproplem2  29983  wwlksnextproplem3  29984  wspthsnwspthsnon  29989  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  clwlkclwwlklem3  30076  wwlksext2clwwlk  30132  clwwlknonex2lem2  30183  eucrctshift  30318  eucrct2eupth  30320  numclwwlk2lem1lem  30417  numclwwlk1  30436  numclwwlk7  30466  ipasslem1  30906  ipasslem2  30907  dpfrac1  32973  archirngz  33271  nn0constr  33918  pthhashvtx  35322  subfacval2  35381  bccolsum  35933  faclimlem1  35937  poimirlem28  37849  heiborlem4  38015  heiborlem6  38017  lcmineqlem3  42285  facp2  42397  sticksstones7  42406  oddnumth  42566  nicomachus  42567  sumcubes  42568  pell14qrgt0  43101  pell14qrdich  43111  pell1qrge1  43112  2nn0ind  43187  jm2.17a  43202  jm2.18  43230  jm2.19lem3  43233  proot1ex  43438  bcc0  44581  dvradcnv2  44588  binomcxplemrat  44591  binomcxplemnotnn0  44597  fperiodmullem  45551  stoweidlem10  46254  stoweidlem17  46261  stoweidlem26  46270  stirlinglem5  46322  stirlinglem7  46324  etransclem23  46501  cjnpoly  47135  subsubelfzo0  47572  fargshiftfo  47688  fmtnodvds  47790  goldbachthlem1  47791  fmtnofac2lem  47814  fmtnofac1  47816  nn0onn0exALTV  47945  nn0enn0exALTV  47946  isubgr3stgrlem2  48213  nn0mnd  48425  ply1mulgsumlem1  48632  ply1mulgsumlem2  48633  nn0onn0ex  48769  nn0enn0ex  48770  fllog2  48814  dignn0fr  48847  digexp  48853  0dig2nn0e  48858  0dig2nn0o  48859  dignn0ehalf  48863  nn0mulfsum  48870  nn0mullong  48871  itcovalpclem1  48916  itcovalpclem2  48917  itcovalt2lem2lem2  48920  ackval1  48927  ackval2  48928  ackval3  48929