Theorem nn0cn 9253

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7872  ℕ₀cn0 9243

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4148  ax-cnex 7965  ax-resscn 7966  ax-1re 7968  ax-addrcl 7971  ax-rnegex 7983

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-un 3158  df-in 3160  df-ss 3167  df-sn 3625  df-int 3872  df-inn 8985  df-n0 9244

This theorem is referenced by:  nn0nnaddcl  9274  elnn0nn  9285  difgtsumgt  9389  nn0n0n1ge2  9390  uzaddcl  9654  fzctr  10202  nn0split  10205  zpnn0elfzo1  10278  ubmelm1fzo  10296  subfzo0  10312  modqmuladdnn0  10442  addmodidr  10447  modfzo0difsn  10469  nn0ennn  10507  expadd  10655  expmul  10658  bernneq  10734  bernneq2  10735  faclbnd  10815  faclbnd6  10818  bccmpl  10828  bcn0  10829  bcnn  10831  bcnp1n  10833  bcn2  10838  bcp1m1  10839  bcpasc  10840  bcn2p1  10844  hashfzo0  10897  hashfz0  10899  fisum0diag2  11593  hashiun  11624  binom1dif  11633  bcxmas  11635  geolim  11657  efaddlem  11820  efexp  11828  eftlub  11836  demoivreALT  11920  nn0ob  12052  modremain  12073  mulgcdr  12158  nn0seqcvgd  12182  modprmn0modprm0  12397  coprimeprodsq  12398  coprimeprodsq2  12399  pcexp  12450  dvdsprmpweqle  12478  difsqpwdvds  12479  znnen  12558  ennnfonelemp1  12566  mulgneg2  13229  cnfldmulg  14075  nn0subm  14082  2lgslem1c  15247  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257