Theorem nn0cn 9402

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8020  ℕ₀cn0 9392

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 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119  ax-rnegex 8131

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 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-int 3927  df-inn 9134  df-n0 9393

This theorem is referenced by:  nn0nnaddcl  9423  elnn0nn  9434  difgtsumgt  9539  nn0n0n1ge2  9540  uzaddcl  9810  fzctr  10358  nn0split  10361  elfzoext  10427  zpnn0elfzo1  10443  ubmelm1fzo  10461  subfzo0  10478  modqmuladdnn0  10620  addmodidr  10625  modfzo0difsn  10647  nn0ennn  10685  expadd  10833  expmul  10836  bernneq  10912  bernneq2  10913  faclbnd  10993  faclbnd6  10996  bccmpl  11006  bcn0  11007  bcnn  11009  bcnp1n  11011  bcn2  11016  bcp1m1  11017  bcpasc  11018  bcn2p1  11022  hashfzo0  11077  hashfz0  11079  ccatalpha  11180  ccatws1lenp1bg  11202  ccatw2s1leng  11205  swrdfv2  11234  swrdspsleq  11238  swrdlsw  11240  pfxmpt  11251  pfxswrd  11277  wrdind  11293  wrd2ind  11294  pfxccatin12lem4  11297  pfxccatin12lem1  11299  pfxccatin12lem2  11302  pfxccatin12  11304  swrdccat3blem  11310  fisum0diag2  11998  hashiun  12029  binom1dif  12038  bcxmas  12040  geolim  12062  efaddlem  12225  efexp  12233  eftlub  12241  demoivreALT  12325  nn0ob  12459  modremain  12480  mulgcdr  12579  nn0seqcvgd  12603  modprmn0modprm0  12819  coprimeprodsq  12820  coprimeprodsq2  12821  pcexp  12872  dvdsprmpweqle  12900  difsqpwdvds  12901  znnen  13009  ennnfonelemp1  13017  mulgneg2  13733  cnfldmulg  14580  nn0subm  14587  rpcxpmul2  15627  0sgmppw  15707  2lgslem1c  15809  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  wlklenvclwlk  16170  clwwlknonex2lem2  16233