Theorem nn0cn 9411

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8029  ℕ₀cn0 9401

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 8122  ax-resscn 8123  ax-1re 8125  ax-addrcl 8128  ax-rnegex 8140

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 9143  df-n0 9402

This theorem is referenced by:  nn0nnaddcl  9432  elnn0nn  9443  difgtsumgt  9548  nn0n0n1ge2  9549  uzaddcl  9819  fzctr  10367  nn0split  10370  elfzoext  10436  zpnn0elfzo1  10452  ubmelm1fzo  10470  subfzo0  10487  modqmuladdnn0  10629  addmodidr  10634  modfzo0difsn  10656  nn0ennn  10694  expadd  10842  expmul  10845  bernneq  10921  bernneq2  10922  faclbnd  11002  faclbnd6  11005  bccmpl  11015  bcn0  11016  bcnn  11018  bcnp1n  11020  bcn2  11025  bcp1m1  11026  bcpasc  11027  bcn2p1  11031  hashfzo0  11086  hashfz0  11088  ccatalpha  11189  ccatws1lenp1bg  11211  ccatw2s1leng  11214  swrdfv2  11243  swrdspsleq  11247  swrdlsw  11249  pfxmpt  11260  pfxswrd  11286  wrdind  11302  wrd2ind  11303  pfxccatin12lem4  11306  pfxccatin12lem1  11308  pfxccatin12lem2  11311  pfxccatin12  11313  swrdccat3blem  11319  fisum0diag2  12007  hashiun  12038  binom1dif  12047  bcxmas  12049  geolim  12071  efaddlem  12234  efexp  12242  eftlub  12250  demoivreALT  12334  nn0ob  12468  modremain  12489  mulgcdr  12588  nn0seqcvgd  12612  modprmn0modprm0  12828  coprimeprodsq  12829  coprimeprodsq2  12830  pcexp  12881  dvdsprmpweqle  12909  difsqpwdvds  12910  znnen  13018  ennnfonelemp1  13026  mulgneg2  13742  cnfldmulg  14589  nn0subm  14596  rpcxpmul2  15636  0sgmppw  15716  2lgslem1c  15818  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  wlklenvclwlk  16223  clwwlknonex2lem2  16288