Theorem nn0cni 12454

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

Syntax hints:   ∈ wcel 2109  ℂcc 11066  ℕ₀cn0 12442

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-i2m1 11136

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-n0 12443

This theorem is referenced by:  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  14229  3dec  14231  nn0le2msqi  14232  nn0opthlem1  14233  nn0opthi  14235  nn0opth2i  14236  faclbnd4lem1  14258  cats1fvn  14824  bpoly4  16025  fsumcube  16026  3dvdsdec  16302  3dvds2dec  16303  divalglem2  16365  3lcm2e6  16702  phiprmpw  16746  dec5dvds  17035  dec5dvds2  17036  dec2nprm  17038  modxai  17039  mod2xi  17040  mod2xnegi  17042  modsubi  17043  gcdi  17044  numexp0  17046  numexp1  17047  numexpp1  17048  numexp2x  17049  decsplit0b  17050  decsplit0  17051  decsplit1  17052  decsplit  17053  karatsuba  17054  2exp8  17059  prmlem2  17090  83prm  17093  139prm  17094  163prm  17095  631prm  17097  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  psdmul  22053  log2ublem1  26856  log2ublem2  26857  log2ublem3  26858  log2ub  26859  birthday  26864  ppidif  27073  bpos1lem  27193  9p10ne21  30399  dfdec100  32755  dp20u  32798  dp20h  32799  dpmul10  32815  dpmul100  32817  dp3mul10  32818  dpmul1000  32819  dpexpp1  32828  0dp2dp  32829  dpadd2  32830  dpadd  32831  dpmul  32833  dpmul4  32834  lmatfvlem  33805  ballotlemfp1  34483  ballotth  34529  reprlt  34610  hgt750lemd  34639  hgt750lem2  34643  subfacp1lem1  35166  poimirlem26  37640  poimirlem28  37642  420gcd8e4  41994  lcmeprodgcdi  41995  12lcm5e60  41996  60lcm7e420  41998  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1p7  42062  aks4d1p1  42064  decaddcom  42272  sqn5i  42273  decpmulnc  42275  decpmul  42276  sqdeccom12  42277  sq3deccom12  42278  235t711  42293  ex-decpmul  42294  sq45  42659  sum9cubes  42660  resqrtvalex  43634  imsqrtvalex  43635  inductionexd  44144  unitadd  44184  fmtno5lem4  47557  257prm  47562  fmtno4prmfac  47573  fmtno5fac  47583  139prmALT  47597  127prm  47600  m11nprm  47602  11t31e341  47733  2exp340mod341  47734  ackval3012  48681