Theorem nn0cni 12461

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 12454	. 2 ⊢ ℕ0 ⊆ ℂ
2		nn0rei.1	. 2 ⊢ 𝐴 ∈ ℕ0
3	1, 2	sselii 3946	1 ⊢ 𝐴 ∈ ℂ

Syntax hints:   ∈ wcel 2109  ℂcc 11073  ℕ₀cn0 12449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-i2m1 11143

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194  df-n0 12450

This theorem is referenced by:  num0u  12667  num0h  12668  numsuc  12670  numsucc  12696  numma  12700  nummac  12701  numma2c  12702  numadd  12703  numaddc  12704  nummul1c  12705  nummul2c  12706  decrmanc  12713  decrmac  12714  decaddi  12716  decaddci  12717  decsubi  12719  decmul1  12720  decmulnc  12723  11multnc  12724  decmul10add  12725  6p5lem  12726  4t3lem  12753  7t3e21  12766  7t6e42  12769  8t3e24  12772  8t4e32  12773  8t8e64  12777  9t3e27  12779  9t4e36  12780  9t5e45  12781  9t6e54  12782  9t7e63  12783  9t11e99  12786  decbin0  12796  decbin2  12797  sq10  14236  3dec  14238  nn0le2msqi  14239  nn0opthlem1  14240  nn0opthi  14242  nn0opth2i  14243  faclbnd4lem1  14265  cats1fvn  14831  bpoly4  16032  fsumcube  16033  3dvdsdec  16309  3dvds2dec  16310  divalglem2  16372  3lcm2e6  16709  phiprmpw  16753  dec5dvds  17042  dec5dvds2  17043  dec2nprm  17045  modxai  17046  mod2xi  17047  mod2xnegi  17049  modsubi  17050  gcdi  17051  numexp0  17053  numexp1  17054  numexpp1  17055  numexp2x  17056  decsplit0b  17057  decsplit0  17058  decsplit1  17059  decsplit  17060  karatsuba  17061  2exp8  17066  prmlem2  17097  83prm  17100  139prm  17101  163prm  17102  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  psdmul  22060  log2ublem1  26863  log2ublem2  26864  log2ublem3  26865  log2ub  26866  birthday  26871  ppidif  27080  bpos1lem  27200  9p10ne21  30406  dfdec100  32762  dp20u  32805  dp20h  32806  dpmul10  32822  dpmul100  32824  dp3mul10  32825  dpmul1000  32826  dpexpp1  32835  0dp2dp  32836  dpadd2  32837  dpadd  32838  dpmul  32840  dpmul4  32841  lmatfvlem  33812  ballotlemfp1  34490  ballotth  34536  reprlt  34617  hgt750lemd  34646  hgt750lem2  34650  subfacp1lem1  35173  poimirlem26  37647  poimirlem28  37649  420gcd8e4  42001  lcmeprodgcdi  42002  12lcm5e60  42003  60lcm7e420  42005  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1p7  42069  aks4d1p1  42071  decaddcom  42279  sqn5i  42280  decpmulnc  42282  decpmul  42283  sqdeccom12  42284  sq3deccom12  42285  235t711  42300  ex-decpmul  42301  sq45  42666  sum9cubes  42667  resqrtvalex  43641  imsqrtvalex  43642  inductionexd  44151  unitadd  44191  fmtno5lem4  47561  257prm  47566  fmtno4prmfac  47577  fmtno5fac  47587  139prmALT  47601  127prm  47604  m11nprm  47606  11t31e341  47737  2exp340mod341  47738  ackval3012  48685