Theorem nn0cn 8888

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

Syntax hints:   → wi 4   ∈ wcel 1463  ℂcc 7542  ℕ₀cn0 8878

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006  ax-cnex 7633  ax-resscn 7634  ax-1re 7636  ax-addrcl 7639  ax-rnegex 7651

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ral 2395  df-rex 2396  df-v 2659  df-un 3041  df-in 3043  df-ss 3050  df-sn 3499  df-int 3738  df-inn 8628  df-n0 8879

This theorem is referenced by:  nn0nnaddcl  8909  elnn0nn  8920  nn0n0n1ge2  9022  uzaddcl  9280  fzctr  9800  nn0split  9803  zpnn0elfzo1  9875  ubmelm1fzo  9893  subfzo0  9909  modqmuladdnn0  10031  addmodidr  10036  modfzo0difsn  10058  nn0ennn  10096  expadd  10225  expmul  10228  bernneq  10302  bernneq2  10303  faclbnd  10377  faclbnd6  10380  bccmpl  10390  bcn0  10391  bcnn  10393  bcnp1n  10395  bcn2  10400  bcp1m1  10401  bcpasc  10402  bcn2p1  10406  hashfzo0  10459  hashfz0  10461  fisum0diag2  11105  hashiun  11136  binom1dif  11145  bcxmas  11147  geolim  11169  efaddlem  11228  efexp  11236  eftlub  11244  demoivreALT  11327  nn0ob  11450  modremain  11471  mulgcdr  11549  nn0seqcvgd  11565  znnen  11753  ennnfonelemp1  11761