Theorem nn0cni 9107

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

Step	Hyp	Ref	Expression
1		nn0re.1	. . 3 ⊢ 𝐴 ∈ ℕ0
2	1	nn0rei 9106	. 2 ⊢ 𝐴 ∈ ℝ
3	2	recni 7892	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2128  ℂcc 7732  ℕ₀cn0 9095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-sep 4084  ax-cnex 7825  ax-resscn 7826  ax-1re 7828  ax-addrcl 7831  ax-rnegex 7843

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-sn 3567  df-int 3810  df-inn 8839  df-n0 9096

This theorem is referenced by:  nn0le2xi  9145  num0u  9310  num0h  9311  numsuc  9313  numsucc  9339  numma  9343  nummac  9344  numma2c  9345  numadd  9346  numaddc  9347  nummul1c  9348  nummul2c  9349  decrmanc  9356  decrmac  9357  decaddi  9359  decaddci  9360  decsubi  9362  decmul1  9363  decmulnc  9366  11multnc  9367  decmul10add  9368  6p5lem  9369  4t3lem  9396  7t3e21  9409  7t6e42  9412  8t3e24  9415  8t4e32  9416  8t8e64  9420  9t3e27  9422  9t4e36  9423  9t5e45  9424  9t6e54  9425  9t7e63  9426  9t11e99  9429  decbin0  9439  decbin2  9440  sq10  10597  3dec  10599  3dvdsdec  11768  3dvds2dec  11769  3lcm2e6  12050