Theorem nn0cni 12538

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

Syntax hints:   ∈ wcel 2108  ℂcc 11153  ℕ₀cn0 12526

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-i2m1 11223

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-n0 12527

This theorem is referenced by:  num0u  12744  num0h  12745  numsuc  12747  numsucc  12773  numma  12777  nummac  12778  numma2c  12779  numadd  12780  numaddc  12781  nummul1c  12782  nummul2c  12783  decrmanc  12790  decrmac  12791  decaddi  12793  decaddci  12794  decsubi  12796  decmul1  12797  decmulnc  12800  11multnc  12801  decmul10add  12802  6p5lem  12803  4t3lem  12830  7t3e21  12843  7t6e42  12846  8t3e24  12849  8t4e32  12850  8t8e64  12854  9t3e27  12856  9t4e36  12857  9t5e45  12858  9t6e54  12859  9t7e63  12860  9t11e99  12863  decbin0  12873  decbin2  12874  sq10  14303  3dec  14305  nn0le2msqi  14306  nn0opthlem1  14307  nn0opthi  14309  nn0opth2i  14310  faclbnd4lem1  14332  cats1fvn  14897  bpoly4  16095  fsumcube  16096  3dvdsdec  16369  3dvds2dec  16370  divalglem2  16432  3lcm2e6  16769  phiprmpw  16813  dec5dvds  17102  dec5dvds2  17103  dec2nprm  17105  modxai  17106  mod2xi  17107  mod2xnegi  17109  modsubi  17110  gcdi  17111  numexp0  17113  numexp1  17114  numexpp1  17115  numexp2x  17116  decsplit0b  17117  decsplit0  17118  decsplit1  17119  decsplit  17120  karatsuba  17121  2exp8  17126  prmlem2  17157  83prm  17160  139prm  17161  163prm  17162  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  psdmul  22170  log2ublem1  26989  log2ublem2  26990  log2ublem3  26991  log2ub  26992  birthday  26997  ppidif  27206  bpos1lem  27326  9p10ne21  30489  dfdec100  32832  dp20u  32860  dp20h  32861  dpmul10  32877  dpmul100  32879  dp3mul10  32880  dpmul1000  32881  dpexpp1  32890  0dp2dp  32891  dpadd2  32892  dpadd  32893  dpmul  32895  dpmul4  32896  lmatfvlem  33814  ballotlemfp1  34494  ballotth  34540  reprlt  34634  hgt750lemd  34663  hgt750lem2  34667  subfacp1lem1  35184  poimirlem26  37653  poimirlem28  37655  420gcd8e4  42007  lcmeprodgcdi  42008  12lcm5e60  42009  60lcm7e420  42011  3exp7  42054  3lexlogpow5ineq1  42055  3lexlogpow5ineq5  42061  aks4d1p1p7  42075  aks4d1p1  42077  decaddcom  42319  sqn5i  42320  decpmulnc  42322  decpmul  42323  sqdeccom12  42324  sq3deccom12  42325  235t711  42339  ex-decpmul  42340  sq45  42681  sum9cubes  42682  resqrtvalex  43658  imsqrtvalex  43659  inductionexd  44168  unitadd  44208  fmtno5lem4  47543  257prm  47548  fmtno4prmfac  47559  fmtno5fac  47569  139prmALT  47583  127prm  47586  m11nprm  47588  11t31e341  47719  2exp340mod341  47720  ackval3012  48613