Theorem nn0cni 12430

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

Syntax hints:   ∈ wcel 2109  ℂcc 11042  ℕ₀cn0 12418

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 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-mulcl 11106  ax-i2m1 11112

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 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-nn 12163  df-n0 12419

This theorem is referenced by:  num0u  12636  num0h  12637  numsuc  12639  numsucc  12665  numma  12669  nummac  12670  numma2c  12671  numadd  12672  numaddc  12673  nummul1c  12674  nummul2c  12675  decrmanc  12682  decrmac  12683  decaddi  12685  decaddci  12686  decsubi  12688  decmul1  12689  decmulnc  12692  11multnc  12693  decmul10add  12694  6p5lem  12695  4t3lem  12722  7t3e21  12735  7t6e42  12738  8t3e24  12741  8t4e32  12742  8t8e64  12746  9t3e27  12748  9t4e36  12749  9t5e45  12750  9t6e54  12751  9t7e63  12752  9t11e99  12755  decbin0  12765  decbin2  12766  sq10  14205  3dec  14207  nn0le2msqi  14208  nn0opthlem1  14209  nn0opthi  14211  nn0opth2i  14212  faclbnd4lem1  14234  cats1fvn  14800  bpoly4  16001  fsumcube  16002  3dvdsdec  16278  3dvds2dec  16279  divalglem2  16341  3lcm2e6  16678  phiprmpw  16722  dec5dvds  17011  dec5dvds2  17012  dec2nprm  17014  modxai  17015  mod2xi  17016  mod2xnegi  17018  modsubi  17019  gcdi  17020  numexp0  17022  numexp1  17023  numexpp1  17024  numexp2x  17025  decsplit0b  17026  decsplit0  17027  decsplit1  17028  decsplit  17029  karatsuba  17030  2exp8  17035  prmlem2  17066  83prm  17069  139prm  17070  163prm  17071  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  psdmul  22029  log2ublem1  26832  log2ublem2  26833  log2ublem3  26834  log2ub  26835  birthday  26840  ppidif  27049  bpos1lem  27169  9p10ne21  30372  dfdec100  32728  dp20u  32771  dp20h  32772  dpmul10  32788  dpmul100  32790  dp3mul10  32791  dpmul1000  32792  dpexpp1  32801  0dp2dp  32802  dpadd2  32803  dpadd  32804  dpmul  32806  dpmul4  32807  lmatfvlem  33778  ballotlemfp1  34456  ballotth  34502  reprlt  34583  hgt750lemd  34612  hgt750lem2  34616  subfacp1lem1  35139  poimirlem26  37613  poimirlem28  37615  420gcd8e4  41967  lcmeprodgcdi  41968  12lcm5e60  41969  60lcm7e420  41971  3exp7  42014  3lexlogpow5ineq1  42015  3lexlogpow5ineq5  42021  aks4d1p1p7  42035  aks4d1p1  42037  decaddcom  42245  sqn5i  42246  decpmulnc  42248  decpmul  42249  sqdeccom12  42250  sq3deccom12  42251  235t711  42266  ex-decpmul  42267  sq45  42632  sum9cubes  42633  resqrtvalex  43607  imsqrtvalex  43608  inductionexd  44117  unitadd  44157  fmtno5lem4  47530  257prm  47535  fmtno4prmfac  47546  fmtno5fac  47556  139prmALT  47570  127prm  47573  m11nprm  47575  11t31e341  47706  2exp340mod341  47707  ackval3012  48654