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

Theorem nn0cn 8249
Description: A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.)
Assertion
Ref Expression
nn0cn (𝐴 ∈ ℕ0𝐴 ∈ ℂ)

Proof of Theorem nn0cn
StepHypRef Expression
1 nn0sscn 8244 . 2 0 ⊆ ℂ
21sseli 2969 1 (𝐴 ∈ ℕ0𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  cc 6945  0cn0 8239
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903  ax-cnex 7033  ax-resscn 7034  ax-1re 7036  ax-addrcl 7039  ax-rnegex 7051
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-un 2950  df-in 2952  df-ss 2959  df-sn 3409  df-int 3644  df-inn 7991  df-n0 8240
This theorem is referenced by:  nn0nnaddcl  8270  elnn0nn  8281  nn0n0n1ge2  8369  uzaddcl  8625  fzctr  9093  nn0split  9096  zpnn0elfzo1  9166  ubmelm1fzo  9184  subfzo0  9199  modqmuladdnn0  9318  addmodidr  9323  modfzo0difsn  9345  nn0ennn  9373  expadd  9462  expmul  9465  bernneq  9537  bernneq2  9538  faclbnd  9609  faclbnd6  9612  bccmpl  9622  bcn0  9623  bcnn  9625  bcnp1n  9627  bcn2  9632  bcp1m1  9633  bcpasc  9634  bcn2p1  9638  nn0ob  10220  modremain  10241  nn0seqcvgd  10263
  Copyright terms: Public domain W3C validator