Theorem nn0cn 9375

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 7993  ℕ₀cn0 9365

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 4201  ax-cnex 8086  ax-resscn 8087  ax-1re 8089  ax-addrcl 8092  ax-rnegex 8104

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 3923  df-inn 9107  df-n0 9366

This theorem is referenced by:  nn0nnaddcl  9396  elnn0nn  9407  difgtsumgt  9512  nn0n0n1ge2  9513  uzaddcl  9777  fzctr  10325  nn0split  10328  elfzoext  10393  zpnn0elfzo1  10409  ubmelm1fzo  10427  subfzo0  10443  modqmuladdnn0  10585  addmodidr  10590  modfzo0difsn  10612  nn0ennn  10650  expadd  10798  expmul  10801  bernneq  10877  bernneq2  10878  faclbnd  10958  faclbnd6  10961  bccmpl  10971  bcn0  10972  bcnn  10974  bcnp1n  10976  bcn2  10981  bcp1m1  10982  bcpasc  10983  bcn2p1  10987  hashfzo0  11040  hashfz0  11042  ccatws1lenp1bg  11163  swrdfv2  11190  swrdspsleq  11194  swrdlsw  11196  pfxmpt  11207  pfxswrd  11233  wrdind  11249  wrd2ind  11250  pfxccatin12lem4  11253  pfxccatin12lem1  11255  pfxccatin12lem2  11258  pfxccatin12  11260  swrdccat3blem  11266  fisum0diag2  11953  hashiun  11984  binom1dif  11993  bcxmas  11995  geolim  12017  efaddlem  12180  efexp  12188  eftlub  12196  demoivreALT  12280  nn0ob  12414  modremain  12435  mulgcdr  12534  nn0seqcvgd  12558  modprmn0modprm0  12774  coprimeprodsq  12775  coprimeprodsq2  12776  pcexp  12827  dvdsprmpweqle  12855  difsqpwdvds  12856  znnen  12964  ennnfonelemp1  12972  mulgneg2  13688  cnfldmulg  14534  nn0subm  14541  rpcxpmul2  15581  0sgmppw  15661  2lgslem1c  15763  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgslem3a1  15770  2lgslem3b1  15771  2lgslem3c1  15772  2lgslem3d1  15773