Theorem nn0cni 12487

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

Syntax hints:   ∈ wcel 2141  ℂcc 11065  ℕ₀cn0 12475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-mulcl 11129  ax-i2m1 11135

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-nn 12205  df-n0 12476

This theorem is referenced by:  num0u  12693  num0h  12694  numsuc  12696  numsucc  12727  numma  12731  nummac  12732  numma2c  12733  numadd  12734  numaddc  12735  nummul1c  12736  nummul2c  12737  decrmanc  12744  decrmac  12745  decaddi  12747  decaddci  12748  decsubi  12750  decmul1  12751  decmulnc  12754  11multnc  12755  decmul10add  12756  6p5lem  12757  4t3lem  12784  7t3e21  12797  7t6e42  12800  8t3e24  12803  8t4e32  12804  8t8e64  12808  9t3e27  12810  9t4e36  12811  9t5e45  12812  9t6e54  12813  9t7e63  12814  9t11e99OLD  12818  decbin0  12829  decbin2  12830  sq10  14271  3dec  14273  nn0le2msqi  14274  nn0opthlem1  14275  nn0opthi  14277  nn0opth2i  14278  faclbnd4lem1  14300  cats1fvn  14865  bpoly4  16080  fsumcube  16081  3dvdsdec  16357  3dvds2dec  16358  divalglem2  16420  3lcm2e6  16758  phiprmpw  16802  dec5dvds  17091  dec5dvds2  17092  dec2nprm  17094  modxai  17095  mod2xi  17096  mod2xnegi  17098  modsubi  17099  gcdi  17100  numexp0  17102  numexp1  17103  numexpp1  17104  numexp2x  17105  decsplit0b  17106  decsplit0  17107  decsplit1  17108  decsplit  17109  karatsuba  17110  2exp8  17115  prmlem2  17147  83prm  17150  139prm  17151  163prm  17152  631prm  17154  1259lem1  17158  1259lem2  17159  1259lem3  17160  1259lem4  17161  1259lem5  17162  1259prm  17163  2503lem1  17164  2503lem2  17165  2503lem3  17166  2503prm  17167  4001lem1  17168  4001lem2  17169  4001lem3  17170  4001lem4  17171  4001prm  17172  psdmul  22219  log2ublem1  26999  log2ublem2  27000  log2ublem3  27001  log2ub  27002  birthday  27007  ppidif  27215  bpos1lem  27334  9p10ne21  30629  dfdec100  32993  dp20u  33016  dp20h  33017  dpmul10  33033  dpmul100  33035  dp3mul10  33036  dpmul1000  33037  dpexpp1  33046  0dp2dp  33047  dpadd2  33048  dpadd  33049  dpmul  33051  dpmul4  33052  lmatfvlem  34073  ballotlemfp1  34750  ballotth  34796  reprlt  34874  hgt750lemd  34903  hgt750lem2  34907  subfacp1lem1  35490  poimirlem26  38106  poimirlem28  38108  420gcd8e4  42584  lcmeprodgcdi  42585  12lcm5e60  42586  60lcm7e420  42588  3exp7  42631  3lexlogpow5ineq1  42632  3lexlogpow5ineq5  42638  aks4d1p1p7  42652  aks4d1p1  42654  decaddcom  42854  sqn5i  42855  decpmulnc  42857  decpmul  42858  sqdeccom12  42859  sq3deccom12  42860  235t711  42875  ex-decpmul  42876  sq45  43214  sum9cubes  43215  resqrtvalex  44182  imsqrtvalex  44183  inductionexd  44692  unitadd  44732  sin5tlem4  47431  sin5tlem5  47432  goldratmolem2  47441  fmtno5lem4  48126  257prm  48131  fmtno4prmfac  48142  fmtno5fac  48152  139prmALT  48166  127prm  48169  m11nprm  48171  11t31e341  48315  2exp340mod341  48316  ackval3012  49275