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

Theorem nn0cni 8367
Description: A nonnegative integer is a complex number. (Contributed by NM, 14-May-2003.)
Hypothesis
Ref Expression
nn0re.1 𝐴 ∈ ℕ0
Assertion
Ref Expression
nn0cni 𝐴 ∈ ℂ

Proof of Theorem nn0cni
StepHypRef Expression
1 nn0re.1 . . 3 𝐴 ∈ ℕ0
21nn0rei 8366 . 2 𝐴 ∈ ℝ
32recni 7193 1 𝐴 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1434  cc 7041  0cn0 8355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-sep 3904  ax-cnex 7129  ax-resscn 7130  ax-1re 7132  ax-addrcl 7135  ax-rnegex 7147
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ral 2354  df-rex 2355  df-v 2604  df-un 2978  df-in 2980  df-ss 2987  df-sn 3412  df-int 3645  df-inn 8107  df-n0 8356
This theorem is referenced by:  nn0le2xi  8405  num0u  8568  num0h  8569  numsuc  8571  numsucc  8597  numma  8601  nummac  8602  numma2c  8603  numadd  8604  numaddc  8605  nummul1c  8606  nummul2c  8607  decrmanc  8614  decrmac  8615  decaddi  8617  decaddci  8618  decsubi  8620  decmul1  8621  decmulnc  8624  11multnc  8625  decmul10add  8626  6p5lem  8627  4t3lem  8654  7t3e21  8667  7t6e42  8670  8t3e24  8673  8t4e32  8674  8t8e64  8678  9t3e27  8680  9t4e36  8681  9t5e45  8682  9t6e54  8683  9t7e63  8684  9t11e99  8687  decbin0  8697  decbin2  8698  sq10  9737  3dec  9739  3dvdsdec  10409  3dvds2dec  10410  3lcm2e6  10683
  Copyright terms: Public domain W3C validator