Theorem nn0cn 9278

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℂcc 7896  ℕ₀cn0 9268

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4152  ax-cnex 7989  ax-resscn 7990  ax-1re 7992  ax-addrcl 7995  ax-rnegex 8007

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-sn 3629  df-int 3876  df-inn 9010  df-n0 9269

This theorem is referenced by:  nn0nnaddcl  9299  elnn0nn  9310  difgtsumgt  9414  nn0n0n1ge2  9415  uzaddcl  9679  fzctr  10227  nn0split  10230  zpnn0elfzo1  10303  ubmelm1fzo  10321  subfzo0  10337  modqmuladdnn0  10479  addmodidr  10484  modfzo0difsn  10506  nn0ennn  10544  expadd  10692  expmul  10695  bernneq  10771  bernneq2  10772  faclbnd  10852  faclbnd6  10855  bccmpl  10865  bcn0  10866  bcnn  10868  bcnp1n  10870  bcn2  10875  bcp1m1  10876  bcpasc  10877  bcn2p1  10881  hashfzo0  10934  hashfz0  10936  fisum0diag2  11631  hashiun  11662  binom1dif  11671  bcxmas  11673  geolim  11695  efaddlem  11858  efexp  11866  eftlub  11874  demoivreALT  11958  nn0ob  12092  modremain  12113  mulgcdr  12212  nn0seqcvgd  12236  modprmn0modprm0  12452  coprimeprodsq  12453  coprimeprodsq2  12454  pcexp  12505  dvdsprmpweqle  12533  difsqpwdvds  12534  znnen  12642  ennnfonelemp1  12650  mulgneg2  13364  cnfldmulg  14210  nn0subm  14217  rpcxpmul2  15257  0sgmppw  15337  2lgslem1c  15439  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449