Theorem nn0cni 11567

Description: A nonnegative integer is a complex number. (Contributed by NM, 14-May-2003.)

Hypothesis

Ref	Expression
nn0rei.1	⊢ 𝐴 ∈ ℕ0

Assertion

Ref	Expression
nn0cni	⊢ 𝐴 ∈ ℂ

Proof of Theorem nn0cni

Step	Hyp	Ref	Expression
1		nn0rei.1	. . 3 ⊢ 𝐴 ∈ ℕ0
2	1	nn0rei 11566	. 2 ⊢ 𝐴 ∈ ℝ
3	2	recni 10336	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2158  ℂcc 10216  ℕ₀cn0 11555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-i2m1 10286  ax-1ne0 10287  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-iun 4710  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-ov 6874  df-om 7293  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-nn 11303  df-n0 11556

This theorem is referenced by:  nn0le2xi  11609  num0u  11766  num0h  11767  numsuc  11769  numsucc  11795  numma  11799  nummac  11800  numma2c  11801  numadd  11802  numaddc  11803  nummul1c  11804  nummul2c  11805  decrmanc  11812  decrmac  11813  decaddi  11815  decaddci  11816  decsubi  11818  decmul1  11819  decmulnc  11822  11multnc  11823  decmul10add  11824  6p5lem  11825  4t3lem  11852  7t3e21  11865  7t6e42  11868  8t3e24  11871  8t4e32  11872  8t8e64  11876  9t3e27  11878  9t4e36  11879  9t5e45  11880  9t6e54  11881  9t7e63  11882  9t11e99  11885  decbin0  11895  decbin2  11896  sq10  13267  3dec  13269  nn0le2msqi  13270  nn0opthlem1  13271  nn0opthi  13273  nn0opth2i  13274  faclbnd4lem1  13296  cats1fvn  13823  bpoly4  15006  fsumcube  15007  3dvdsdec  15272  3dvds2dec  15273  divalglem2  15334  3lcm2e6  15653  phiprmpw  15694  dec5dvds  15981  dec5dvds2  15982  dec2nprm  15984  modxai  15985  mod2xi  15986  mod2xnegi  15988  modsubi  15989  gcdi  15990  decexp2  15992  numexp0  15993  numexp1  15994  numexpp1  15995  numexp2x  15996  decsplit0b  15997  decsplit0  15998  decsplit1  15999  decsplit  16000  karatsuba  16001  2exp8  16004  prmlem2  16034  83prm  16037  139prm  16038  163prm  16039  631prm  16041  1259lem1  16045  1259lem2  16046  1259lem3  16047  1259lem4  16048  1259lem5  16049  1259prm  16050  2503lem1  16051  2503lem2  16052  2503lem3  16053  2503prm  16054  4001lem1  16055  4001lem2  16056  4001lem3  16057  4001lem4  16058  4001prm  16059  log2ublem1  24883  log2ublem2  24884  log2ublem3  24885  log2ub  24886  birthday  24891  ppidif  25099  bpos1lem  25217  dfdec100  29900  dp20u  29908  dp20h  29909  dpmul10  29925  dpmul100  29927  dp3mul10  29928  dpmul1000  29929  dpexpp1  29938  0dp2dp  29939  dpadd2  29940  dpadd  29941  dpmul  29943  dpmul4  29944  lmatfvlem  30203  ballotlemfp1  30875  ballotth  30921  reprlt  31019  hgt750lemd  31048  hgt750lem2  31052  subfacp1lem1  31481  poimirlem26  33745  poimirlem28  33747  sqn5i  37743  inductionexd  38950  unitadd  38995  fmtno5lem4  42040  257prm  42045  fmtno4prmfac  42056  fmtno5fac  42066  139prmALT  42083  127prm  42087  m11nprm  42090