Theorem nn0cn 9578

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

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

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 4249  ax-cnex 8271  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277  ax-rnegex 8289

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 9308  df-n0 9569

This theorem is used by:  nn0nnaddcl  9599  elnn0nn  9610  difgtsumgt  9719  nn0n0n1ge2  9720  uzaddcl  9996  fzctr  10551  nn0split  10554  elfzoext  10621  zpnn0elfzo1  10637  ubmelm1fzo  10655  subfzo0  10672  modqmuladdnn0  10820  addmodidr  10825  modfzo0difsn  10847  nn0ennn  10885  expadd  11033  expmul  11036  bernneq  11113  bernneq2  11114  faclbnd  11195  faclbnd6  11198  bccmpl  11208  bcn0  11209  bcnn  11211  bcnp1n  11213  bcn2  11218  bcp1m1  11219  bcpasc  11220  bcn2p1  11225  hashfzo0  11280  hashfz0  11282  ccatalpha  11397  ccatws1lenp1bg  11419  ccatw2s1leng  11422  swrdfv2  11451  swrdspsleq  11455  swrdlsw  11457  pfxmpt  11468  pfxswrd  11494  wrdind  11510  wrd2ind  11511  pfxccatin12lem4  11514  pfxccatin12lem1  11516  pfxccatin12lem2  11519  pfxccatin12  11521  swrdccat3blem  11527  fisum0diag2  12233  hashiun  12264  binom1dif  12273  bcxmas  12275  geolim  12297  efaddlem  12460  efexp  12468  eftlub  12476  demoivreALT  12560  nn0ob  12694  modremain  12715  mulgcdr  12814  nn0seqcvgd  12838  modprmn0modprm0  13058  coprimeprodsq  13059  coprimeprodsq2  13060  pcexp  13111  dvdsprmpweqle  13139  difsqpwdvds  13140  znnen  13341  ennnfonelemp1  13349  mulgneg2  14012  cnfldmulg  14997  nn0subm  15004  psrbagconf1o  15149  rpcxpmul2  16110  0sgmppw  16248  bcctr  16263  bcmono  16265  bcmax  16266  bcp1ctr  16267  2lgslem1c  16375  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  wlklenvclwlk  16780  clwwlknonex2lem2  16845