Theorem nn0cn 9157

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

Syntax hints:   → wi 4   ∈ wcel 2146  ℂcc 7784  ℕ₀cn0 9147

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-sep 4116  ax-cnex 7877  ax-resscn 7878  ax-1re 7880  ax-addrcl 7883  ax-rnegex 7895

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-v 2737  df-un 3131  df-in 3133  df-ss 3140  df-sn 3595  df-int 3841  df-inn 8891  df-n0 9148

This theorem is referenced by:  nn0nnaddcl  9178  elnn0nn  9189  difgtsumgt  9293  nn0n0n1ge2  9294  uzaddcl  9557  fzctr  10101  nn0split  10104  zpnn0elfzo1  10176  ubmelm1fzo  10194  subfzo0  10210  modqmuladdnn0  10336  addmodidr  10341  modfzo0difsn  10363  nn0ennn  10401  expadd  10530  expmul  10533  bernneq  10608  bernneq2  10609  faclbnd  10687  faclbnd6  10690  bccmpl  10700  bcn0  10701  bcnn  10703  bcnp1n  10705  bcn2  10710  bcp1m1  10711  bcpasc  10712  bcn2p1  10716  hashfzo0  10769  hashfz0  10771  fisum0diag2  11421  hashiun  11452  binom1dif  11461  bcxmas  11463  geolim  11485  efaddlem  11648  efexp  11656  eftlub  11664  demoivreALT  11747  nn0ob  11878  modremain  11899  mulgcdr  11984  nn0seqcvgd  12006  modprmn0modprm0  12221  coprimeprodsq  12222  coprimeprodsq2  12223  pcexp  12274  dvdsprmpweqle  12301  difsqpwdvds  12302  znnen  12364  ennnfonelemp1  12372  mulgneg2  12875