Theorem nn0cni 12622

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

This proof depends on syntax axioms:   ∈ wcel 2144  ℂcc 11202  ℕ₀cn0 12610

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752  ax-1cn 11262  ax-icn 11263  ax-addcl 11264  ax-mulcl 11266  ax-i2m1 11272

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7424  df-om 7879  df-2nd 8003  df-frecs 8303  df-wrecs 8334  df-recs 8383  df-rdg 8422  df-nn 12340  df-n0 12611

This theorem is used by:  num0u  12829  num0h  12830  numsuc  12832  numsucc  12863  numma  12867  nummac  12868  numma2c  12869  numadd  12870  numaddc  12871  nummul1c  12872  nummul2c  12873  decrmanc  12880  decrmac  12881  decaddi  12883  decaddci  12884  decsubi  12886  decmul1  12887  decmulnc  12890  11multnc  12891  decmul10add  12892  6p5lem  12893  4t3lem  12920  7t3e21  12933  7t6e42  12936  8t3e24  12939  8t4e32  12940  8t8e64  12944  9t3e27  12946  9t4e36  12947  9t5e45  12948  9t6e54  12949  9t7e63  12950  9t11e99OLD  12954  decbin0  12965  decbin2  12966  sq10  14412  3dec  14414  nn0le2msqi  14415  nn0opthlem1  14416  nn0opthi  14418  nn0opth2i  14419  faclbnd4lem1  14441  cats1fvn  15014  bpoly4  16231  fsumcube  16232  3dvdsdec  16508  3dvds2dec  16509  divalglem2  16571  3lcm2e6  16914  phiprmpw  16959  dec5dvds  17248  dec5dvds2  17249  dec2nprm  17251  modxai  17252  mod2xi  17253  mod2xnegi  17255  modsubi  17256  gcdi  17257  numexp0  17259  numexp1  17260  numexpp1  17261  numexp2x  17262  decsplit0b  17263  decsplit0  17264  decsplit1  17265  decsplit  17266  karatsuba  17267  2exp8  17272  prmlem2  17304  139prm  17308  163prm  17309  631prm  17311  1259lem1  17315  1259lem2  17316  1259lem3  17317  1259lem4  17318  1259lem5  17319  1259prm  17320  2503lem1  17321  2503lem2  17322  2503lem3  17323  2503prm  17324  4001lem1  17325  4001lem2  17326  4001lem3  17327  4001lem4  17328  4001prm  17329  psdmul  22493  log2ublem1  27280  log2ublem2  27281  log2ublem3  27282  log2ub  27283  birthday  27288  ppidif  27496  bpos1lem  27615  9p10ne21  31077  dfdec100  33468  dp20u  33491  dp20h  33492  dpmul10  33508  dpmul100  33510  dp3mul10  33511  dpmul1000  33512  dpexpp1  33521  0dp2dp  33522  dpadd2  33523  dpadd  33524  dpmul  33526  dpmul4  33527  lmatfvlem  34494  ballotlemfp1  35171  ballotth  35217  reprlt  35295  hgt750lemd  35324  hgt750lem2  35328  subfacp1lem1  36031  poimirlem26  38658  poimirlem28  38660  420gcd8e4  43150  lcmeprodgcdi  43151  12lcm5e60  43152  60lcm7e420  43154  3exp7  43197  3lexlogpow5ineq1  43198  3lexlogpow5ineq5  43204  aks4d1p1p7  43218  aks4d1p1  43220  decaddcom  43435  sqn5i  43436  decpmulnc  43438  decpmul  43439  sqdeccom12  43440  sq3deccom12  43441  235t711  43456  ex-decpmul  43457  sq45  43776  sum9cubes  43777  resqrtvalex  44739  imsqrtvalex  44740  inductionexd  45249  unitadd  45289  sin5tlem4  48016  sin5tlem5  48017  goldratmolem2  48027  fmtno5lem4  48735  257prm  48740  fmtno4prmfac  48751  fmtno5fac  48761  139prmALT  48775  127prm  48778  m11nprm  48780  11t31e341  48924  2exp340mod341  48925  ackval3012  49898