Theorem nn0cni 12456

Description: A nonnegative integer is a complex number. (Contributed by NM, 14-May-2003.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 8-Oct-2022.)

Hypothesis

Ref	Expression
nn0rei.1	⊢ 𝐴 ∈ ℕ0

Assertion

Ref	Expression
nn0cni	⊢ 𝐴 ∈ ℂ

Proof of Theorem nn0cni

Step	Hyp	Ref	Expression
1		nn0sscn 12449	. 2 ⊢ ℕ0 ⊆ ℂ
2		nn0rei.1	. 2 ⊢ 𝐴 ∈ ℕ0
3	1, 2	sselii 3966	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2106  ℂcc 11080  ℕ₀cn0 12444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5283  ax-nul 5290  ax-pr 5411  ax-un 7699  ax-1cn 11140  ax-icn 11141  ax-addcl 11142  ax-mulcl 11144  ax-i2m1 11150

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3372  df-rab 3426  df-v 3468  df-sbc 3765  df-csb 3881  df-dif 3938  df-un 3940  df-in 3942  df-ss 3952  df-pss 3954  df-nul 4310  df-if 4514  df-pw 4589  df-sn 4614  df-pr 4616  df-op 4620  df-uni 4893  df-iun 4983  df-br 5133  df-opab 5195  df-mpt 5216  df-tr 5250  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5615  df-we 5617  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6280  df-ord 6347  df-on 6348  df-lim 6349  df-suc 6350  df-iota 6475  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-ov 7387  df-om 7830  df-2nd 7949  df-frecs 8239  df-wrecs 8270  df-recs 8344  df-rdg 8383  df-nn 12185  df-n0 12445

This theorem is referenced by:  nn0le2xi  12498  num0u  12660  num0h  12661  numsuc  12663  numsucc  12689  numma  12693  nummac  12694  numma2c  12695  numadd  12696  numaddc  12697  nummul1c  12698  nummul2c  12699  decrmanc  12706  decrmac  12707  decaddi  12709  decaddci  12710  decsubi  12712  decmul1  12713  decmulnc  12716  11multnc  12717  decmul10add  12718  6p5lem  12719  4t3lem  12746  7t3e21  12759  7t6e42  12762  8t3e24  12765  8t4e32  12766  8t8e64  12770  9t3e27  12772  9t4e36  12773  9t5e45  12774  9t6e54  12775  9t7e63  12776  9t11e99  12779  decbin0  12789  decbin2  12790  sq10  14196  3dec  14198  nn0le2msqi  14199  nn0opthlem1  14200  nn0opthi  14202  nn0opth2i  14203  faclbnd4lem1  14225  cats1fvn  14781  bpoly4  15975  fsumcube  15976  3dvdsdec  16247  3dvds2dec  16248  divalglem2  16310  3lcm2e6  16640  phiprmpw  16681  dec5dvds  16969  dec5dvds2  16970  dec2nprm  16972  modxai  16973  mod2xi  16974  mod2xnegi  16976  modsubi  16977  gcdi  16978  decexp2  16980  numexp0  16981  numexp1  16982  numexpp1  16983  numexp2x  16984  decsplit0b  16985  decsplit0  16986  decsplit1  16987  decsplit  16988  karatsuba  16989  2exp8  16994  prmlem2  17025  83prm  17028  139prm  17029  163prm  17030  631prm  17032  1259lem1  17036  1259lem2  17037  1259lem3  17038  1259lem4  17039  1259lem5  17040  1259prm  17041  2503lem1  17042  2503lem2  17043  2503lem3  17044  2503prm  17045  4001lem1  17046  4001lem2  17047  4001lem3  17048  4001lem4  17049  4001prm  17050  log2ublem1  26355  log2ublem2  26356  log2ublem3  26357  log2ub  26358  birthday  26363  ppidif  26571  bpos1lem  26689  9p10ne21  29518  dfdec100  31837  dp20u  31845  dp20h  31846  dpmul10  31862  dpmul100  31864  dp3mul10  31865  dpmul1000  31866  dpexpp1  31875  0dp2dp  31876  dpadd2  31877  dpadd  31878  dpmul  31880  dpmul4  31881  lmatfvlem  32526  ballotlemfp1  33221  ballotth  33267  reprlt  33362  hgt750lemd  33391  hgt750lem2  33395  subfacp1lem1  33901  poimirlem26  36218  poimirlem28  36220  420gcd8e4  40576  lcmeprodgcdi  40577  12lcm5e60  40578  60lcm7e420  40580  3exp7  40623  3lexlogpow5ineq1  40624  3lexlogpow5ineq5  40630  aks4d1p1p7  40644  aks4d1p1  40646  decaddcom  40896  sqn5i  40897  decpmulnc  40899  decpmul  40900  sqdeccom12  40901  sq3deccom12  40902  235t711  40903  ex-decpmul  40904  resqrtvalex  42079  imsqrtvalex  42080  inductionexd  42589  unitadd  42630  fmtno5lem4  45908  257prm  45913  fmtno4prmfac  45924  fmtno5fac  45934  139prmALT  45948  127prm  45951  m11nprm  45953  11t31e341  46084  2exp340mod341  46085  ackval3012  46938