Theorem nn0cn 9412

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  ℕ₀cn0 9402

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207  ax-cnex 8123  ax-resscn 8124  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-int 3929  df-inn 9144  df-n0 9403

This theorem is referenced by:  nn0nnaddcl  9433  elnn0nn  9444  difgtsumgt  9549  nn0n0n1ge2  9550  uzaddcl  9820  fzctr  10368  nn0split  10371  elfzoext  10438  zpnn0elfzo1  10454  ubmelm1fzo  10472  subfzo0  10489  modqmuladdnn0  10631  addmodidr  10636  modfzo0difsn  10658  nn0ennn  10696  expadd  10844  expmul  10847  bernneq  10923  bernneq2  10924  faclbnd  11004  faclbnd6  11007  bccmpl  11017  bcn0  11018  bcnn  11020  bcnp1n  11022  bcn2  11027  bcp1m1  11028  bcpasc  11029  bcn2p1  11033  hashfzo0  11088  hashfz0  11090  ccatalpha  11194  ccatws1lenp1bg  11216  ccatw2s1leng  11219  swrdfv2  11248  swrdspsleq  11252  swrdlsw  11254  pfxmpt  11265  pfxswrd  11291  wrdind  11307  wrd2ind  11308  pfxccatin12lem4  11311  pfxccatin12lem1  11313  pfxccatin12lem2  11316  pfxccatin12  11318  swrdccat3blem  11324  fisum0diag2  12013  hashiun  12044  binom1dif  12053  bcxmas  12055  geolim  12077  efaddlem  12240  efexp  12248  eftlub  12256  demoivreALT  12340  nn0ob  12474  modremain  12495  mulgcdr  12594  nn0seqcvgd  12618  modprmn0modprm0  12834  coprimeprodsq  12835  coprimeprodsq2  12836  pcexp  12887  dvdsprmpweqle  12915  difsqpwdvds  12916  znnen  13024  ennnfonelemp1  13032  mulgneg2  13748  cnfldmulg  14596  nn0subm  14603  rpcxpmul2  15643  0sgmppw  15723  2lgslem1c  15825  2lgslem3a  15828  2lgslem3b  15829  2lgslem3c  15830  2lgslem3d  15831  2lgslem3a1  15832  2lgslem3b1  15833  2lgslem3c1  15834  2lgslem3d1  15835  wlklenvclwlk  16230  clwwlknonex2lem2  16295