Theorem nn0cni 9404

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 9403	. 2 ⊢ 𝐴 ∈ ℝ
3	2	recni 8181	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2200  ℂcc 8020  ℕ₀cn0 9392

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205  ax-cnex 8113  ax-resscn 8114  ax-1re 8116  ax-addrcl 8119  ax-rnegex 8131

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-sn 3673  df-int 3927  df-inn 9134  df-n0 9393

This theorem is referenced by:  nn0le2xi  9442  num0u  9611  num0h  9612  numsuc  9614  numsucc  9640  numma  9644  nummac  9645  numma2c  9646  numadd  9647  numaddc  9648  nummul1c  9649  nummul2c  9650  decrmanc  9657  decrmac  9658  decaddi  9660  decaddci  9661  decsubi  9663  decmul1  9664  decmulnc  9667  11multnc  9668  decmul10add  9669  6p5lem  9670  4t3lem  9697  7t3e21  9710  7t6e42  9713  8t3e24  9716  8t4e32  9717  8t8e64  9721  9t3e27  9723  9t4e36  9724  9t5e45  9725  9t6e54  9726  9t7e63  9727  9t11e99  9730  decbin0  9740  decbin2  9741  sq10  10964  3dec  10966  cats1fvn  11335  3dvdsdec  12416  3dvds2dec  12417  3lcm2e6  12722  dec5dvds  12975  dec5dvds2  12976  dec2nprm  12978  modxai  12979  mod2xi  12980  modsubi  12982  gcdi  12983  numexp0  12985  numexp1  12986  numexpp1  12987  numexp2x  12988  decsplit0b  12989  decsplit0  12990  decsplit1  12991  decsplit  12992  karatsuba  12993  2exp8  12998