Theorem nn0cn 9276

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7894  ℕ₀cn0 9266

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7987  ax-resscn 7988  ax-1re 7990  ax-addrcl 7993  ax-rnegex 8005

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-int 3876  df-inn 9008  df-n0 9267

This theorem is referenced by:  nn0nnaddcl  9297  elnn0nn  9308  difgtsumgt  9412  nn0n0n1ge2  9413  uzaddcl  9677  fzctr  10225  nn0split  10228  zpnn0elfzo1  10301  ubmelm1fzo  10319  subfzo0  10335  modqmuladdnn0  10477  addmodidr  10482  modfzo0difsn  10504  nn0ennn  10542  expadd  10690  expmul  10693  bernneq  10769  bernneq2  10770  faclbnd  10850  faclbnd6  10853  bccmpl  10863  bcn0  10864  bcnn  10866  bcnp1n  10868  bcn2  10873  bcp1m1  10874  bcpasc  10875  bcn2p1  10879  hashfzo0  10932  hashfz0  10934  fisum0diag2  11629  hashiun  11660  binom1dif  11669  bcxmas  11671  geolim  11693  efaddlem  11856  efexp  11864  eftlub  11872  demoivreALT  11956  nn0ob  12090  modremain  12111  mulgcdr  12210  nn0seqcvgd  12234  modprmn0modprm0  12450  coprimeprodsq  12451  coprimeprodsq2  12452  pcexp  12503  dvdsprmpweqle  12531  difsqpwdvds  12532  znnen  12640  ennnfonelemp1  12648  mulgneg2  13362  cnfldmulg  14208  nn0subm  14215  rpcxpmul2  15233  0sgmppw  15313  2lgslem1c  15415  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425