ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nn0cn Unicode version

Theorem nn0cn 9154
Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0cn  |-  ( A  e.  NN0  ->  A  e.  CC )

Proof of Theorem nn0cn
StepHypRef Expression
1 nn0sscn 9149 . 2  |-  NN0  C_  CC
21sseli 3146 1  |-  ( A  e.  NN0  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2144   CCcc 7781   NN0cn0 9144
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 707  ax-5 1443  ax-7 1444  ax-gen 1445  ax-ie1 1489  ax-ie2 1490  ax-8 1500  ax-10 1501  ax-11 1502  ax-i12 1503  ax-bndl 1505  ax-4 1506  ax-17 1522  ax-i9 1526  ax-ial 1530  ax-i5r 1531  ax-ext 2155  ax-sep 4113  ax-cnex 7874  ax-resscn 7875  ax-1re 7877  ax-addrcl 7880  ax-rnegex 7892
This theorem depends on definitions:  df-bi 117  df-tru 1354  df-nf 1457  df-sb 1759  df-clab 2160  df-cleq 2166  df-clel 2169  df-nfc 2304  df-ral 2456  df-rex 2457  df-v 2735  df-un 3128  df-in 3130  df-ss 3137  df-sn 3592  df-int 3838  df-inn 8888  df-n0 9145
This theorem is referenced by:  nn0nnaddcl  9175  elnn0nn  9186  difgtsumgt  9290  nn0n0n1ge2  9291  uzaddcl  9554  fzctr  10098  nn0split  10101  zpnn0elfzo1  10173  ubmelm1fzo  10191  subfzo0  10207  modqmuladdnn0  10333  addmodidr  10338  modfzo0difsn  10360  nn0ennn  10398  expadd  10527  expmul  10530  bernneq  10605  bernneq2  10606  faclbnd  10684  faclbnd6  10687  bccmpl  10697  bcn0  10698  bcnn  10700  bcnp1n  10702  bcn2  10707  bcp1m1  10708  bcpasc  10709  bcn2p1  10713  hashfzo0  10767  hashfz0  10769  fisum0diag2  11419  hashiun  11450  binom1dif  11459  bcxmas  11461  geolim  11483  efaddlem  11646  efexp  11654  eftlub  11662  demoivreALT  11745  nn0ob  11876  modremain  11897  mulgcdr  11982  nn0seqcvgd  12004  modprmn0modprm0  12219  coprimeprodsq  12220  coprimeprodsq2  12221  pcexp  12272  dvdsprmpweqle  12299  difsqpwdvds  12300  znnen  12362  ennnfonelemp1  12370  mulgneg2  12872
  Copyright terms: Public domain W3C validator