Theorem nn0cn 9584

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ℂcc 8183  ℕ₀cn0 9574

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251  ax-cnex 8276  ax-resscn 8277  ax-1re 8279  ax-addrcl 8282  ax-rnegex 8294

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-sn 3715  df-int 3971  df-inn 9314  df-n0 9575

This theorem is used by:  nn0nnaddcl  9605  elnn0nn  9616  difgtsumgt  9725  nn0n0n1ge2  9726  uzaddcl  10002  fzctr  10557  nn0split  10560  elfzoext  10627  zpnn0elfzo1  10643  ubmelm1fzo  10661  subfzo0  10678  modqmuladdnn0  10826  addmodidr  10831  modfzo0difsn  10853  nn0ennn  10891  expadd  11039  expmul  11042  bernneq  11119  bernneq2  11120  faclbnd  11201  faclbnd6  11204  bccmpl  11214  bcn0  11215  bcnn  11217  bcnp1n  11219  bcn2  11224  bcp1m1  11225  bcpasc  11226  bcn2p1  11231  hashfzo0  11286  hashfz0  11288  ccatalpha  11403  ccatws1lenp1bg  11425  ccatw2s1leng  11428  swrdfv2  11457  swrdspsleq  11461  swrdlsw  11463  pfxmpt  11474  pfxswrd  11500  wrdind  11516  wrd2ind  11517  pfxccatin12lem4  11520  pfxccatin12lem1  11522  pfxccatin12lem2  11525  pfxccatin12  11527  swrdccat3blem  11533  fisum0diag2  12239  hashiun  12270  binom1dif  12279  bcxmas  12281  geolim  12303  efaddlem  12466  efexp  12474  eftlub  12482  demoivreALT  12566  nn0ob  12700  modremain  12721  mulgcdr  12820  nn0seqcvgd  12844  modprmn0modprm0  13064  coprimeprodsq  13065  coprimeprodsq2  13066  pcexp  13117  dvdsprmpweqle  13145  difsqpwdvds  13146  znnen  13347  ennnfonelemp1  13355  mulgneg2  14018  cnfldmulg  15022  nn0subm  15029  psrbagconf1o  15174  psrass1filem  15177  psrlidmfi  15199  psrass1fi  15201  rpcxpmul2  16146  0sgmppw  16287  bcctr  16302  bcmono  16304  bcmax  16305  bcp1ctr  16306  2lgslem1c  16414  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  wlklenvclwlk  16819  clwwlknonex2lem2  16884