Theorem nn0cn 9506

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

Syntax hints:   → wi 4   ∈ wcel 2203  ℂcc 8125  ℕ₀cn0 9496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4228  ax-cnex 8218  ax-resscn 8219  ax-1re 8221  ax-addrcl 8224  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-int 3950  df-inn 9238  df-n0 9497

This theorem is referenced by:  nn0nnaddcl  9527  elnn0nn  9538  difgtsumgt  9647  nn0n0n1ge2  9648  uzaddcl  9918  fzctr  10467  nn0split  10470  elfzoext  10537  zpnn0elfzo1  10553  ubmelm1fzo  10571  subfzo0  10588  modqmuladdnn0  10730  addmodidr  10735  modfzo0difsn  10757  nn0ennn  10795  expadd  10943  expmul  10946  bernneq  11022  bernneq2  11023  faclbnd  11103  faclbnd6  11106  bccmpl  11116  bcn0  11117  bcnn  11119  bcnp1n  11121  bcn2  11126  bcp1m1  11127  bcpasc  11128  bcn2p1  11133  hashfzo0  11188  hashfz0  11190  ccatalpha  11301  ccatws1lenp1bg  11323  ccatw2s1leng  11326  swrdfv2  11355  swrdspsleq  11359  swrdlsw  11361  pfxmpt  11372  pfxswrd  11398  wrdind  11414  wrd2ind  11415  pfxccatin12lem4  11418  pfxccatin12lem1  11420  pfxccatin12lem2  11423  pfxccatin12  11425  swrdccat3blem  11431  fisum0diag2  12133  hashiun  12164  binom1dif  12173  bcxmas  12175  geolim  12197  efaddlem  12360  efexp  12368  eftlub  12376  demoivreALT  12460  nn0ob  12594  modremain  12615  mulgcdr  12714  nn0seqcvgd  12738  modprmn0modprm0  12954  coprimeprodsq  12955  coprimeprodsq2  12956  pcexp  13007  dvdsprmpweqle  13035  difsqpwdvds  13036  znnen  13149  ennnfonelemp1  13157  mulgneg2  13873  cnfldmulg  14724  nn0subm  14731  psrbagconf1o  14828  rpcxpmul2  15778  0sgmppw  15861  2lgslem1c  15963  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgslem3a1  15970  2lgslem3b1  15971  2lgslem3c1  15972  2lgslem3d1  15973  wlklenvclwlk  16368  clwwlknonex2lem2  16433