Theorem nn0cni 12658

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

This proof depends on syntax axioms:   ∈ wcel 2147  ℂcc 11237  ℕ₀cn0 12646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-i2m1 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376  df-n0 12647

This theorem is used by:  num0u  12865  num0h  12866  numsuc  12868  numsucc  12899  numma  12903  nummac  12904  numma2c  12905  numadd  12906  numaddc  12907  nummul1c  12908  nummul2c  12909  decrmanc  12916  decrmac  12917  decaddi  12919  decaddci  12920  decsubi  12922  decmul1  12923  decmulnc  12926  11multnc  12927  decmul10add  12928  6p5lem  12929  4t3lem  12956  7t3e21  12969  7t6e42  12972  8t3e24  12975  8t4e32  12976  8t8e64  12980  9t3e27  12982  9t4e36  12983  9t5e45  12984  9t6e54  12985  9t7e63  12986  9t11e99OLD  12990  decbin0  13001  decbin2  13002  sq10  14449  3dec  14451  nn0le2msqi  14452  nn0opthlem1  14453  nn0opthi  14455  nn0opth2i  14456  faclbnd4lem1  14478  cats1fvn  15051  bpoly4  16269  fsumcube  16270  3dvdsdec  16546  3dvds2dec  16547  divalglem2  16609  3lcm2e6  16952  phiprmpw  16997  dec5dvds  17286  dec5dvds2  17287  dec2nprm  17289  modxai  17290  mod2xi  17291  mod2xnegi  17293  modsubi  17294  gcdi  17295  numexp0  17297  numexp1  17298  numexpp1  17299  numexp2x  17300  decsplit0b  17301  decsplit0  17302  decsplit1  17303  decsplit  17304  karatsuba  17305  2exp8  17310  prmlem2  17342  139prm  17346  163prm  17347  631prm  17349  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  1259prm  17358  2503lem1  17359  2503lem2  17360  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  4001prm  17367  psdmul  22542  log2ublem1  27331  log2ublem2  27332  log2ublem3  27333  log2ub  27334  birthday  27339  ppidif  27547  bpos1lem  27666  9p10ne21  31128  dfdec100  33517  dp20u  33540  dp20h  33541  dpmul10  33557  dpmul100  33559  dp3mul10  33560  dpmul1000  33561  dpexpp1  33570  0dp2dp  33571  dpadd2  33572  dpadd  33573  dpmul  33575  dpmul4  33576  lmatfvlem  34558  ballotlemfp1  35235  ballotth  35281  reprlt  35359  hgt750lemd  35388  hgt750lem2  35392  subfacp1lem1  36152  poimirlem26  38832  poimirlem28  38834  420gcd8e4  43322  lcmeprodgcdi  43323  12lcm5e60  43324  60lcm7e420  43326  3exp7  43369  3lexlogpow5ineq1  43370  3lexlogpow5ineq5  43376  aks4d1p1p7  43390  aks4d1p1  43392  decaddcom  43607  sqn5i  43608  decpmulnc  43610  decpmul  43611  sqdeccom12  43612  sq3deccom12  43613  235t711  43628  ex-decpmul  43629  sq45  43948  sum9cubes  43949  resqrtvalex  44906  imsqrtvalex  44907  inductionexd  45416  unitadd  45456  sin5tlem4  48195  sin5tlem5  48196  goldratmolem2  48206  fmtno5lem4  48914  257prm  48919  fmtno4prmfac  48930  fmtno5fac  48940  139prmALT  48954  127prm  48957  m11nprm  48959  11t31e341  49103  2exp340mod341  49104  ackval3012  50135