Theorem nn0cn 9390

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8008  ℕ₀cn0 9380

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202  ax-cnex 8101  ax-resscn 8102  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-int 3924  df-inn 9122  df-n0 9381

This theorem is referenced by:  nn0nnaddcl  9411  elnn0nn  9422  difgtsumgt  9527  nn0n0n1ge2  9528  uzaddcl  9793  fzctr  10341  nn0split  10344  elfzoext  10410  zpnn0elfzo1  10426  ubmelm1fzo  10444  subfzo0  10460  modqmuladdnn0  10602  addmodidr  10607  modfzo0difsn  10629  nn0ennn  10667  expadd  10815  expmul  10818  bernneq  10894  bernneq2  10895  faclbnd  10975  faclbnd6  10978  bccmpl  10988  bcn0  10989  bcnn  10991  bcnp1n  10993  bcn2  10998  bcp1m1  10999  bcpasc  11000  bcn2p1  11004  hashfzo0  11058  hashfz0  11060  ccatalpha  11161  ccatws1lenp1bg  11183  swrdfv2  11210  swrdspsleq  11214  swrdlsw  11216  pfxmpt  11227  pfxswrd  11253  wrdind  11269  wrd2ind  11270  pfxccatin12lem4  11273  pfxccatin12lem1  11275  pfxccatin12lem2  11278  pfxccatin12  11280  swrdccat3blem  11286  fisum0diag2  11973  hashiun  12004  binom1dif  12013  bcxmas  12015  geolim  12037  efaddlem  12200  efexp  12208  eftlub  12216  demoivreALT  12300  nn0ob  12434  modremain  12455  mulgcdr  12554  nn0seqcvgd  12578  modprmn0modprm0  12794  coprimeprodsq  12795  coprimeprodsq2  12796  pcexp  12847  dvdsprmpweqle  12875  difsqpwdvds  12876  znnen  12984  ennnfonelemp1  12992  mulgneg2  13708  cnfldmulg  14555  nn0subm  14562  rpcxpmul2  15602  0sgmppw  15682  2lgslem1c  15784  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgslem3a1  15791  2lgslem3b1  15792  2lgslem3c1  15793  2lgslem3d1  15794  wlklenvclwlk  16114