Theorem nn0cn 9552

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

Syntax hints:   → wi 4   ∈ wcel 2209  ℂcc 8167  ℕ₀cn0 9542

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 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 4244  ax-cnex 8260  ax-resscn 8261  ax-1re 8263  ax-addrcl 8266  ax-rnegex 8278

This theorem 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 3711  df-int 3966  df-inn 9284  df-n0 9543

This theorem is referenced by:  nn0nnaddcl  9573  elnn0nn  9584  difgtsumgt  9693  nn0n0n1ge2  9694  uzaddcl  9965  fzctr  10518  nn0split  10521  elfzoext  10588  zpnn0elfzo1  10604  ubmelm1fzo  10622  subfzo0  10639  modqmuladdnn0  10783  addmodidr  10788  modfzo0difsn  10810  nn0ennn  10848  expadd  10996  expmul  10999  bernneq  11076  bernneq2  11077  faclbnd  11157  faclbnd6  11160  bccmpl  11170  bcn0  11171  bcnn  11173  bcnp1n  11175  bcn2  11180  bcp1m1  11181  bcpasc  11182  bcn2p1  11187  hashfzo0  11242  hashfz0  11244  ccatalpha  11359  ccatws1lenp1bg  11381  ccatw2s1leng  11384  swrdfv2  11413  swrdspsleq  11417  swrdlsw  11419  pfxmpt  11430  pfxswrd  11456  wrdind  11472  wrd2ind  11473  pfxccatin12lem4  11476  pfxccatin12lem1  11478  pfxccatin12lem2  11481  pfxccatin12  11483  swrdccat3blem  11489  fisum0diag2  12192  hashiun  12223  binom1dif  12232  bcxmas  12234  geolim  12256  efaddlem  12419  efexp  12427  eftlub  12435  demoivreALT  12519  nn0ob  12653  modremain  12674  mulgcdr  12773  nn0seqcvgd  12797  modprmn0modprm0  13013  coprimeprodsq  13014  coprimeprodsq2  13015  pcexp  13066  dvdsprmpweqle  13094  difsqpwdvds  13095  znnen  13267  ennnfonelemp1  13275  mulgneg2  13936  cnfldmulg  14885  nn0subm  14892  psrbagconf1o  14987  rpcxpmul2  15938  0sgmppw  16021  2lgslem1c  16123  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  wlklenvclwlk  16528  clwwlknonex2lem2  16593