Theorem nn0cn 9454

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8073  ℕ₀cn0 9444

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-sep 4212  ax-cnex 8166  ax-resscn 8167  ax-1re 8169  ax-addrcl 8172  ax-rnegex 8184

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-sn 3679  df-int 3934  df-inn 9186  df-n0 9445

This theorem is referenced by:  nn0nnaddcl  9475  elnn0nn  9486  difgtsumgt  9593  nn0n0n1ge2  9594  uzaddcl  9864  fzctr  10413  nn0split  10416  elfzoext  10483  zpnn0elfzo1  10499  ubmelm1fzo  10517  subfzo0  10534  modqmuladdnn0  10676  addmodidr  10681  modfzo0difsn  10703  nn0ennn  10741  expadd  10889  expmul  10892  bernneq  10968  bernneq2  10969  faclbnd  11049  faclbnd6  11052  bccmpl  11062  bcn0  11063  bcnn  11065  bcnp1n  11067  bcn2  11072  bcp1m1  11073  bcpasc  11074  bcn2p1  11078  hashfzo0  11133  hashfz0  11135  ccatalpha  11239  ccatws1lenp1bg  11261  ccatw2s1leng  11264  swrdfv2  11293  swrdspsleq  11297  swrdlsw  11299  pfxmpt  11310  pfxswrd  11336  wrdind  11352  wrd2ind  11353  pfxccatin12lem4  11356  pfxccatin12lem1  11358  pfxccatin12lem2  11361  pfxccatin12  11363  swrdccat3blem  11369  fisum0diag2  12071  hashiun  12102  binom1dif  12111  bcxmas  12113  geolim  12135  efaddlem  12298  efexp  12306  eftlub  12314  demoivreALT  12398  nn0ob  12532  modremain  12553  mulgcdr  12652  nn0seqcvgd  12676  modprmn0modprm0  12892  coprimeprodsq  12893  coprimeprodsq2  12894  pcexp  12945  dvdsprmpweqle  12973  difsqpwdvds  12974  znnen  13082  ennnfonelemp1  13090  mulgneg2  13806  cnfldmulg  14655  nn0subm  14662  psrbagconf1o  14757  rpcxpmul2  15707  0sgmppw  15790  2lgslem1c  15892  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgslem3d1  15902  wlklenvclwlk  16297  clwwlknonex2lem2  16362